University of Surrey

Test tubes in the lab Research in the ATI Dance Research

Formal Analysis of V2X Revocation Protocols.

Whitefield, Jorden, Chen, Liqun, Kargl, F, Paverd, A, Schneider, Steven, Treharne, Helen and Wesemeyer, Stephan (2017) Formal Analysis of V2X Revocation Protocols. Proceedings of STM’17. Lecture Notes in Computer Science..

[img]
Preview
Text
main.pdf - Accepted version Manuscript

Download (474kB) | Preview

Abstract

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, 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 literature 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.

Item Type: Article
Divisions : Faculty of Engineering and Physical Sciences > Computing Science
Authors :
NameEmailORCID
Whitefield, Jordenj.whitefield@surrey.ac.ukUNSPECIFIED
Chen, Liqunliqun.chen@surrey.ac.ukUNSPECIFIED
Kargl, FUNSPECIFIEDUNSPECIFIED
Paverd, AUNSPECIFIEDUNSPECIFIED
Schneider, StevenS.Schneider@surrey.ac.ukUNSPECIFIED
Treharne, HelenH.Treharne@surrey.ac.ukUNSPECIFIED
Wesemeyer, StephanS.Wesemeyer@surrey.ac.ukUNSPECIFIED
Date : September 2017
Copyright Disclaimer : The final publication will be available at Springer via http://www.springer.com/gb/computer-science/lncs
Uncontrolled Keywords : ad hoc networks, authentication, security verification, V2X.
Related URLs :
Additional Information : Paper presented at the 13th International Workshop on Security and Trust Management (STM 2017) Oslo, Norway, September 14-15, 2017
Depositing User : Melanie Hughes
Date Deposited : 09 Aug 2017 10:14
Last Modified : 09 Aug 2017 10:17
URI: http://epubs.surrey.ac.uk/id/eprint/841862

Actions (login required)

View Item View Item

Downloads

Downloads per month over past year


Information about this web site

© The University of Surrey, Guildford, Surrey, GU2 7XH, United Kingdom.
+44 (0)1483 300800