Process-Mining of Hypertraces: Enabling Scalable Formal Security Verification of (Automotive) Network Architectures

Computer Science > Cryptography and Security [Submitted on 23 Apr 2026] Process-Mining of Hypertraces: Enabling Scalable Formal Security Verification of (Automotive) Network Architectures Julius Figge, David Knuplesch, Andreas Maletti, Dragan Zuvic 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. Comments: Full version prior to submission for publication Subjects: Cryptography and Security (cs.CR) Cite as: arXiv:2604.21606 [cs.CR]   (or arXiv:2604.21606v1 [cs.CR] for this version)   https://doi.org/10.48550/arXiv.2604.21606 Focus to learn more Submission history From: Julius Figge [view email] [v1] Thu, 23 Apr 2026 12:28:28 UTC (6,077 KB) Access Paper: view license Current browse context: cs.CR < prev   |   next > new | recent | 2026-04 Change to browse by: cs References & Citations NASA ADS Google Scholar Semantic Scholar Export BibTeX Citation Bookmark Bibliographic Tools Bibliographic and Citation Tools Bibliographic Explorer Toggle Bibliographic Explorer (What is the Explorer?) Connected Papers Toggle Connected Papers (What is Connected Papers?) Litmaps Toggle Litmaps (What is Litmaps?) scite.ai Toggle scite Smart Citations (What are Smart Citations?) Code, Data, Media Demos Related Papers About arXivLabs Which authors of this paper are endorsers? | Disable MathJax (What is MathJax?)