Formal Analysis And Research On Methods Of Security Protocol Based On Strand Space

With the rapid development of network and information exchange volume of the growing, the problem information security has been more and more attention. The information in uncertain network environment are attacked, greatly damage the interests of users, to some key security departments have posed a serious threat. With the rapid development of network and information exchange volume of the growing, the problem information security is more and more attention. In order to maintain the safety of network environment, people use password techniques and security protocols, and security protocol is the basis of information security, the property of their safety has now become a key issue. After nearly30years of research, formalized method become security protocols of the most important one of the tool. In1998, Thayer, Herzog and Guttmann put forward the strand space model; the strand space model is a intuitive and rigorous formalization analysis method. The strand space model introduced into the causal relationship between the partial order relations, so as to cut the state space of the analysis of protocol, avoid the state space explosion. In1999, Song design automation protocol verification tools Athena, used mainly reverse search technology to generate and traverse all able to generate the target state, while reducing the state space search. Although Athena to a certain extent reduce the number of traversal state, but still can not solve the protocol state scale series increased. In this paper, improvement and innovation for more than three points.The paper first introduce the security protocol on the background and current development status, as well as the strand space model of the basic concept, the original strand space model based on only considered poor password the original language, it can not description and analysis of the password security protocol,such as hash function and sign. In order to solve this problem, this paper proposes a kind of extension of the strand space model. First message term, the in-term relation and penetrator model in the strand space model are extended. Secondly in the strand space model based on the introduction of authentication the theory of authentication test three authentication test method and corresponding certification test rules to Needham-Schroeder public key protocol as an example, the application of the relevant theories. And redefined a transforming edge and an outgoing test, and prove the correctness of the theory, using the improved protocol Wide-Mouth Frog Protocol to verify its validity. Finally, we achieve the verification of authentication test method of safety test algorithm. The algorithm is proved, and the algorithm is able to meet the security attributes, using the partial ordering of node in the strand space model and certification test methods can effectively reduce the number of state space generation, and to avoid state space explosion problem in the protocol verification process verified by experiments.