Security Analysis of Automotive Protocols

The technology of modern vehicles is currently undergoing a major transformation with increased communication and the introduction of new protocols. It is essential that these protocols are secure and do not allow attacks on the vehicle. In this paper, we discuss how formal models can be used to verify the security of protocols used in modern vehicles and propose new group membership authentication properties for shared key scenarios used in some automotive protocols. Our focus is on tool-based analysis for which we provide an overview of suitable tools, analyze the current status of (automotive) protocol analysis and, as an example, analyze AUTOSAR's Secure Onboard Communication (SecOC) with the Tamarin tool. Our results show that tool-based formal analysis is a relatively quick and easy way to assess the security of protocols and can help to increase the security of modern vehicles.