@COMMENT This file was generated by bib2html.pl <https://sourceforge.net/projects/bib2html/> version 0.94
@COMMENT written by Patrick Riley <http://sourceforge.net/users/patstg/>
@techreport{LSV:11:24,
   author = {Arnaud, Mathilde and Cortier, V{\'e}ronique and Delaune, St{\'e}phanie}, 
   institution = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France}, 
   month = dec, 
   note = {68~pages}, 
   number = {LSV-11-24}, 
   type = {Research Report}, 
   title = {Modeling and Verifying Ad Hoc Routing Protocols}, 
   year = {2011}, 
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 
protocols of the literature, such as SRP applied to DSR and SDMSR.
},
}