Formal security evaluation of ad hoc routing protocols

Research into routing protocol development for mobile ad hoc networks has been a significant undertaking since the late 1990's. Secure routing protocols for mobile ad hoc networks provide the necessary functionality for proper network operation. If the underlying routing protocol cannot be trusted to follow the protocol operations, additional trust layers cannot be obtained. For instance, authentication between nodes is meaningless without a trusted underlying route.; Security analysis procedures to formally evaluate these developing protocols have been significantly lagging, resulting in unstructured security analysis approaches and numerous secure ad hoc routing protocols that can easily be broken. Evaluation techniques to analyze security properties in ad hoc routing protocols generally rely on manual, non-exhaustive approaches. Nonexhaustive analysis techniques may conclude a protocol is secure, while in reality the protocol may contain unapparent or subtle flaws. Using formalized exhaustive evaluation techniques to analyze security properties increases protocol confidence.; Intertwined to the security evaluation process is the threat model chosen to form the analysis. Threat models drive analysis capabilities, affecting how we evaluate trust. Current attacker threat models limit the results obtained during protocol security analysis over ad hoc routing protocols. Developing a proper threat model to evaluate security properties in mobile ad hoc routing protocols presents a significant challenge. If the attacker strength is too weak, we miss vital security flaws. If the attacker strength is too strong, we cannot identify the minimum required attacker capabilities needed to break the routing protocol.; To solve these problems, we contribute to the field in the following ways: Adaptive Threat Modeling. We develop an adaptive threat model to evaluate route discovery attacks against ad hoc routing protocols. Adaptive threat modeling enables us to evaluate trust in the ad hoc routing process and allows us to identify minimum requirements an attacker needs to break a given routing protocol. Automated Security Evaluation. We develop an automated evaluation process to analyze security properties in the route discovery phase for on-demand source routing protocols. 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.; Our contributions provide the first automated exhaustive analysis approach to evaluate ad hoc on-demand source routing protocols.