Formal Analysis of C-ITS PKI protocols - Equipe Autonomic and Critical Embedded Systems
Conference Papers Year : 2024

Formal Analysis of C-ITS PKI protocols

Abstract

Vehicular networking is gaining a lot of popularity and attraction from among the industry and academic research communities in the last decade. The communication between vehicles will lead to more efficient and secured roads because we will be able to provide information about traffic and road conditions to vehicle’s drivers. However, ensuring the security of these networks and devices still remains a main major concern to guarantee the expected services. Secure Public Key Infrastructure (PKI) represents a common solution to achieve many security and privacy requirements. Unfortunately, current Cooperative Intelligent Transport Systems (C-ITS) PKI protocols were not verified in terms of security and privacy. In this paper, we propose a security analysis of C-ITS PKI protocols in the symbolic model using ProVerif. We formally modeled C-ITS PKI protocols based on the specifications given in the ETSI standard. We model C-ITS PKI protocols and formalize their security properties in the applied Pi-calculus. We used an automatic privacy verifier UKano to analyse Enrolment protocol. We found attacks on authentication properties, in Authorization and Validation protocols when considering a dishonest Authorization Authority (AA).We analysed proof results and we fixed identified attacks by introducing new parameters in protocol request.
Fichier principal
Vignette du fichier
SECRYPT-2024.pdf (405.66 Ko) Télécharger le fichier
Origin Files produced by the author(s)

Dates and versions

hal-04620494 , version 1 (21-06-2024)

Identifiers

  • HAL Id : hal-04620494 , version 1

Cite

Mounira Msahli, Pascal Lafourcade, Dhekra Mahmoud. Formal Analysis of C-ITS PKI protocols. SECRYPT : International Conference on Information Security and Cryptography, Jul 2024, Dijon, France. ⟨hal-04620494⟩
352 View
80 Download

Share

More