Modeling vulnerabilities of ad hoc routing protocols

The purpose of this work is to automate the analysis of ad hoc routing protocols in the presence of attackers. To this end, a formal model of protocol behavior is developed in which time is modeled by a set of constraints on the time of occurrence of events, enabling the representation of partially ordered timed events and asynchronous communication. Data variables are represented symbolically, capturing a range of distinct executions in each expression. Given a formal description of Ad Hoc On Demand Distance Vector Routing Algorithm (AODV) and a desired safety property (route stability), an analysis by a naive semi-decision procedure discovers an instance of an attack that leads to a violation of the property. Categories and Subject Descriptors C.2.2 [Computer Systems Organization]: ComputerCommunication NetworksNetwork Protocols[protocol verication, routing protocols] General Terms Ad Formal Verication, Ad hoc Wireless Networks, Security

• Type: Conference
• Year: 2003
• Where: SASN
• Authors: Shahan Yang, John S. Baras
• Keywords: Ad Hoc, Hoc Routing Protocols, Routing Protocols, SASN 2003