Research On Formal Analysis Methods Of Authentication Protocols Based On Strand Space Model

The rapid development of computer networks and network applications is bring about great challenges to network security. Therefore, the network security has become the new focus of information security. As a vital component of the network security architecture, security protocol is becoming increasingly important. However, due to the complexity of the security protocol, designing a perfect security protocol is very difficult. A wide range of security vulnerabilities have been found in many published security protocols, which makes the security protocol analysis aiming at ensuring correctness become an important research area. Security protocol analysis has two methods: formal analysis method and non-formal analysis method, of which the first one is a focus of theoretical research. The commonly used methods of formal analysis includes: BAN logic, Kailar logic, SPI calculus, CSP method and Strand space model.Strand Space Model (SSM), created by Fabrega, Herzog and Guttman in 1998, is the newest research fruit in the area of security protocol analysis that is highly efficient, intuitive and practical for formal analysis of security protocol. It not only can be used to prove the correctness of security protocols, but also be used for constructing an attack to reveal the inherent flaws of security protocol. This method has been successfully adopted to analyze the Needham-Schroeder-Lowe protocol, Otway-Rees protocol, Yahalom protocol, as well as many other protocols and been generally regarded as an advanced and highly efficient protocol analysis method.This paper briefly introduces the basic concept and theory of strand space, analyzes three branches of strand space in detail, not only their theory but also how to apply them to analyze protocols in practice. Also, the traits and advantages of strand space are demonstrated.Firstly, by virtue of strand space, we analyze the IEEE 802.11i protocol which is extensively used to Wireless Local Area Networks(WLAN). By modeling protocols with strand space, we give a detailed analysis on corresponding protocols. We use the Idea and Honest method to prove the secret property of the protocol and the authentication protocol of the protocol.Secondly, after a study on applying SSM(strand space model) to analyze repeated authentication protocol, we find the previous study of the repeated authentication protocol divide the repeated authentication protocol into some independent sub-protocol. To solve this problem, we extend the theory of strand space. We propose a new casual relation between sub-protocols, redefine the definition of strand space and buddle, and propose two new properties that are repeated authentication agreement and reapeated security.Lastly, we analyze the Kao Chow repeated authentication protocol by the extended strand space model. We use the Idea and Honest method to prove the security property of the protocol and the authentication protocol of the protocol.