ASM-SPV: A Model Checker for Security Protocols
Jianhua Peng, Feng Liu, Zhenju Zhao, Danqing Huang, Rui Xue · 2010
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.