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

Volume

1

fYear

2009

fDate

22-24 May 2009

Firstpage

318

Lastpage

322

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;

fLanguage

English

Publisher

ieee

Conference_Titel

Electronic Commerce and Security, 2009. ISECS '09. Second International Symposium on

Conference_Location

Nanchang

Print_ISBN

978-0-7695-3643-9

Type

conf

DOI

10.1109/ISECS.2009.155

Filename

5209789