Modeling And Research On Formal Analysis Of Security Protocols Based On Strand Space

There are many links in ensuring the security of computer network communication system, the security protocol is a particularly important part of the system. The secure communication between entities in the network is done over a secure protocol to assist. So once the attackers find the vulnerability of the security protocol, they can use it to attack the protocols and achieve their purpose. Because of this, the researchers on the security protocol are also gradually in recent years. As one of the current topics and important research in the field of security, security protocol analysis made a rapid development in the past 20 years. As one of the most important methods of the analysis of security protocols, Formal analysis has great theoretical significance and practical value on security protocol analysis research.The paper depth discussion the theory of strand space in the full understanding of the abstract modeling of security protocols based on the use of concurrent system logic test tool SPIN and its modeling language Promela for modeling security protocols and simulation. The article focuses on the main ideas and methods of using the Promela language modeling security protocols, and describes the basic steps of using model checking tool SPIN to construct and verify the above system model. On this basis, we model and simulate the simple key exchange protocol Diffie-Hellman protocol and establish an efficient model of attacker. It improves that Diffie-Hellman protocol has security vulnerabilities.Using formal analysis of the technology in the analysis of security protocols, we can effectively detect the Diffie-Hellman protocol security vulnerability that exists, and has a higher practicality.