Automating the security analysis process of secure ad hoc routing protocols

Conventional security property evaluation approaches for ad hoc network routing protocols do not provide an automated or exhaustive capability. This paper provides an automated process to evaluate security properties in the route discovery phase for on-demand source routing protocols. For a given network topology, model checking is used to exhaustively evaluate protocol abstractions against an attacker attempting to corrupt the route discovery process. Additionally, topology reduction techniques are developed to reduce computational requirements while maintaining exhaustive analysis results.