Exploiting Partial Order of Keys to Verify Security of a Vehicular Group Protocol
This addresses security for vehicular networks, which is essential for safety and efficiency, but the approach is incremental as it builds on existing verification methods with a specific adaptation.
The paper tackled the security verification of a vehicular platooning protocol by using a proof strategy based on a partial order relation on keys, making the verification feasible and proving strong authenticity properties along with secrecy of all keys.
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.