Modern cars are highly connected and complex IT systems, featuring various services such as backend communication, Vehicle to Everything (V2X) communication, app-control of car features, and seamless authentication of charging processes for electric vehicles. This poses new challenges to cybersecurity as many previous attacks have demonstrated. Because of the broad attack surface, it is important to not only consider the security of the car’s external interfaces but also secure the internal communication to hamper lateral movement. However, designing secure communication protocols is prone to errors. Despite this, many common automotive protocol standards have not been thoroughly analyzed. A powerful method for such an analysis is formal verification, which defines and proves the security properties provided by a protocol. This can be further supported by automated tools such as the Tamarin prover. In this work, we formally analyze the security of automotive communication protocol standards for in-vehicle and external communication and propose security extensions or mitigations for the issues we identify. For in-vehicle communication, we analyze AUTOSAR SecOC, an authentication protocol for CAN and automotive Ethernet communication, and the communication middlewares SOME/IP and DDS. We identify multiple attacks on SOME/IP and propose two extensions to address its missing security mechanism, one based on asymmetric cryptography and digital certificates and one based on symmetric cryptography utilizing a central authentication server. In our analysis of DDS, we identify a vulnerability in the encryption algorithm that can enable replay attacks in some circumstances. Furthermore, we systematically compare different approaches to secure automotive Ethernet-based in-vehicle communication, also considering MACsec, IPsec, and TLS. Finally, we introduce a new dataset for in-vehicle communication that highlights the limitations of the current state-of-the-art and is a useful resource for developing vehicular IDSs. For external communication, we focus on two important use cases: Vehicle diagnostics and Electric Vehicle (EV) charging. We formally analyze the authentication mechanisms in the diagnostics protocol UDS, pointing out insecure configurations and identifying two novel vulnerabilities. We propose and formally verify mitigations for these vulnerabilities and practically evaluate a resulting attack. For the second use case, we propose two extensions to the ISO 15118 protocol for EV charging. Our first extension implements missing privacy properties, while our second extension augments the protocol standard with security against quantum attackers and a mechanism for cryptographic agility. Both extensions are formally verified and practically evaluated. Finally, we propose a novel concept for a privacy-preserving EV charging protocol. This thesis demonstrates how formal verification can improve the security of automotive communication protocol standards and, thus, should become an integral part of the development of new security protocols.
Timm Lauser (Thu,) studied this question.