Formally verifiable features in embedded vehicular security systems

Embedding Security in Vehicles, Wolf et al. give a general state-of-the-art overview of IT security in vehicles and describe core security technologies and relevant security mechanisms. In this paper we show that a formal analysis of many of the related properties is possible. This indicates that many expected aspects in the design of vehicular security can be verified formally. Our presentation is based on a recent paper by the second author et al. [13] where a new attestation-based vehicular security systems is represented. We briefly summarize the general properties required in the design of vehicular IT security and verify that the new architecture given by Oguma et al. suggests new desirable security aspects. I