Sciweavers

Share
ESORICS
2010
Springer

Formal Analysis of Privacy for Vehicular Mix-Zones

9 years 1 months ago
Formal Analysis of Privacy for Vehicular Mix-Zones
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 show that in many scenarios it does not preserve privacy, and we propose a fix.
Morten Dahl, Stéphanie Delaune, Graham Stee
Added 09 Nov 2010
Updated 09 Nov 2010
Type Conference
Year 2010
Where ESORICS
Authors Morten Dahl, Stéphanie Delaune, Graham Steel
Comments (0)
books