A Tale of Two Automotive Security Services: A Formal Analysis

Automotive system faced in the past decade an abundance of security services proposed by the scientific literature to strengthen their system security. The solutions solve problems in terms of key distribution, data authentication, or system monitoring. While the volume of research done brings in consequence novel ideas, strong validation and extensive experimentation is a must to prove their viability and correctness. Consequently, the work at hand offers a formal analysis of two existing security services for automotive systems, namely for a Key Distribution Service (KDS) and for a data authentication and aggregation method titled Mixed data authentication for Controller Area Network (MixCAN). While the KDS aims to distribute long-term and short-term cryptographic keys, MixCAN envisions a lightweight authentication protocol through Encrypted Bloom Filters (EBFs). The objective of the formal analysis is to prove the correctness of the mentioned security solutions through a Burrows-Abadi-Needham (BAN) logic analysis.