Title :
Some Improvements on Model Checking CoreASM Models of Security Protocols
Author :
Zhao, Zhenju ; Liu, Feng ; Peng, Jianhua ; Huang, Danqing ; Xue, Rui ; Zhang, Zhenfeng
Author_Institution :
State Key Lab. of Inf. Security, Chinese Acad. of Sci., Beijing, China
Abstract :
This paper presents a tool called ASM-SPV (Abstract State Machines-Security Protocols Verifier) for verifying security protocols by model checking. In ASM-SPV, a security protocol is modeled by CoreASM language which is an executable ASM (Abstract State Machines) language. Then a modified CoreASM engine takes the CoreASM model of the protocol to build state space on-demand. Furthermore, security properties of the protocol are described as CTL (Computation Tree Logic) formulas and an adapted model checking algorithm is introduced to check whether the CoreASM model satisfies a given CTL formula or not. In this paper, we show the effectiveness of ASM-SPV with regard to memory consumption and speed of generating states compared with another CoreASM based model checker [mc]square.
Keywords :
finite state machines; formal verification; multiprocessing systems; security of data; ASM-SPV; CTL; abstract state machines; abstract state machines security protocols verifier; adapted model checking algorithm; computation tree logic; memory consumption; model checking CoreASM models; Adaptation model; Arrays; Computational modeling; Engines; Memory management; Protocols; Security; ASM; CoreASM; model checking; security protocols;
Conference_Titel :
Data, Privacy and E-Commerce (ISDPE), 2010 Second International Symposium on
Conference_Location :
Buffalo, NY
Print_ISBN :
978-1-4244-8377-8
Electronic_ISBN :
978-0-7695-4203-4
DOI :
10.1109/ISDPE.2010.17
