Extension And Application Of Formal Verification Methods Based On Strand Space Model

Security protocol is the basis for achieving information security, is the core technology of network security Communication, Its correctness plays an important role in the network security, Therefore, the safety of their own has become an important part of security research. But how to ensure the safety of security protocols, how to design a protocol to make it meet the safety requirements, are issues need to continue to explore in security protocols research areas. In order to analyze the security of security protocols, the researchers propose a formal analysis, and use these methods found many shortcomings and attack methods of many protocols, Formal analysis provides a great help to the design and analysis of security protocols. However, the security protocols adds many new cryptographic operations for security considerations, and some formal methods have not define these operations, so it can not be used to analyze these security protocols. Therefore, this article These issues study these problems in-depth bases on strand space model, honest vision and authentication tests, obtains some results. The main research as follows:First, this article makes a thorough study in the strand space model, honest vision and authentication tests in the classic analysis of security protocols, and finds security flaws and attacks on these protocols through formal analysis of these agreements , gives the corresponding attack and specific improvements on these protocols based on the results .Secondly, we find the strand space model, honest vision and authentication tests can not be effectively analyzed these security protocol which join the signature algorithm and hash operations. So we extend the strand space model, honest vision and certification testing methods. We extend free hypothesis, child relationships, and the intruder model in the strand apace, definitions and theorem of honest ideal. We extends test weight, the conversion side, is converted to side, output test, input test and active testing.Finally, we verify the integrity of the expanded vision and the accuracy of authentication test through analysis an e-mail transmission protocol.