The automotive domain is transitioning: vehicles act as rolling servers, persistently connected to numerous external entities. This connectivity, combined with rising on-board computing power for advanced driver assistance systems and similar use cases, creates escalating challenges for securing automotive network architectures. This work advances the security analysis of internet-connected automotive network architectures and their protocols. We introduce a strong, active adversary model tailored to the automotive domain. We substantially extend security protocol verification possible based on Attack Resilience Hyperproperties (ARHs) by introducing a verification-orchestration algorithm. Furthermore, we provide methods for comparative attribution of security property invalidations to specific, ne-grained component compromises. We present a novel integration of formal verification and process mining. By utilizing ARH counterexample traces for process mining, we systematically identify and aggregate attacker behavior that causes security property invalidations. This pipeline enables in-depth understanding of root causes and attack paths leading to protocol-security invalidations. We demonstrate real-world applicability through a prototype and case study on the secure transmission of battery management system data within an automotive network architecture.

翻译：汽车领域正在转型：车辆作为移动服务器运行，持续与众多外部实体连接。这种连接性，加上用于高级驾驶辅助系统及类似用例的车载计算能力的提升，给保障汽车网络架构安全带来了日益严峻的挑战。本文推进了联网汽车网络架构及其协议的安全分析。我们引入了一个针对汽车领域量身定制的强主动攻击者模型。通过引入一种验证编排算法，我们显著扩展了基于攻击弹性超属性（ARHs）的安全协议验证能力。此外，我们提供了将安全属性失效比较性地归因于特定、精细的组件受损的方法。我们展示了形式验证与过程挖掘的一种新颖集成。通过利用ARH反例轨迹进行过程挖掘，我们系统地识别并聚合导致安全属性失效的攻击者行为。这一流程能够深入理解导致协议安全失效的根本原因和攻击路径。我们通过一个针对汽车网络架构内电池管理系统数据安全传输的原型及案例研究，展示了其实际应用性。