On Technology Of Model Checking Security Protocols

At the present time, following the inundant developing of computer network and compunication, the importance of security protocols becomes more and more evident. Security protocols take charge of distributing keys and authenticating identity. Once there is a flaw in a security protocol itself, the security of communication would face danger. The method of model checking has shown its advantage in the verification of security protocols.The object of this paper is to verify security protocols with model checking tools. We research different kinds of formal methods, particularly study the mechanism of symbolic model checking tool SMV, and finally we decide to adopt SMV as the tool for the model checking of security protocols. With SMV, we model check the authentication version of Needham-Schroeder public key protocol and Woo and Lam IJ symmetric key protocol.During the modeling and verification of the authentication version of Needham-Schroeder public key protocol with SMV, we get more comprehension on the theory of symbolic model checking and small system model, and finally find a flaw in this protocol that corresponds with the one that Gavin Lowe found with FDR.In order to break through the limitation of small system model, for the verification of Woo and Lam U symmetric key protocol with SMV, a model is built up. An honest agent in the model is allowed to participate in two protocols. Finally a flaw is found that an intruder can successfully commit an attack when the responder is allowed to participate in two protocols simultaneously.While modeling and verifying security protocols with SMV, we find a bug of SMV and some other problems, which are ignored by the authors in the handbook of SMV.First, this paper introduces the notation, categories and properties of security protocols, and formal methods to verify security protocols and small system model. The emphasis is the research and analysis of the principle of the model checking method. We study the mechanism and syntax of symbolic model checking tool SMV, model check the authentication version of Needham-Schroeder public key protocol and Woo and Lam IJ symmetric key protocol. Flaws are found in both cases.