The Research Of Effective Model Checking For Network Authentication Protocol

The major role of the network authentication protocol is to verify the identity of communication entity and distribute the session key for the entity. In the open, distributed and complex network environment, the network authentication protocol may have some hidden defects, which is difficult to find by the testing method. Because of the verifiability, accuracy and unambiguity, formal methods can effectively verify the security properties of the authentication protocol. Theorem proving, model checking and modal logic are the current commonly used formal analysis methods.Model checking, as one of the formal methods has many good advantages, such as automatism and providing the counterexample. Model checking method can effectively reduce the security protocol design errors, there are many model checking tools have been successfully used in security protocols analysis. The existing modeling method is short of universal due to its poor readability, low automatization and verification efficiency, and less efficient verification. Based on the famous model checker SPIN, we are committed to providing an efficient framework of model checing about the authentication protocol.Against the state explosion problem in model checing, this paper analyzes the partial order reduction algorithm and the state compression technology, and through comparison of experimental results to illustrate the impact of which on the efficiency verification.And we study the model optimization methods such as reducing the variable definitions and the introduction of atomic statements etc, in using Promela language to describe the model. Experiments show that such optimizations are able to reduce the number of states.In order to effectively improve the efficiency of the network authentication protocol modeling, based on the actual network environment, the operating characteristics of authentication protocol, this paper presents a general description approach of network authentication protocol model. This paper describes the protocol as a collection of entities based on the sequence of events and builds the attacker model through the information analysis and information synthesis. The protocol model can be easily described by using Promela language. This paper presents some reduction strategies about the protocol model in order to solve the state explosion of the model. These strategies can effectively reduce the state space of the model. Compared with the existing literatures, this paper achieves higher degree of automation, and better efficiency of verification.Finally, based on the model checking method in this paper, we model and verify the authentication protocols such as PKM, Ban-Yahalom, TMN, and find the flaws of the protocols. And the experimental results show that the method of model checking is effective, which is useful for the other authentication protocols.