Research On Automaitc Analysis Of Security Protocols Based On Strand Space Model

With the fast development of network communication and information technology, network has exised in various fields. And network security problem is increasingly serious; whose reason is its circumstances is an open secret that can be easily modified, forged and replayed. So how to solve the network security problem has been the increasingly outstanding problem.Security protocol, called cryptographic protocol which seems especially important in safety and reliability, is a protocol for various types of security service over an insecure network. Before it is put into use, taking the openness of environmet and the imperfection of structrue into account, the attacker may execute effective attacks with the aid of shortcomings, therefore it is important for us to validate its correctness.So far, it has became a hotspot and important area in security protocols to give formal analysis and automatic detection, correspondingly, designing efficient and reliable tools for analyzing security protocols has been the dominant trend.Based on strand space model, this paper makes a research on some kinds of formal analysis and automatic analysis in security protocols nowadays, especially focus on the analysis of security protocols using automatic mehod. Following are the main results of this paper:1) This paper makes a deep study on security protocols, and focusing on the current formal analysis method boardly-strand space model, we mainly studies the analysis of NSL protocol process by whose construction method. At the same time, this paper also further studies the authentication process and puts forward the SSM protocol.2) This paper proposes a new automatic analysis method based on strand space model.Aming at the problem that not checking the source of information and only accepting it as a subset, the paper proposes an automatic method, which supports the string matching through structure the strings of identical construction, and it not only can analyze the two-party protocols but also makes it use three-side indentication protocols.lastly; it illuminates the structure of the tool, and implements technology with the aid of two agreements. All the whole process has majour or theoretic value and wideranging application.