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.

• Type: Conference
• Year: 2010
• Where: ESORICS
• Authors: Morten Dahl, Stéphanie Delaune, Graham Steel
• Keywords: Ad-Hoc Networks, ESORICS 2010, Safety Critical Applications, Security Privacy, Vehicles