Analysing routing protocols: four nodes topologies are sufficient

Analysing routing protocols: four nodes topologies are sufficient. Véronique Cortier, Jan Degrieck, and Stéphanie Delaune. Research Report LSV-11-25, Laboratoire Spécification et Vérification, ENS Cachan, France, 2011. 28 pages.

Download

[PDF]

Abstract

Routing protocols aim at establishing a route between nodes on a network. Secured versions of routing protocols have been proposed in order to provide more guarantees on the resulting routes. Formal methods have proved their usefulness when analysing standard security protocols such as confidentiality or authentication protocols. However, existing results and tools do not apply to routing protocols. This is due in particular to the fact that all possible topologies (infinitely many) have to be considered. In this paper, we propose a simple reduction result: when looking for attacks on properties such as the validity of the route, it is sufficient to consider topologies with only four nodes, resulting in a number of just five distinct topologies to consider. As an application, we analyse the SRP applied to DSR and the SDMSR protocols using the ProVerif tool.

BibTeX

@techreport{LSV:11:25,
   author = {Cortier, V{\'e}ronique and Degrieck, Jan and Delaune, St{\'e}phanie}, 
   institution = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France}, 
   month = dec, 
   note = {28~pages}, 
   number = {LSV-11-25}, 
   type = {Research Report}, 
   title = {Analysing routing protocols: four nodes topologies are sufficient}, 
   year = {2011}, 
abstract = {
Routing protocols aim at establishing a route between nodes on a
network. Secured versions of routing protocols have been proposed in
order to 
provide more guarantees on the resulting routes. 
Formal methods have proved their usefulness when analysing standard security protocols such as confidentiality or authentication protocols.
However, existing results and tools do not apply to routing protocols.
This is due in particular to the fact that all possible topologies
(infinitely many) have to be considered.
In this paper, we propose a simple reduction result: when looking for
attacks on properties such as the validity of the route, it is
sufficient to consider topologies
with only four nodes, resulting in a number of just five distinct
topologies to consider.
As an application, we analyse the SRP applied to DSR and the SDMSR protocols using the ProVerif tool.
},
}