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

fYear

2010

fDate

15-17 Oct. 2010

Firstpage

458

Lastpage

461

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;

fLanguage

English

Publisher

ieee

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

Type

conf

DOI

10.1109/IIHMSP.2010.117

Filename

5636276