Title :
ASM-SPV: A Model Checker for Security Protocols
Author :
Peng, Jianhua ; Liu, Feng ; Zhao, Zhenju ; Huang, Danqing ; Xue, Rui
Author_Institution :
State Key Lab. Of Inf. Security, Chinese Acad. of Sci., Beijing, China
Abstract :
This paper presents details of a model checker for security protocols, called ASM-SPV (Abstract State Machines-Security Protocols Verifier), which employs the on-the-fly model checking technique as the convenient verification method and directly supports the whole Core- ASM language. Security protocol is modeled as distributed abstract state machines and the property to be verified is specified in form of the CTL (Computation Tree Logic) formula in the model checker. This paper also introduces the features of the model checker in detail and shows the efficiency and usability by taking the verification of the authentication of Helsinki protocol as an example. Then advantages over FDR are presented and the runtime performance and memory consumption are also given compared with that of [mc]square.
Keywords :
finite state machines; formal verification; protocols; security of data; trees (mathematics); ASM-SPV; Helsinki protocol; abstract state machine-security protocol verifier; authentication; computation tree logic; convenient verification method; core ASM language; memory consumption; on-the-fly model checking technique; runtime performance; Authentication; Computational modeling; Cryptography; Memory management; Protocols; Runtime; abstract state machines; formal methods; model checking; security protocols;
Conference_Titel :
Intelligent Information Hiding and Multimedia Signal Processing (IIH-MSP), 2010 Sixth International Conference on
Conference_Location :
Darmstadt
Print_ISBN :
978-1-4244-8378-5
Electronic_ISBN :
978-0-7695-4222-5
DOI :
10.1109/IIHMSP.2010.117
