Reserch On Security Protocol Based On Strand Space Theory

With the rapid development of network technology, network security has become an important issue. Security protocol is an important research direction of the information security, it works as a kind of the kernel technology for the secure network communication, thus their security is very crucial to network security. Although the analysis and design of security protocols has developed more than thirty years, it remains many difficulties and challenges for the complexity of security protocol design, the diversity of network attack, and the differences of the running environment.Formal analysis method is the most important tool in security protocol analysis. With the development of security protocol, many kinds of verification model and analysis method have been presented. Although the formal methods have been succeeded in finding flaws and attacks of many security protocols, they still have many limitations, such as the simple structure of the formal method, it cannot analyze some security protocols, and the faultiness of the formal method itself. In the formal method, strand space theory has become the research focus for its compact model, precise definition and efficient proof. It sets off a new upsurge of security protocols formal analysis.Based on strand space theory, we make further study on the analysis and design of authentication protocols, security protocols for wireless network, secure routing protocol for Ad hoc network and the authenticated group key agreement (AGKA) protocols. The main works and results are as follows:We do the research on how to apply the strand space theory to analyze the classic security protocols. Based on strand space theory, Yahalom-Paulson protocol is analyzed. The results of the protocol analysis show that there are authentication flaws in the protocol, and an improved protocol is proposed to avoid the above attacks.CCITTX.509(3) protocol is analyzed using strand space theory, authentication flaws in the protocol have been found, and the attack process of the protocol is presented.We make further study on the analysis and design of authentication protocols. The penetrator's model is extended through adding the behavior of penetrator. The cryptographic primitives are extended. New notion is defined and the relevant propositions or theorems are therefore modified and proved. The extended theory is called extended theory of strand spaces. In order to overcome the defects of sever-specific MAKEP, we propose an improved protocol, Eserver-specific MAKEP. The Eserver-specific MAKEP is analyzed by extended theory of strand space. From the analysis, we are able to conclude that both of the communication parties know each other's true identity and no single party has full control over the selection of the session key.The two-party key agreement protocol in a sensor network using SNEP is analyzed by extended theory of strand space, then one attack had been found in the authentication guarantee property of the protocol:the intruder impersonates the node and creates false requests. An improved protocol to this attack was proposed. The security of improved protocol was analyzed by the extended theory of strand space, where two main security properties were checked:authenticity and confidentiality. And the analysis proves the correctness of the protocol. Confirmed the effectiveness of the extended theory of strand space by analyzing the above protocols, and expanded the scope of application of strand space theory.Make further study on the secure routing protocol for Ad hoc network. In order to analyze the secure routing protocol for Ad hoc network, an extended theory of strand spaces is proposed. In the extended theory of strand spaces, the notions of correctness have modified, and the behavior of penetrator has added. The ARAN protocol is analyzed by the extended theory of strand spaces and two security vulnerabilities are found, that is conspiracy and replay attacks. A new secure routing protocol for Ad hoc network (eARAN protocol) is proposed. The security of eARAN is analyzed by the extended theory of strand spaces, and the analysis proves the correctness of the protocol. The extended theory of strand spaces is proved to be valid by analyzing the above protocols.HTK protocol is analyzed, and found to be vulnerable to the insider attacks. We review the DB protocol and present the flaws of the protocol, then a new scheme is proposed based on DB protocol (EDB protocol). A new analysis method is proposed to analyze the dynamic AGKA protocol based on strand space theory. We analyze procedure AuthKeyAgree, procedure Join and procedure Leave of the EDB protocol, and then the analysis proved the correctness of the EDB protocol. Further expand the scope of application of strand space theory by analyzing the AGKA protocol.