身份认证协议的模型检测分析

提出一个直观、易用的模型来模拟和验证身份认证协议，并给出基于Spin(模型检测工具）的实现，它不仅可以模拟多对参与者同时进行会话，而且还有效缩减了状态空间，从而避免了以前文献中提到的状态爆炸现象，同时该文用Needham-Schroeder公钥协议和TMN协议来说明如何应用该模型。

Model Checking of Authentication Protocols

The increasing popularity of distributed systems and the emergence of new technologies, such as electronic commerce, demand new security solutions. The corresponding cornerstone of security is often authentication, therefore easy to use methods and tools for modeling and verification of authentication are needed. This paper develops a way of verifying authentication protocols using model checking. Model checking has been proven to be a very useful technique for verifying hardware designs. By modeling circuits as finite-state machines, and exploring all possible execution traces, model checking can find a number of errors in real world designs. Like hardware designs, authentication protocols are very subtle, and can also have bugs which are difficult to find. Specially, this paper presents a simpler model for modeling and verifing authentication protocols, which not only adapts to the situation with multi-pairs of participants but also efficiently reduces the sizes of the state space and avoids states explosion problem mentioned in previous literatures. Also this paper implements the model using Model Checker Spin. Needham-Schroeder Public Key protocol and TMN protocol examples are illustrated to show how this framework is applied.