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