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 paper, the authors describe a formal analysis of mix-zones. They model a mix-zone and propose a formal definition of privacy for such a zone.