Modeling and Verifying Ad Hoc Routing Protocols

Modeling and Verifying Ad Hoc Routing Protocols. Mathilde Arnaud, Véronique Cortier, and Stéphanie Delaune. In Proceedings of the 23rd IEEE Computer Security Foundations Symposium (CSF'10), pp. 59–74, IEEE Computer Society Press, Edinburgh, Scotland, UK, July 2010.

Download

[PDF] [HTML]

Abstract

Mobile ad hoc networks consist of mobile wireless devices which autonomously organize their infrastructure. In such networks, a central issue, ensured by routing protocols, is to find a route from one device to another. Those protocols use cryptographic mechanisms in order to prevent malicious nodes from compromising the discovered route.
Our contribution is twofold. We first propose a calculus for modeling and reasoning about security protocols, including in particular secured routing protocols. Our calculus extends standard symbolic models to take into account the characteristics of routing protocols and to model wireless communication in a more accurate way. Our second main contribution is a decision procedure for analyzing routing protocols for any network topology. By using constraint solving techniques, we show that it is possible to automatically discover (in NPTIME) whether there exists a network topology that would allow malicious nodes to mount an attack against the protocol, for a bounded number of sessions. We also provide a decision procedure for detecting attacks in case the network topology is given a priori. We demonstrate the usage and usefulness of our approach by analyzing the protocol \textsfSRP applied to \textsfDSR.

BibTeX

@inproceedings{ACD-routing-CSF10,
  address =       {Edinburgh, Scotland, UK},
  author =        {Arnaud, Mathilde and Cortier, V{\'e}ronique and
                   Delaune, St{\'e}phanie},
  booktitle =     {{P}roceedings of the 23rd {IEEE} {C}omputer
                   {S}ecurity {F}oundations {S}ymposium ({CSF}'10)},
  month =         jul,
  pages =         {59-74},
  publisher =     {{IEEE} Computer Society Press},
  title =         {Modeling and Verifying Ad Hoc Routing Protocols},
  year =          {2010},
  abstract =      {Mobile ad hoc networks consist of mobile wireless
                   devices which autonomously organize their
                   infrastructure. In such networks, a central issue,
                   ensured by routing protocols, is to find a route from
                   one device to another. Those protocols use
                   cryptographic mechanisms in order to prevent
                   malicious nodes from compromising the discovered
                   route.\par Our contribution is twofold. We first
                   propose a calculus for modeling and reasoning about
                   security protocols, including in particular secured
                   routing protocols. Our calculus extends standard
                   symbolic models to take into account the
                   characteristics of routing protocols and to model
                   wireless communication in a more accurate way. Our
                   second main contribution is a decision procedure for
                   analyzing routing protocols for any network topology.
                   By using constraint solving techniques, we show that
                   it is possible to automatically discover (in NPTIME)
                   whether there exists a network topology that would
                   allow malicious nodes to mount an attack against the
                   protocol, for a bounded number of sessions. We also
                   provide a decision procedure for detecting attacks in
                   case the network topology is given a priori. We
                   demonstrate the usage and usefulness of our approach
                   by analyzing the protocol \textsf{SRP} applied
                   to~\textsf{DSR}.},
  doi =           {10.1109/CSF.2010.12},
}