Salle seminaire CE4
22 November 2011 - 14h00
Formal verification of secure routing protocols
by Mathilde Arnaud from LSV
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.
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.
We then give decision procedures for analyzing routing protocols. 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.
Slides of the Presentation.
ATTENTION : Changement de lieu, le séminaire sera au centre equation 4 salle dans la nouvelle salle de séminaire. Entrée par Verimag historique
