Research On Formal Validation Of Security Of Ad Hoc Network Protocols

Wireless mobile Ad hoc network (MANET, Ad hoc networks for short) is a kind of mobile self-organized networks without fixed infrastructure. Ad hoc networks became a focus in study of networks because they were widely applied to military and civilian fields. Along with the research on security of Ad hoc networks, the routing protocols were rapidly improved and perfected. However network attacks and the infinitely concurrent sessions still led that the protocol design was difficult to achieve its objectives. It was important to validate and analyze the security of protocols. The formal methods had been proved to be the analysis and verification of the effective means of secure protocols. However, the formalization of conventional methods, such as BAN logic proposed by Needham and others, and subsequently improved AT and SVO logic, Perti model, finite state model (FSM) and the random oracle model and so were ideal theoretical state space, theoretical logic was strong, the verification process would take a long step in the reasoning. Intuitive and rigorous to the validation, we introduced the AVISPA tools to validate formally the security of protocols.This thesis was focused on the study of formal validation on Ad hoc networks and its main study was an effective method for formal verification. The main research and innovation of this paper were as follows:(1) Comparing with several common formal methods in advantages and defects, we chose AVISPA tools as the formal validation tools for validating the security of protocols.(2) To verify that is whether or not ARAN protocol could resist the internal malicious attacks which is in discussion of relevant literature, we used the HLPSL language to describe the ARAN protocol and establish an abstract model. Formal verification of ARAN confirmed that the answer is positive, that is to say ARAN can resist the attacks from internal malicious nodes.(3) With network coding technology in the Ad hoc network applications, formal validation on security of network coding became a new research field. For validating the security of the homomorphism signature scheme based on network coding, we built an authenticated network coding transport protocol based on the homomorphism signature algorithm to validate the security of this scheme. Then we used the HLPSL language to establish an abstract authentication model for the network transport protocols and validated the security of this protocol at the first time.