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

• URL: http://arxiv.org/abs/2604.21606v1
• Date: Thu, 23 Apr 2026 12:28:28 GMT
• Title: Process-Mining of Hypertraces: Enabling Scalable Formal Security Verification of (Automotive) Network Architectures
• Abstract summary: We introduce a strong, active adversary model tailored to the automotive domain.<n>We extend security protocol verification possible by introducing a verification-orchestration algorithm.<n>We present a novel integration of formal verification and process mining.
• Score: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: 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.

Related papers

• CANGuard: A Spatio-Temporal CNN-GRU-Attention Hybrid Architecture for Intrusion Detection in In-Vehicle CAN Networks [0.7919969809015935]
  Internet of Vehicles (IoV) has become an essential component of smart transportation systems, enabling seamless interaction among vehicles and infrastructure.<n>This paper presents CANGuard, a deep learning architecture that combines Convolutional Neural Networks (CNN), Gated novel Recurrent Units (RUG) and an attention mechanism to effectively identify such attacks.<n>The proposed approach demonstrates strong potential for practical and scalable security enhancements in modern IoV environments.
  arXiv  Detail & Related papers  (2026-03-26T03:49:04Z)
• OS-Sentinel: Towards Safety-Enhanced Mobile GUI Agents via Hybrid Validation in Realistic Workflows [77.95511352806261]
  Computer-using agents powered by Vision-Language Models (VLMs) have demonstrated human-like capabilities in operating digital environments like mobile platforms.<n>We propose OS-Sentinel, a novel hybrid safety detection framework that combines a Formal Verifier for detecting explicit system-level violations with a Contextual Judge for assessing contextual risks and agent actions.
  arXiv  Detail & Related papers  (2025-10-28T13:22:39Z)
• CANDoSA: A Hardware Performance Counter-Based Intrusion Detection System for DoS Attacks on Automotive CAN bus [45.24207460381396]
  This paper presents a novel Intrusion Detection System (IDS) designed for the Controller Area Network (CAN) environment.<n>A RISC-V-based CAN receiver is simulated using the gem5 simulator, processing CAN frame payloads with AES-128 encryption as FreeRTOS tasks.<n>Results indicate that this approach could significantly improve CAN security and address emerging challenges in automotive cybersecurity.
  arXiv  Detail & Related papers  (2025-07-19T20:09:52Z)
• CANTXSec: A Deterministic Intrusion Detection and Prevention System for CAN Bus Monitoring ECU Activations [53.036288487863786]
  We propose CANTXSec, the first deterministic Intrusion Detection and Prevention system based on physical ECU activations.<n>It detects and prevents classical attacks in the CAN bus, while detecting advanced attacks that have been less investigated in the literature.<n>We prove the effectiveness of our solution on a physical testbed, where we achieve 100% detection accuracy in both classes of attacks while preventing 100% of FIAs.
  arXiv  Detail & Related papers  (2025-05-14T13:37:07Z)
• VMGuard: Reputation-Based Incentive Mechanism for Poisoning Attack Detection in Vehicular Metaverse [52.57251742991769]
  vehicular Metaverse guard (VMGuard) protects vehicular Metaverse systems from data poisoning attacks.<n>VMGuard implements a reputation-based incentive mechanism to assess the trustworthiness of participating SIoT devices.<n>Our system ensures that reliable SIoT devices, previously missclassified, are not barred from participating in future rounds of the market.
  arXiv  Detail & Related papers  (2024-12-05T17:08:20Z)
• Navigating Connected Car Cybersecurity: Location Anomaly Detection with RAN Data [2.147995542780459]
  Cyber-attacks, including hijacking and spoofing, pose significant threats to connected cars. This paper presents a novel approach for identifying potential attacks through Radio Access Network (RAN) event monitoring. The major contribution of this paper is a location anomaly detection module that identifies devices that appear in multiple locations simultaneously.
  arXiv  Detail & Related papers  (2024-07-02T22:42:45Z)
• A Framework for the Systematic Assessment of Anomaly Detectors in Time-Sensitive Automotive Networks [0.4077787659104315]
  We present an assessment framework that allows for reproducible, comparable, and rapid evaluation of anomaly detection algorithms. We evaluate exemplary detection mechanisms and reveal how the detection performance is influenced by different combinations of TSN traffic flows and anomaly types.
  arXiv  Detail & Related papers  (2024-05-02T14:29:42Z)
• SISSA: Real-time Monitoring of Hardware Functional Safety and Cybersecurity with In-vehicle SOME/IP Ethernet Traffic [49.549771439609046]
  We propose SISSA, a SOME/IP communication traffic-based approach for modeling and analyzing in-vehicle functional safety and cyber security. Specifically, SISSA models hardware failures with the Weibull distribution and addresses five potential attacks on SOME/IP communication. Extensive experimental results show the effectiveness and efficiency of SISSA.
  arXiv  Detail & Related papers  (2024-02-21T03:31:40Z)
• A Survey and Comparative Analysis of Security Properties of CAN Authentication Protocols [92.81385447582882]
  The Controller Area Network (CAN) bus leaves in-vehicle communications inherently non-secure. This paper reviews and compares the 15 most prominent authentication protocols for the CAN bus. We evaluate protocols based on essential operational criteria that contribute to ease of implementation.
  arXiv  Detail & Related papers  (2024-01-19T14:52:04Z)
• When Authentication Is Not Enough: On the Security of Behavioral-Based Driver Authentication Systems [53.2306792009435]
  We develop two lightweight driver authentication systems based on Random Forest and Recurrent Neural Network architectures. We are the first to propose attacks against these systems by developing two novel evasion attacks, SMARTCAN and GANCAN. Through our contributions, we aid practitioners in safely adopting these systems, help reduce car thefts, and enhance driver security.
  arXiv  Detail & Related papers  (2023-06-09T14:33:26Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.