Morten Dahl, Stéphanie Delaune, and Graham Steel. Formal Analysis of Privacy for Vehicular Mix-Zones. In Proceedings of the Workshop on Foundations of Security and Privacy (FCS-PrivMod'10), pp. 55–70, Edinburgh, Scotland, UK, July 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-fcsprivmod10,
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 = {Edinburgh, Scotland, UK},
author = {Dahl, Morten and Delaune, St{\'e}phanie and
Steel, Graham},
booktitle = {{P}roceedings of the {W}orkshop on {F}oundations of
{S}ecurity and {P}rivacy ({FCS-PrivMod}'10)},
OPTDOI = {10.1007/978-3-642-15497-3_4},
editor = {Cortier, V{\'e}ronique and Ryan, Mark D. and
Shmatikov, Vitaly},
month = jul,
pages = {55-70},
title = {Formal Analysis of Privacy for Vehicular Mix-Zones},
year = {2010},
acronym = {{FCS-PrivMod}'10},
nmonth = {7},
lsv-category = {intc},
wwwpublic = {public and ccsb},
}