Morten Dahl, Stéphanie Delaune, and Graham Steel. Formal Analysis of Privacy for Vehicular Mix-Zones. In Proceedings of the 15th European Symposium on Research in Computer Security (ESORICS'10), pp. 55–70, Lecture Notes in Computer Science 6345, Springer, Athens, Greece, September 2010.
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.
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.
@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)},
OPTDOI = {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},
lsv-category = {intc},
wwwpublic = {public and ccsb},
}