Analysis And Verification Of Security Protocol Based On Strand Space

Security protocols which play an important part in network communication between entities is the basis of network security.However, As the network environment is complex and the defects of security protocols, attacker could hand these vulnerabilities to carry out a variety of attacks on security protocols to meet the purpose of damaging network security. Therefore, analyzing security protocols reasonable and correctly plays an increasingly important role in the network security.Formal analysis method is one of the most important method of security protocol analysis.Proposing the authentication test method and automated analysis method of security protocol Athena is the two most important events in the development of strand space model,this paper based on having made an intensive. study of analysis and verification methods of security protocol has mainly done the following work and innovation:First of all, I have made intensive study and exploration of strand space method of security protocol analysis basing on in-depth understanding of protocol analysis method, so I could analyze and verify security protocol with strand space model of formal analysis method.Secondly,I have mastered of the authentication test method of security protocol analysis, and I have improved the original authentication test method by overcoming its shortcomings so as to expand the scope of its analysis. What's more, TLS protocol has been analyzed with the improved authentication test method and the analysis result proves the effectiveness of the improved method.Thirdly, This paper has proposed an automated analysis method of security protocol and it's corresponding model has also been designed, above all, a series of algorithms that the core of the method were put forward ro achieve the model. And presented the process and characteristic of its protocol analysis.The last but the most important of all, the basic function of the model was achieved by experiments, and using the model analyzed the original and improved Helsinki protocol to prove accuracy and efficient of the proposed method. Automated analysis method of security protocol is a forward direction in the field of formal analysis, the automated analysis method that was proposed in this paper overcomes the disadvantage of manual analysis of security protocol, so it makes the process of security protocol analysis more simple and intuitive, and improves the efficiency of security protocol analysis.