Security Properties Analysis of Routing Protocol for MANET

Secure protocol is the foundation of the MANET. It is very critical to ensure the correctness of the security properties in the designed routing protocols. However, nowadays, new designed protocols are predominantly validated by an interpretation of simulation methods, lacking rigid formal analysis to ensure security properties. Firstly, this paper presents a formal analysis procedure of SRP routing protocols in the context of attack model which is suitable to the MANET and gives the denotational semantics and abstract interpretation model. Secondly, we propose an attack model which fits for the open traits of MANET. Thirdly, we give a detailed analysis procedure of SRP protocol in our attach model. Finally, we test and demonstrate our idea by the SPRITE tool based on Spi calculus.