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.
Formal Verification of a V2X Privacy Preserving Scheme Using Proverif / Bussa, Simone; Sisto, Riccardo; Valenza, Fulvio. - (2023), pp. 341-346. (Intervento presentato al convegno 2023 IEEE International Conference on Cyber Security and Resilience (CSR) tenutosi a Venice (IT) nel 31 July 2023 - 02 August 2023) [10.1109/CSR57506.2023.10224908].
Formal Verification of a V2X Privacy Preserving Scheme Using Proverif
Bussa, Simone;Sisto, Riccardo;Valenza, Fulvio
2023
Abstract
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.File | Dimensione | Formato | |
---|---|---|---|
92_simone_bussa_Camera_Ready (1).pdf
accesso aperto
Tipologia:
2. Post-print / Author's Accepted Manuscript
Licenza:
Pubblico - Tutti i diritti riservati
Dimensione
368.11 kB
Formato
Adobe PDF
|
368.11 kB | Adobe PDF | Visualizza/Apri |
Formal_Verification_of_a_V2X_Privacy_Preserving_Scheme_Using_Proverif.pdf
accesso riservato
Tipologia:
2a Post-print versione editoriale / Version of Record
Licenza:
Non Pubblico - Accesso privato/ristretto
Dimensione
1.02 MB
Formato
Adobe PDF
|
1.02 MB | Adobe PDF | Visualizza/Apri Richiedi una copia |
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
https://hdl.handle.net/11583/2982760