Spi-based Calculus Of Mobile Autonomous Network Security Routing Protocol Analysis

In the mobile ad hoc network (MANET) protocol's research is one of the most important main domain. Comparing between the nature of the Manet and traditional wired network has formed many new challenge, the most existed routing protocols are resource-centralized protocols that don't suit in the trait of mobile ad hoc network. In view the characteristic of the mobile ad hoc , applied different methods to solve the routing protocol have been proposed, the security route protocols also are been studying and been proposing , IETF(Internet Engineer Task Force) has established a MANET work team to accomplish this goal. The analysis of the security routing protocols is a complex question and whether the security routing protocol satisfies the security goals or not will directly affect the mobile ad hoc network promotion and the application. In the early phrase of designing the security route protocols if there are no corresponding method to examine the security objects of the security routing protocol, the latent flaw has no appropriate method to detection , then the network operation is very easily attacked and cannot work at the same time it will be create many nonessential wastes. In view of this goal, there have had many inferences methods to apply in the security route protocol analysis at present, but these methods are mostly simulative method as well as the logical inference and the state space search, These methods are mostly using the finite states the point to analysis and draw the conclusion. Applying these methods obtain the results at least can't satisfy the below two goals:(l) There is no clear (meaning formal) definition of the term "secure routing". Therefore, different authors interpret security in different ways, and design their routing protocols with different requirements in mind. As a consequence, the properties of different proposals are difficult to compare(2) There is no mathematically rigorous way to prove a proposed routing protocol secure. In fact, many of the proposed protocols (e.g., SRP andKerberos) are flawed in the sense that they do not achieve the properties claimed by their authors;a clear consequence of the lack of a sound proof technique.Method of formal analysis security routing protocols very few and the applied advancement algebra method are less. The application advancement algebra method to analysis security performance of security route protocols overcomes the non- formal the nonessential artificial intervention and the experience infers, strictly according to mathematics syntax, the semantics realizes the security goal analysis.In this thesis, the author refers the SPI calculus to analysis the MANET routing protocols, Spi calculus, an extension of the pi calculus designed for the description and analysis of cryptographic protocols. It can provide a precise and solid basic for reasoning about protocols, other notations such as BAN are more formal, but there relation to implementation may be more tenuous or subtle. The Spi calculus is a middle ground: it is directly executable and it has a precise semantics..We apply Spi calculus to concrete analysis SRP routing protocol, in the attack model that the author refers and the associate security goals, the SRP routing protocol expose some vulnerability and analysis the cause of the vulnerability, Pointing out in the designing of SRP protocol some assumes are improper, discovering its modifying methods.To illustrate the convenience and efficiency of the Spi calculus to analysis security protocols, we take the famous Kerberos protocol as the example to simple described and analysis to enlarge the extending and at the same time pointing the designing flaws of this famous authentication protocol.At last, we give the conclusion of this thesis and the future work direction and research objection.