Formal verification of a V2X Security Credential Management System

Vehicles are currently being developed and sold with increasing levels of connectivity and automation. Communication technologies connect the vehicles with various on-road elements, such as pedestrians, infrastructures, roads, cloud computing platforms etc. to each other. V2X communication technology is expected to improve traffic efficiency by reducing traffic incidents and road pollution. Some examples of how this technology could be very promising and useful are: traffic jam/incident reporting, collision warning and avoidance, cooperative automated driving, infotainment services. All of this, results in a heightened risk of cyber-security attacks. In literature many different types of attack have been extensively and deeply analyzed and discussed. Here the focus is on the privacy. The main issue is related to the mechanism used to provide authenication and integrity of the exchanged messages. This is typically obtained using digital signatures and a digital certificate that certifies the public key of the vehicle. But this exposes the vehicle to a lack of anonymity and unlinkability. An attacker who intercepts all messages signed using the same certificate could link these data and trace the vehicle position. The most promising solution to solve this problem is the use of pseudonymous certificates. By using pseudonyms, each node can safely exchange messages preserving authentication and integrity and at the same time they can provide a certain level of conditional linkability, that can be used by authorities in case of disputes to resolve the initial identity of the vehicle or to profile services offered to the nodes. Among all pseudonym related vehicular communication protocols, the stateof- the-art is represented by Security Credential Management System, developed by the Crash Avoidance Metrics Partners LLC. The thesis focuses on the formal analysis of the protocol by means of the TAMARIN prover. Formal verification strives to provide a rigid and thorough method of analyzing the correctness of a security protocol, allowing even minor flaws to be discovered. Since the aims of using this communication protocol will be, to be widespread on V2X communications, even the slightest vulnerability will result in tremendous harm to all users who use it. This is why it is important to formally verify these protocols, so to be sure they meet the security properties they claim. Lemmas were implemented that describe all the security properties that must be fulfilled by the protocol.