Exploiting Partial Order of Keys to Verify Security of a Vehicular Group Protocol

TL;DR

This paper presents a novel verification method for vehicular group protocols that leverages the partial order of keys to efficiently prove security properties like secrecy and authenticity.

Contribution

It introduces a relation-based proof strategy using key partial orders to verify complex vehicular security protocols more effectively.

Findings

Proves strong authenticity properties of the protocol.

Establishes secrecy of all protocol keys.

Demonstrates the feasibility of order-aware verification.

Abstract

Vehicular networks will enable a range of novel applications to enhance road traffic efficiency, safety, and reduce fuel consumption. As for other cyber-physical systems, security is essential to the deployment of these applications and standardisation efforts are ongoing. In this paper, we perform a systematic security evaluation of a vehicular platooning protocol through a thorough analysis of the protocol and security standards. We tackle the complexity of the resulting model with a proof strategy based on a relation on keys. The key relation forms a partial order, which encapsulates both secrecy and authenticity dependencies. We show that our order-aware approach makes the verification feasible and proves strong authenticity properties along with secrecy of all keys used throughout the protocol.