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.

Key words: network authentication protocol, model checking, Simple Promela Interpreter（SPIN）, modeling simplified strategies, Privacy and Key Management（PKM） protocol

摘要： 为了有效地提高网络认证协议建模和验证的效率，基于模型检测方法提出一个通用的网络认证协议模型描述方法，结合模型检测工具SPIN可以方便地进行性质验证。通过一些模型的简化策略，不仅可以对不同协议进行高效建模，而且减小了模型的状态空间。与现有的文献相比，自动化程度较高，模型验证的效率较好。基于该方法，对PKM认证协议进行了模型检测，实验证明该模型分析验证方法的有效性，可用于其他网络认证协议的分析验证。

关键词: 网络认证协议, 模型检测, 简单进程元语言解释器（SPIN）, 模型简化策略, 密钥管理（PKM）协议