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

**Authors:** Felipe Boeira, Mikael Asplund  
**arXiv:** [2105.02664](https://arxiv.org/abs/2105.02664)  
**Date:** 2021-05-06  
**Summary page:** https://www.summarizepaper.com/en/paper/2105.02664v2/

## Key points

- The paper focuses on the security evaluation of a vehicular platooning protocol designed to enhance road traffic efficiency, safety and reduce fuel consumption.
- The authors perform a systematic analysis of the protocol and security standards to ensure secure deployment of these applications.
- They use a proof strategy based on a relation on keys to tackle the complexity of the resulting model.
- The key relation forms a partial order that encapsulates both secrecy and authenticity dependencies.
- The authors compare different proof strategies such as Bare TAMARIN, Lemma reuse, Oracle only and Order-aware.
- Their order-aware approach makes verification feasible and proves strong authenticity properties along with secrecy of all keys used throughout the protocol.
- The paper provides a formal analysis of Ensemble - a pre-standardization vehicular group formation protocol with key establishment and distribution - through defining secrecy and authentication relations applied in a proof strategy based on their partial order.
- The authors automate key hierarchy extraction from TAMARIN models by creating oracles to guide prover based on ordering keys while using ASN.1 definitions from standards as well as compilers to generate sample packets for refining message protocols avoiding misinterpretations or ambiguities from multiple documents.
- They discuss weaknesses found within IEEE and ETSI security message formats when appropriate checks are not performed by vehicles.
- They suggest that formally describing agent behavior towards received data and appropriate security checks could be a point of discussion in the context of standardization work.
- Finally, they believe that an automated security analysis should be able to derive without manual intervention the ideal tuning for TAMARIN in formal analysis of several complex protocols while contributing to future work on analyzing vehicular platooning.

## Summary

This paper focuses on the security evaluation of a vehicular platooning protocol designed to enhance road traffic efficiency, safety and reduce fuel consumption. The authors perform a systematic analysis of the protocol and security standards to ensure secure deployment of these applications. They use a proof strategy based on a relation on keys to tackle the complexity of the resulting model. The key relation forms a partial order that encapsulates both secrecy and authenticity dependencies. By using this approach, they prove strong authenticity properties along with secrecy of all keys used throughout the protocol. The authors compare different proof strategies such as Bare TAMARIN, Lemma reuse, Oracle only and Order-aware. They demonstrate that their order-aware approach makes verification feasible and proves strong authenticity properties along with secrecy of all keys used throughout the protocol. The results show that the key-aware oracle is crucial in making the model tractable for verifiers. The paper also discusses related work in formal verification and solving theory. Cremers and Mauw employ partial order reduction to lower the number of traversed states in checking secrecy of terms in a cryptographic protocol in their tool SCYTHER while Schmidt et al. develop an algorithm to verify protocol group key agreement protocols that can handle Diffie-Hellman exponentiation, bilinear pairing and AC-operators. In conclusion, this paper provides a formal analysis of Ensemble - a pre-standardization vehicular group formation protocol with key establishment and distribution - through defining secrecy and authentication relations applied in a proof strategy based on their partial order. The authors automate key hierarchy extraction from TAMARIN models by creating oracles to guide prover based on ordering keys while using ASN.1 definitions from standards as well as compilers to generate sample packets for refining message protocols avoiding misinterpretations or ambiguities from multiple documents. The authors also discuss weaknesses found within IEEE and ETSI security message formats when appropriate checks are not performed by vehicles. They suggest that formally describing agent behavior towards received data and appropriate security checks could be a point of discussion in the context of standardization work. Finally, they believe that an automated security analysis should be able to derive without manual intervention the ideal tuning for TAMARIN in formal analysis of several complex protocols while contributing to future work on analyzing vehicular platooning.