Formal Analysis of V2X Revocation Protocols
Authors:
Jorden Whitefield,
Liqun Chen,
Frank Kargl,
Andrew Paverd,
Steve Schneider,
Helen Treharne,
Stephan Wesemeyer
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…
▽ More
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. 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 Forster et al. and its subschemes BASIC and RTOKEN aim to solve this challenge by means of cryptographic solutions and trusted hardware.
Formal analysis using the TAMARIN prover identifies two flaws with some of the functional correctness and authentication properties in these schemes. We then propose Obscure Token (OTOKEN), 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 OTOKEN is the first V2X revocation protocol to be co-designed with a formal model.
△ Less
Submitted 6 August, 2017; v1 submitted 24 April, 2017;
originally announced April 2017.
Symbolic Reachability Analysis of B through ProB and LTSmin
Authors:
Jens Bendisposto,
Philipp Koerner,
Michael Leuschel,
Jeroen Meijer,
Jaco van de Pol,
Helen Treharne,
Jorden Whitefield
Abstract:
We present a symbolic reachability analysis approach for B that can provide a significant speedup over traditional explicit state model checking. The symbolic analysis is implemented by linking ProB to LTSmin, a high-performance language independent model checker. The link is achieved via LTSmin's PINS interface, allowing ProB to benefit from LTSmin's analysis algorithms, while only writing a few…
▽ More
We present a symbolic reachability analysis approach for B that can provide a significant speedup over traditional explicit state model checking. The symbolic analysis is implemented by linking ProB to LTSmin, a high-performance language independent model checker. The link is achieved via LTSmin's PINS interface, allowing ProB to benefit from LTSmin's analysis algorithms, while only writing a few hundred lines of glue-code, along with a bridge between ProB and C using ZeroMQ. ProB supports model checking of several formal specification languages such as B, Event-B, Z and TLA. Our experiments are based on a wide variety of B-Method and Event-B models to demonstrate the efficiency of the new link. Among the tested categories are state space generation and deadlock detection; but action detection and invariant checking are also feasible in principle. In many cases we observe speedups of several orders of magnitude. We also compare the results with other approaches for improving model checking, such as partial order reduction or symmetry reduction. We thus provide a new scalable, symbolic analysis algorithm for the B-Method and Event-B, along with a platform to integrate other model checking improvements via LTSmin in the future.
△ Less
Submitted 14 March, 2016;
originally announced March 2016.
