Mathilde Arnaud, Véronique Cortier, and Stéphanie Delaune. Modeling and Verifying Ad Hoc Routing Protocol. In Preliminary Proceedings of the 4th International Workshop on Security and Rewriting Techniques (SecReT'09), pp. 33–46, Port Jefferson, New York, USA, July 2009.
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.
@inproceedings{ACD-secret09,
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.},
address = {Port Jefferson, New~York, 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},
acronym = {{SecReT}'09},
nmonth = {7},
lsv-category = {autc},
wwwpublic = {public and ccsb},
}