Research And Application On Formal Analysis Of Security Protocol Of Mobile Ad Hoc Network

With the wide application of computer networks, people are becoming more dependent on the network, while network security has become increasingly important. Especially in recent years, emerging mobile Ad Hoc networks rapidly develop. Because of more open network architecture and transmission media, in the coverage of network any one can send or receive messages. Its network security will face more serious threats. Security environment of Mobile Ad Hoc networks is based on secure routing protocol. Secure routing protocol security the security of the entire network environment plays a vital role. Routing protocol design and analysis of security has become a very important research topic and a challenging task. Because traditional network security technologies can not be directly applied to the mobile Ad Hoc networks and secure routing look secure, but may contain exploit subtle flaws and weaknesses of attack. A large number of facts show that, many secure routing protocols, even after careful analysis and design security experts, still have a lot of loopholes. To ensure the safety of secure routing protocols, the researchers made use of formal analysis methods to guide mobile Ad Hoc network routing protocol design and analysis. Among them, the strand space model is a typical method of formal analysis to design and analysis of security protocols has brought great changes, this article through the strand space model to solve the mobile Ad Hoc network security routing protocol security problem.Firstly this dissertation described the security protocols and formal analysis methods, after the dissertation focuses on formal analysis of the strand space model. By an in-depth analysis of research and extension of strand space model and using a simple application example, the advantages of strand space model: simple, clear, and effective. Finally, the safety of mobile Ad Hoc network routing protocol and its formal analysis methods were analyzed. By the attacking examples of existing mobile Ad Hoc network security DSR Routing Protocol (SRP routing protocol and Ariadne routing protocol security) security loopholes, the dissertation propose a new secure DSR routing protocol model-Ariadne-S model, and use the strand space model to analyze the security proof.