Formal Analysis Methods Of Security Protocols Based On Strand Space Model And Its Application

Communication security of computer network is a hot attention, it requires not only the support of the security architecture, technology and engineering, but also the correct security protocol. The design of security protocol is very complex, its defects and possible attacks have been the focus of our discussion. In order to ensure the safety and correctness of the protocol, the formal analysis methods and techniques of protocol can be profound and comprehensive to analysis whether the protocol to meet its security objectives. The formal analysis methods and technique of security protocol is becoming more mature after decades of development. For a long time, the formal analysis method has been proved to be an effective method for the analysis and design of security protocols and weapons. Strand space model (SSM) is a mixed method about combination of theorem proving technologies and protocols traces. Strand space model is the most simple, intuitive, and effective formal analysis methods. Its appearance and studies has caused widespread concern and became a commonly method for formal analysis techniques of protocol.This paper chooses space model theory as the research object, and makes the following discussion and analysis:(1)Based on the principle and theory of the minimal element and ideal of Strand space model, it uses the concept of the ideal and honest to analysis and improve Otway-Rees protocol. The improved Otway-Rees protocol meets its certification and secret.(2) Based on the certification test theory, It analyzes authentication and confidentiality of old x.509protocol. According to the defects of old x.509protocol, it puts forward the corresponding improvement program. And it uses authentication test method to prove that the improved x.509protocol meets its security goal.(3) Formal analysis of the DKNRP protocol, the e-mail protocol has some defects. It proposes a new e-mail protocol, formal analysis of the new e-mail protocol by expanded certification testing and parameter consistency matrix. The new protocol meets the relevant characteristics of e-mail. Finally, related development and application of space model theory is introduced, and the development trend of space model theory is to be discussed. Strand space model theory can analysis protocol easily and intuitively. It provides a certain guarantee to the correctness of the security protocol, thus more conducive to the network security.