Formal Verification of a V2X Privacy Preserving Scheme Using Proverif

V2X communications will be an integral part of all vehicles in the future, broadcasting information such as the vehicle's speed and position to all surrounding neighbors. Being sensitive, a compromise of this data may expose the vehicle to cyberattacks. In this paper, we focus on a particular issue, which is the privacy of vehicles and their drivers. Specifically, we consider a scheme that has been proposed in the literature for ensuring privacy in v2x communications, we build a formal model of it and we analyze its security properties through formal verification. Our analysis conducted using Proverif revealed some issues that could impact the privacy and safety of the vehicle. Some of them are well-known in the literature and could be common to other existing schemes; other ones are specific to the modeled protocol.