Formal Security Verification of a Standard Protocol for V2X Communications

Vehicle-to-Everything communications are technologies that enable message exchange between vehicles and other vehicles or infrastructure components. These technologies are employed for the Intelligent Transportation Systems which enable the implementation of safety-related applications such as electronic emergency braking light, cooperative collision avoidance or traffic light announcements. The messages exchanged between vehicles and other vehicles or infrastructure elements, called Basic Safety Messages, contain sensitive information such as time, position, and motion data. It is critical to protect this information to prevent users tracking and attacks that could harm users' safety. To address the security issues, Crash Avoidance Metrics Partners LLC developed the Security Credential Management System to support the establishment of a Public Key Infrastructure for V2X security, which issues certificates to system participants. The solution adopted to protect the users privacy is the use of Pseudonym Certificates, which provide authentication while protecting user identity and making tracking more difficult. The objective of this thesis is to use formal verification methods to analyse the protocol and verify its security properties. The formal analysis was performed using the Tamarin prover. Each protocol step was formalized and sanity checks were executed to verify the execution of the protocol. The work then focused on the formal verification of security properties such as secrecy and authentication.