Formal analysis of V2X revocation protocols

Jorden Whitefield, Liqun Chen, Frank Kargl, Andrew Paverd, Steve Schneider, Helen Treharne*, Stephan Wesemeyer

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contributionScientificpeer-review

17 Citations (Scopus)


Research on vehicular networking (V2X) security has produced a range of securitymechanisms 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, that is the revocation of malicious or misbehaving vehicles from the V2X system by invalidating their credentials. This revocation needs to be performed in an unlinkable way for vehicle privacy even in the context of vehicles regularly changing their pseudonyms. 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 two flaws: one previously reported in the lierature concerned with functional correctness of the protocol, and one previously unknown flaw concerning an authentication property of the R-token scheme. In response to these flaws we 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.

Original languageEnglish
Title of host publicationSecurity and Trust Management - 13th International Workshop, STM 2017, Proceedings
Number of pages17
Publication statusPublished - 2017
MoE publication typeA4 Article in a conference publication
EventInternational Workshop on Security and Trust Management - Oslo, Norway
Duration: 14 Sep 201715 Sep 2017
Conference number: 13

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume10547 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


WorkshopInternational Workshop on Security and Trust Management
Abbreviated titleSTM


  • Ad hoc networks
  • Authentication
  • Security verification
  • V2X


Dive into the research topics of 'Formal analysis of V2X revocation protocols'. Together they form a unique fingerprint.

Cite this