Analysing routing protocols: four nodes topologies are sufficient

Véronique Cortier, Jan Degrieck, and Stéphanie Delaune. Analysing routing protocols: four nodes topologies are sufficient. In Proceedings of the 1st International Conference on Principles of Security and Trust (POST'12), pp. 30–50, Lecture Notes in Computer Science 7215, Springer, Tallinn, Estonia, March 2012.

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

@inproceedings{CDD-post12,
  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.\par 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.},
  address =       {Tallinn, Estonia},
  author =        {Cortier, V{\'e}ronique and Degrieck, Jan and
                   Delaune, St{\'e}phanie},
  booktitle =     {{P}roceedings of the 1st {I}nternational {C}onference
                   on {P}rinciples of {S}ecurity and {T}rust
                   ({POST}'12)},
  OPTDOI =           {10.1007/978-3-642-28641-4_3},
  editor =        {Degano, Pierpaolo and Guttman, Joshua D.},
  month =         mar,
  pages =         {30-50},
  publisher =     {Springer},
  series =        {Lecture Notes in Computer Science},
  title =         {Analysing routing protocols: four nodes topologies
                   are sufficient},
  volume =        {7215},
  year =          {2012},
  acronym =       {{POST}'12},
  nmonth =        {3},
  OPTLONGPDF =       {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/
                  rr-lsv-2011-25.pdf},
  lsv-category =  {intc},
  wwwpublic =     {public and ccsb},
}