Formal analysis of privacy for routing protocols in mobile ad hoc networks

Rémy Chrétien and Stéphanie Delaune. Formal analysis of privacy for routing protocols in mobile ad hoc networks. In Proceedings of the 2nd International Conference on Principles of Security and Trust (POST'13), pp. 1–20, Lecture Notes in Computer Science 7796, Springer, Rome, Italy, March 2013.

Download

[PDF] 

Abstract

Routing protocols aim at establishing a route between distant nodes in ad hoc networks. Secured versions of routing protocols have been proposed to provide more guarantees on the resulting routes, and some of them have been designed to protect the privacy of the users. In this paper, we propose a framework for analysing privacy-type properties for routing protocols. We use a variant of the applied-pi calculus as our basic modelling formalism. More precisely, using the notion of equivalence between traces, we formalise three security properties related to privacy, namely indistinguishability, unlinkability, and anonymity. We study the relationship between these definitions and we illustrate them using two versions of the ANODR routing protocol.

BibTeX

@inproceedings{CD-post13,
  abstract =      {Routing protocols aim at establishing a route between
                   distant nodes in ad hoc networks. Secured versions of
                   routing protocols have been proposed to provide more
                   guarantees on the resulting routes, and some of them
                   have been designed to protect the privacy of the
                   users. In this paper, we propose a framework for
                   analysing privacy-type properties for routing
                   protocols. We use a variant of the applied-pi
                   calculus as our basic modelling formalism. More
                   precisely, using the notion of equivalence between
                   traces, we formalise three security properties
                   related to privacy, namely indistinguishability,
                   unlinkability, and anonymity. We study the
                   relationship between these definitions and we
                   illustrate them using two versions of the ANODR
                   routing protocol.},
  address =       {Rome, Italy},
  author =        {Chr{\'e}tien, R{\'e}my and Delaune, St{\'e}phanie},
  booktitle =     {{P}roceedings of the 2nd {I}nternational {C}onference
                   on {P}rinciples of {S}ecurity and {T}rust
                   ({POST}'13)},
  OPTDOI =           {10.1007/978-3-642-36830-1_1},
  editor =        {Basin, David and Mitchell, John},
  month =         mar,
  pages =         {1-20},
  publisher =     {Springer},
  series =        {Lecture Notes in Computer Science},
  title =         {Formal analysis of privacy for routing protocols in
                   mobile ad~hoc networks},
  volume =        {7796},
  year =          {2013},
  acronym =       {{POST}'13},
  nmonth =        {3},
  OPTLONGPDF =       {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/
                  rr-lsv-2012-21.pdf},
  lsv-category =  {intc},
  wwwpublic =     {public and ccsb},
}