Study On Security Analysis Techniques In Routing Protocols For Mobile Ad Hoc Networks

Mobile ad hoc networks(MANET) are currently a very active area of the academic and industrial research for its foreseeable broad applications. However, MANET is vulnerable to a wide range of attacks. Especially, routing is one of the most basic networking functions in mobile ad hoc networks. Hence, an adversary can easily paralyze the operation of the network by attacking the routing protocol. Many “secure” routing protocols have been proposed for ad hoc networks in recent years. The security of these routing protocols in MANET is usually analyzed by informal means such as visual inspection and network simulation. Therefore, many “secure” protocols are later found to have flaws.Recently, there have been attempts to develop formal means to prove routing protocols secure. This dissertation studies the current analysis techniques being used to evaluate security properties in MANET routing protocols, especially the simulation-based approaches and the formal analysis techniques which have automatic analysis capabilities. The relevant work is supported by the Key Program of National Natural Science Foundation of China(NO.U1135002).The first part focuses on the ABV model based on simulation paradigm, which is a formal model tailored to the security analysis of on-demand source routing protocols in MANET. In the ABV model, since adjacent adversarial nodes can communicate with each other in an unrestricted manner, they can appear as a single node to the other nodes. Hence, these adversarial nodes are not neighbors in G; if they were, they are merged into a single adversarial vertex that would inherit all the neighbors of the original nodes. So, the ability of these adversarial vertices is restricted in G, which are not neighbors and cannot communicate by out-of-band channels. The mergence of these adversarial nodes makes the security proof for endair A easier, and obviates the key question to be resolved in the ABV model. It is improper to exclude the wormhole attack. In fact, the definition of G in the model tolerates the wormhole attack. So the mergence of the adversarial nodes in G weakens the analysis ability of the ABV model and a provably secure protocol in the model is vulnerable to the wormhole attack. The ABV model assumes that the adversary has compromised some identifiers, which means that it hascompromised the cryptographic keys that are used to authenticate those identifiers. Thus, the adversary can appear as an honest participant under any of these compromised identities. However, the secure route is defined as plausible route, which perhaps only exists in G and does not almost exist in the actual network for the emergence of the adversarial nodes. So the definition of the plausible route is improper, which obviates the case that an adversarial vertex has several identifiers, and excludes the Sybil attack. In fact, the definition of the plausible route tolerates the Sybil attack. So the definition of the plausible route in the ABV model weakens the analysis ability of the model and a provably secure protocol in the model is vulnerable to the Sybil attack.We presents an attack to endair A, which leads endair A to accept a route that is not plausible. So provably secure route protocols such as endair A in the ABV model are vulnerable to some hidden channel attacks.The second part focuses on the extended ABV model, which is a formal model tailored to the security analysis of on-demand distance vector routing protocols in MANET. In the extended ABV model, we find that the mergence of the adversarial nodes in G weakens the analysis ability of the extended ABV model and a provably secure protocol in the model is vulnerable to the wormhole attack. The definition of the correct system state in the extended ABV model weakens the analysis ability of the model and a provably secure protocol in the model is vulnerable to the Sybil attack. Provably secure ARAN in the extended ABV model has flaws, which will lead to incorrect entry in the routing table of a normal node.Finally, we develop an automated evaluation process to analyze security properties in the route discovery phase for on-demand source routing protocols, such as SRP, Ariadne and endair A. Using the automated security evaluation process, we are able to produce and analyze all topologies for a given network size. The individual network topologies are fed into the SPIN model checker to exhaustively evaluate protocol models against an attacker attempting to corrupt the route discovery process.