Modeling and Verifying Ad Hoc Routing Protocol

Modeling and Verifying Ad Hoc Routing Protocol. Mathilde Arnaud, Véronique Cortier, and Stéphanie Delaune. In Preliminary Proceedings of the 4th International Workshop on Security and Rewriting Techniques (SecReT'09), pp. 33–46, Port Jefferson, NY, USA, July 2009.

Download

[PDF]

Abstract

Mobile ad hoc networks consist of mobile wireless devices which autonomously organize their infrastructure. In such a network, 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 a malicious node from compromising the discovered route.
We present 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. Then, by using constraint solving techniques, we propose a decision procedure for analyzing routing protocols for a bounded number of sessions and for a fixed network topology. We demonstrate the usage and usefulness of our approach by analyzing the protocol SRP applied to DSR.

BibTeX

@inproceedings{ACD-secret09,
  address =       {Port Jefferson, NY, USA},
  author =        {Arnaud, Mathilde and Cortier, V{\'e}ronique and
                   Delaune, St{\'e}phanie},
  booktitle =     {{P}reliminary {P}roceedings of the 4th
                   {I}nternational {W}orkshop on {S}ecurity and
                   {R}ewriting {T}echniques ({SecReT}'09)},
  editor =        {Comon-Lundh, Hubert and Meadows, Catherine},
  month =         jul,
  pages =         {33-46},
  title =         {Modeling and Verifying Ad Hoc Routing Protocol},
  year =          {2009},
  abstract =      {Mobile ad hoc networks consist of mobile wireless
                   devices which autonomously organize their
                   infrastructure. In~such a network, 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 a
                   malicious node from compromising the discovered
                   route.\par We present 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. Then,
                   by using constraint solving techniques, we propose a
                   decision procedure for analyzing routing protocols
                   for a bounded number of sessions and for a fixed
                   network topology. We~demonstrate the usage and
                   usefulness of our approach by analyzing the protocol
                   SRP applied to~DSR.},
}