Formal verification of a cryptographic protocol in Cooperative Intelligent Transport Systems communications

Cooperative Intelligent Transport Systems (C-ITS) and Vehicle-to-Everything (V2X) communication are at the forefront of revolutionizing transportation. C-ITS enables vehicles to communicate with each other and with traffic management systems through wireless networks, which supports cooperative and automated driving experiences. V2X is a broader term that includes various forms of vehicle communication, such as vehicle-to-vehicle (V2V), vehicle-to-infrastructure (V2I), vehicle-to-network (V2N), and vehicle-to-pedestrian (V2P) communications. These technologies are integral to enhancing road safety, traffic efficiency, and driving comfort.SCOOP@F, or "Système COopératif", is a pioneering C-ITS project in France that aims to improve road safety and traffic management by enabling V2V and V2I communication. This collaborative effort between road managers and car manufacturers tackles real-life challenges such as privacy, cybersecurity, and interoperability. The thesis in question examines the security mechanisms and the protocols used in SCOOP@F. In particular, it focuses on message exchanges between vehicles and Public Key Infrastructure (PKI) entities, as well as among the PKI entities themselves. Given the complexity and potential vulnerabilities of cryptographic protocols, which are crucial for protecting digital communications, the security mechanisms of the protocol require meticulous inspection. This scrutiny ensures the protection of message exchanges, thereby safeguarding user privacy and system integrity. Formal verification of cryptographic protocols, also used in C-ITS, is highlighted as a vital process to validate their resilience against potential vulnerabilities and to verify their security properties and robustness against message manipulation by attackers on the network. Proverif, a state-of-the-art tool for formal verification, is utilized to symbolically model and analyze the protocol. Proverif is capable of handling a wide range of cryptographic primitives and can process an unlimited number of protocol sessions simultaneously, allowing for extensive analysis and verification of protocols under various conditions and scenarios. The results of the formal verification, which are described in the thesis, show the traces produced by the tool. This verification process is essential to instill trust in the C-ITS landscape, where highly reliable communications and secure protocols are required.