Formal Analysis of V2X Revocation Protocols

Jorden Whitefield1, Liqun Chen1, Frank Kargl2, Andrew Paverd3, Steve Schneider1, Helen Treharne1, and Stephan Wesemeyer1

1Department of Computer Science, University of Surrey, Guildford, UK
{J.Whitefield, Liqun.Chen, S.Schneider, H.Treharne, S.Wesemeyer}

2Ulm University, Ulm, Germany

3Aalto University, Espoo, Finland


Research on vehicular networking (V2X) security has produced a range of security mechanisms and protocols tailored for this domain, addressing both security and privacy. Typically, the security analysis of these proposals has largely been informal. However, formal analysis can be used to expose flaws and ultimately provide a higher level of assurance in the protocols. This paper focusses on the formal analysis of a particular element of security mechanisms for V2X found in many proposals: the revocation of malicious or misbehaving vehicles from the V2X system by invalidating their credentials, even in the context of vehicles regularly changing their pseudonyms in an unlinkable way for vehicle privacy. The Rewire scheme by Förster et al. and its subschemes Plain and R-Token aim to solve this challenge by means of cryptographic solutions and trusted hardware. Formal analysis using the Tamarin prover identifies flaws with some of the functional correctness and authentication properties in these schemes. We then propose Obscure Token (O-token), an extension of Rewire to enable revocation in a privacy preserving manner. Our approach addresses the functional and authentication properties by introducing an additional key-pair, which offers a stronger and verifiable guarantee of successful revocation of vehicles without resolving the long-term identity. Moreover O-token is the first V2X revocation protocol to be co-designed with a formal model.


    author = "Jorden Whitefield, Liqun Chen, Frank Kargl, Andrew Paverd,
              Steve Schneider, Helen Treharne, and Stephan Wesemeyer",
    title = "{Formal Analysis of V2X Revocation Protocols}",
    year = "2017"


Jorden Whitefield is funded by the EPSRC iCASE studentship 15220193 through Thales UK. Thanks to Cas Cremers for detailed discussions on Tamarin. Thanks also to François Dupressoir and Adrian Waller for providing detailed feedback on early versions of this paper.