计算机工程与应用2012，Vol.48Issue(21)：62-67,6.DOI:10.3778/j.issn.1002-8331.2012.21.014
基于SPIN的网络认证协议高效模型检测
Effective model checking of network authentication protocol based on SPIN
摘要
Abstract
In order to improve the efficiency of modeling and verification on network authentication protocols with the model checking, this paper proposes a universal formalization description method of the network authentication protocol. Combined with model checking tool SPIN, the method can expediently verify the properties of the protocol. By some modeling simplified strategies, several protocols can be modeled efficiently, and the state space of the model is reduced. Compared with the previous literature, this paper achieves higher degree of automation, and better efficiency of model verification. Based on the method described in this paper, the PKM authentication protocol is modeled and verified. The experimental results show that the method of model checking is effective, which is useful for the other authentication protocols.关键词
网络认证协议/模型检测/简单进程元语言解释器(SPIN)/模型简化策略/密钥管理(PKM)协议Key words
network authentication protocol/ model checking/ Simple Promela Interpreter (SPIN)/ modeling simplified strategies/ Privacy and Key Management(PKM) protocol分类
信息技术与安全科学引用本文复制引用
缪力,谭志华,张大方..基于SPIN的网络认证协议高效模型检测[J].计算机工程与应用,2012,48(21):62-67,6.基金项目
中央高校基本科研业务费资助. （）
