Security Verification of Secure MANET Routing Protocols
AIR FORCE INST OF TECH WRIGHT-PATTERSON AFB OH GRADUATE SCHOOL OF ENGINEERING AND MANAGEMENT
Pagination or Media Count:
Secure mobile ad hoc network MANET routing protocols are not tested thoroughly against their security properties. Previous research focuses on verifying secure, reactive, accumulation-based routing protocols. An improved methodology and framework for secure MANET routing protocol verification is proposed which includes table-based and proactive protocols. The model checker, SPIN, is selected as the core of the secure MANET verification framework. Security is defined by both accuracy and availability a protocol forms accurate routes and these routes are always accurate. The framework enables exhaustive verification of protocols and results in a counter-example if the protocol is deemed insecure. The framework is applied to models of the Optimized Link-State Routing OLSR and Secure OLSR protocol against five attack vectors. These vectors are based on known attacks against each protocol. Vulnerabilities consistent with published findings are automatically revealed. No unknown attacks were found however, future attack vectors may lead to new attacks. The new framework for verifying secure MANET protocols extends verification capabilities to table-based and proactive protocols.
- Computer Systems