Title : 
Security Protocol Analysis Based on Rewriting Approximation
         
        
            Author : 
Liu, Nan ; Zhu, Wen-Ye ; Zhu, Yue-Fei
         
        
            Author_Institution : 
Network Eng. Dept., Zhengzhou Inf. Sci. & Technol. Inst., Zhengzhou, China
         
        
        
        
        
        
        
            Abstract : 
TA4SP is a state-of-art tool of AVISPA that can automatically verify security protocol with unbounded number of parallel sessions. But it still has some limitations and can´t verify hierarchy of authentication automatically. In this paper, we use an approximation-based model to define security protocol and design an algorithm close to the real implementation to calculate the fix-point tree automata based on the tool TA4SP. A method is proposed for analyzing hierarchy of authentication properties as extension of TA4SP. We illustrate the effectiveness of this model with the example of NSPK protocol.
         
        
            Keywords : 
automata theory; cryptographic protocols; trees (mathematics); AVISPA; NSPK protocol; TA4SP; fix-point tree automata; rewriting approximation; security protocol analysis; Algorithm design and analysis; Authentication; Automata; Cryptographic protocols; Cryptography; Electronic commerce; Humans; Information analysis; Information science; Information security; approximation; authentication; fix-point tree automata; security protocol;
         
        
        
        
            Conference_Titel : 
Electronic Commerce and Security, 2009. ISECS '09. Second International Symposium on
         
        
            Conference_Location : 
Nanchang
         
        
            Print_ISBN : 
978-0-7695-3643-9
         
        
        
            DOI : 
10.1109/ISECS.2009.155