Formal Analysis of Privacy for Vehicular Mix-Zones (bibtex)
by Morten Dahl, Stéphanie Delaune, Graham Steel
Abstract:
Safety critical applications for recently proposed vehicle to vehicle ad-hoc networks (VANETs) rely on a beacon signal, which poses a threat to privacy since it could allow a vehicle to be tracked. Mix-zones, where vehicles encrypt their transmissions and then change their identifiers, have been proposed as a solution to this problem. \par In this work, we describe a formal analysis of mix-zones. We model a mix-zone and propose a formal definition of privacy for such a zone. We give a set of necessary conditions for any mix-zone protocol to preserve privacy. We analyse, using the tool ProVerif, a particular proposal for key distribution in mix-zones, the CMIX protocol. We report attacks on privacy and we propose a fix.
Reference:
Formal Analysis of Privacy for Vehicular Mix-Zones (Morten Dahl, Stéphanie Delaune, Graham Steel), In Proceedings of the 15th European Symposium on Research in Computer Security (ESORICS'10) (Dimitris Gritzalis, Bart Preneel, eds.), Springer, volume 6345, 2010.
Bibtex Entry:
@inproceedings{DDS-esorics10,
  abstract =      {Safety critical applications for recently proposed
                   vehicle to vehicle ad-hoc networks~(VANETs) rely on a
                   beacon signal, which poses a threat to privacy since
                   it could allow a vehicle to be tracked. Mix-zones,
                   where vehicles encrypt their transmissions and then
                   change their identifiers, have been proposed as a
                   solution to this problem. \par In this work,
                   we~describe a formal analysis of mix-zones. We~model
                   a mix-zone and propose a formal definition of privacy
                   for such a zone. We~give a set of necessary
                   conditions for any mix-zone protocol to preserve
                   privacy. We~analyse, using the tool ProVerif,
                   a~particular proposal for key distribution in
                   mix-zones, the CMIX protocol. We~report attacks on
                   privacy and we propose a fix.},
  address =       {Athens, Greece},
  author =        {Dahl, Morten and Delaune, St{\'e}phanie and
                   Steel, Graham},
  booktitle =     {{P}roceedings of the 15th {E}uropean {S}ymposium on
                   {R}esearch in {C}omputer {S}ecurity ({ESORICS}'10)},
  DOI =           {10.1007/978-3-642-15497-3_4},
  editor =        {Gritzalis, Dimitris and Preneel, Bart},
  month =         sep,
  pages =         {55-70},
  publisher =     {Springer},
  series =        {Lecture Notes in Computer Science},
  title =         {Formal Analysis of Privacy for Vehicular Mix-Zones},
  volume =        {6345},
  year =          {2010},
  acronym =       {{ESORICS}'10},
  nmonth =        {9},
  url =           {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DDS-esorics10.pdf},
  PDF =           {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DDS-esorics10.pdf},
  PS =            {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DDS-esorics10.ps},
  lsv-category =  {intc},
  wwwpublic =     {public and ccsb},
}
Powered by bibtexbrowser