Model Checking of Authentication Protocols
Wei Xu · Chinese Journal of Computers · 2003
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.