Attack-ability Analysis of Wireless Network Routing Protocols

Abstract

This paper takes a specific routing protocol as an example and formally analyzes the protocol in a machine-assisted theorem proving tool Isabelle/HOL, to prove that routing protocols in wireless networks can be attacked by designing particular attacking schemes and can also be protected from attacks by modifying protocol contents. The paper first gives the specification of the routing protocol and formal definition of the attacker, and then finds the security vulnerability in the routing protocol through strict logical analysis.