Study On Formal Analysis To Security Protocol Based On Strand Space Model

The rapid development of computer networks and network applications has brought great impact to network security, which has become a new hot spot. As an important 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, and many published security protocols were later found that they have a wide range of security vulnerabilities. Security protocol analysis, to ensure security of cryptographic protocols, has become an important research task. Security protocol analysis has two types: formal analysis and non-formal analysis, and the second one is a focus of theoretical research. There are some famous formal analysis methods, such as BAN logic, Kailar logic, SPI calculus, CSP method and Strand space model.The resent research fruit of formal analysis, Strand Space Model (SSM), brought forward by Fabrega, Herzog and Guttman in 1998, is 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 can be used for constructing an attack, revealing the inherent flaws of security protocol. This method has been successfully analyzed the Needham-Schroeder-Lowe protocol, Otway-Rees protocol, Yahalom protocol, and many other protocols, was generally acknowledged to be an advanced and efficient protocol analysis method.This paper mainly focuses the following study on Strand Space Model:(1) Do further study on the basic theory of SSM, and apply it to analyse a two-way authentication protocol proposed by Natalia Miloslavskaya et al., and find some flaws of the protocol on authentication. Based on the analysis result, an improved protocol is proposed.(2)After a study on applying SSM to analyse non-repudiation protocol, we find two problems of previous researchs which focus on fairness analysis by SSM, and give some solutions.Then use SSM to formally describe the specific assumptions of non-repudiation protocol, such as resilient channel, synchronization messages. This work removes the obstacles of protocol analysis. Then an example is given to illustrate how to use space space theory to prove the fairness of the non-repudiation protocol. The correct propositions are the core of the methods. (3) Analyse TEENP protocol and find some flaws of the protocol. Based on the analysis result, a new protocol is proposed. Some flaws of other two non-repudiation protocol is found, which never appear in the old literature.(4) In addition, some ideas about the fairness of non-repudiation protocol and abnormal data processing are discussed.