arXiv CSopen access

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

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

arXiv:2604.21606v1 [cs.CR] 23 Apr 2026

1

1,2

, David Knuplesch2 , Andreas Maletti1 , and Dragan Zuvic2

Institute of Computer Science, Leipzig University, 04109 Leipzig, Germany {julius.figge,andreas.maletti}@uni-leipzig.de 2 Mercedes-Benz Tech Innovation GmbH, 89081 Ulm, Germany {julius.figge,david.knuplesch,dragan.zuvic}@mercedes-benz.com

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, fine-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. Keywords: Formal Verification · Hyperproperties · Process Mining · Automotive Security · Network Architectures

1

Introduction

Automotive vehicles are undergoing a major transformation [15], with the emergence of software-defined vehicles [2] and ubiquitous connectivity to external entities, e.g. mandatory over-the-air updates [24], becoming the norm. Vehicles are evolving into rolling datacenters with high-performance compute units using hypervisors and virtual machines [27, 12], increasingly exposing them to broader cybersecurity challenges, including e.g. the shift to post-quantum cryptography [17] and required hardening against (remote) compromise. These challenges

2

J. Figge et al.

are compounded by regulation, including UN Regulation No. R156 (over-the-air updates), UN Regulation No. R155 (cybersecurity and software update management systems), and ISO/SAE 21434 (Road vehicles – Cybersecurity engineering) [25, 20]. In parallel, vehicle functionality advances through systems such as advanced driver assistance system (ADAS) and battery-electric platforms, introducing further safety challenges that necessitate security. Motivation and Research Gap Component compromise in the automotive domain is expected; its occurrence is a matter of when, not if [14, 26]. This motivates the comprehensive analysis of automotive network architectures (ANAs) security under (partial) compromise as required by automotive regulations (e.g., ISO 21434) [20]. Formal verification is well suited to prove the conditions under which security properties (SPs) of protocols in ANAs become invalid. Simultaneously, research gaps remain in formal verification (FV) capabilities required to analyse ANAs. In particular, a comprehensive view is lacking, which would allow assessing the impact of different possible partial compromises. Statespace explosion limits comprehensive granularity, because of the trade-off between detail and analysis complexity. Thus, FV focuses on refuting the examined SPs [6], yielding only isolated compromise scenarios as counterexamples. This e.g. hinders comparative analyses of compromise impacts on SP validity and the verification of fine-grained permission models. We previously investigated these security challenges in ANAs [8, 9]. In particular, with Attack Resilience Hyperproperties (ARHs) [9], we provide a systematic method to analyze protocol SPs invalidation. Grounded in security-protocol verification, ARHs are hyperproperties (HPs) that attribute SP’s invalidation to protocol components (e.g., control units and network domains). For instance, they permit the identification of components that are necessary for the invalidation of a given SP, but are not sufficient when considered in isolation. Despite these strengths, the above research gaps remain for ARHs, but some are addressable. However, their foundational approach imposes a conceptual limitation: ARH analysis answers “who” is responsible for invalidation but not “how ” adversarial behavior invalidates a protocol’s SPs. These ARH limitations should be addressed by developing a method to synthesize comprehensive SPs invalidating attacker behaviors. This is especially relevant since HP-based attribution obscures the underlying counterexample-traces, which renders the manual analysis of many traces, which is required to understand the possible attacker behavior, impractical. Research Questions Our research questions RQ1-RQ5 delineate this contribution’s scope and limits and explicitly address the identified research gap. To reflect automotive architectural specifics and attacker’s operating conditions, we must define a suitable attacker model (RQ1) that captures adversarial behavior, which is observed in the automotive domain, while not being limited to it. Current ARH analysis is constrained by state-space explosion. To advance the state of art and ensure practical applicability, we devise algorithmic improve-

Process-Mining for Formal Security Verification of Automotive Architectures

3

ments that reduce the number of scenarios to analyze (RQ2). With respect to the current capabilities of ARH analysis, it is desirable to enhance granularity by incorporating comparative assessments across SPs (RQ3) and by distinguishing between different compromise modalities (RQ4). This increases both the level of detail and depth of the analysis. While current approaches are limited to compromise attribution without identifying the behavior that invalidates SPs, our work focuses on comprehensive attacker-behavior identification and the development of necessary analysis techniques (RQ5). RQ1 How can an attacker model be extended to represent strong, active adversaries in automotive network architectures who participate maliciously in protocol flows? RQ2 Which approaches can make ARH-based hyperproperty analysis scalable by reducing the number of compromise scenarios that must be verified? RQ3 Which methods enable the comparison of compromise scenarios across multiple security properties to assess and contrast invalidation conditions? RQ4 How can compromise modalities (e.g. read vs. write permissions) be modeled and analyzed to explain their impact on the invalidation of security properties? RQ5 How can ARH analysis be extended to identify and summarize adversarial behavior that causes invalidation of security property? Contributions Our contributions C1–C4, detailed in the next section, directly address RQ1–RQ5. We map each contribution to its corresponding research question. C1 Adversarial CRASH-model C2 Component compromise impact identification C2.1 ARH verification orchestration algorithm C2.2 Comparative multi-lemma analysis C2.3 Fine granular adversarial permissions C3 Comprehensive adversarial behavior analysis C3.1 Interface between FV and process mining C3.2 Synthetic event-log generation C4 Prototypical implementation ImpACT & ROAD-Miner Our “Compromised Realm Adversary System Hack” model (CRASH-model) (see Sect. 2.1), contribution C1, successfully answers RQ1 by providing an adversary model tailored to strong, active attackers in ANAs that covers permission levels, compromise of protocol entities and network segments, message extraction and injection, as well as complete takeover of entities including their full internal knowledge. Our second contribution C2 on identifying component-compromise impact comprises three sub-contributions. For C2.1 we present an ARH verification orchestration algorithm that significantly reduces HP verification runtime and complexity via algorithmic improvements and thus enables the analysis of large problem spaces and complex, fine-grained compromise scenarios as required by RQ2.

4

J. Figge et al.

For C2.2 we provide an extended comparative analysis of ARHs (see Sect. 3.2) to answer RQ3 on the impact of different compromise scenarios across security properties. With C2.3 we provide fine-grained adversarial permissions (see Sect. 3.2) to answer RQ4 on analyzing how different compromise types and variants invalidate security properties. C3 comprises of two sub-contributions that enable a comprehensive adversarial behavior analysis (see Sect. 4) and answer RQ5. We provide an interface between FV and process mining (PM) in C3.1 via a formalization of component definitions, translation elements, and mappings linking both fields. The synthetic event-log generation C3.2 enables the use of security protocol verification traces with PM algorithms to analyze the adversarial behavior. At the same time, the behavioral analyses C3.1 and C3.2 add value to the compromise impact identification C2.2 and C2.3 and further answer RQ3–RQ4. We validate the real-world applicability of our contributions C1–C3 as an answer to RQ1–RQ5 with the help of our prototypical implementations ImpACT and ROAD-Miner (C4; see Sect. 5). Structure We introduce our case study in Sect. 2, define the attacker model, present the ANA and protocol, and define the relevant security properties. We then present our contributions for identifying the impact of component compromises in Sect. 3, a fine-grained subdivision of compromises in Sect. 3.2, comparative SP analysis in Sect. 3.2, and an algorithmic verification-orchestration approach in Sect. 3.3 that enables ARH verification under our attacker model. Next, we present our contribution for the comprehensive adversarial-behavior analysis in Sect. 4. We validate real-world relevance by applying the case study to our prototypical implementation in Sect. 5. Finally, we discuss related work in Sect. 6 and highlight how our contributions differs from existing research. We conclude with a summary and outlook in Sect. 7.

2

Case Study

In the following, we describe our case study using a fictional battery management system (BMS) protocol. We first present our contribution of the CRASH-model as the adversarial model and subsequently the exemplary ANA. We provide a level of detail that reflects an industrially relevant, real-world example while remaining comprehensible. 2.1

Adversarial Model

We present our attacker model as an enhancement of the Dolev-Yao model (DYmodel), the standard adversarial model used in verification tools such as the Tamarin Prover (Tamarin). Our “Compromised Realm Adversary System Hack” model (CRASH-model) (see Fig. 1) is designed with a focus on ANAs and cyber–physical systems. It adds extensions and modifications to better suit these areas than the DY-model.

Process-Mining for Formal Security Verification of Automotive Architectures

5

At its core, the CRASHm2 m4 model introduces two key B m1 k1 changes. These changes m4 m4 m2 A D E F AD focus on entity and dok1 , k 2 m3 k1′ C main compromise and align m′4 m′2 with our threat model, which considers physical Fig. 1: CRASH-model access to networks (including bus systems and Ethernet subnets). Access can lead to takeover and compromise of entities such as electronic control units (ECUs). First, the attacker model supports network segmentation (e.g. into domains). An attacker can interact with traffic (messages on the network) only after compromising a network segment (domain) or a participant (entity). It can intercept messages inside compromised segments (e.g. m2 in Fig. 1) and inject forged messages (m′2 ). Alternatively, it can intercept messages to or from compromised entities (m4 ) or inject such messages (m′4 ).3 This first extension thus refines the existing DY-model capabilities, while the second extension grants the attacker completely new abilities. It can also read and even alter the internal knowledge (k1 ) for all compromised entities. Automotive Network Architecture Our exemplary ANA (see Fig. 2) is a simplified abstracTarget UseCase DGW TCU tion of a real-world ANA. The ANA consists of two main Car Internet components: the vehicle and Fig. 2: Exemplary ANA the Internet. The vehicle is represented by two network segments with different levels of criticality, regarding security and safety. On the left is the Inner domain, the segment of higher criticality, hosting the UseCase ECU. This placeholder is the protocol’s first communication partner. Examples of highly critical ECUs include components such as BMS and autonomous driving systems. The domain gateway (DGW) bridges the Inner and Internet-Facing domains and communicates with the UseCase. In the less critical Internet-Facing domain, the telematic control unit (TCU) is the communication partner, connecting the vehicle to the Internet. On the Internet, the (vehicle manufacturer’s) Backend segment hosts the exemplary Target service, which is the protocol’s recipient and communication partner for the TCU. Inner

Internet-Facing

Backend

Protocol Description Finally, we present our example protocol, based on the previously presented ANA and used in the evaluation of the prototypical implementation (see Sect. 5). The 3

Extended capabilities, such as suppressing or modifying messages, are possible but unnecessary here and are excluded from our model.

6

J. Figge et al.

protocol is intentionally insecure to facilitate demonstration. It targets message authenticity4 [18], while message confidentiality relies on closed network segments and communication channels. We motivate the example with a BMS protocol, where an electric vehicle transmits battery charge status, charge cycles, and temperature to the manufacturer to optimize battery lifespan. The protocol below outlines BMS data transmission in concise, abstracted form. UseCase DGW TCU Target The BMS U seCase mon∼pkUC ∼pkT itors relevant battery parameters to be transmitFr(∼n) ted to the backend and sigN=sign(∼n,∼pkUC) stores them as data ∼n. <∼n,sigN> The data ∼n is signed by <∼n,sigN> the BMS with its private Fr(∼oN) key ∼pkU C and sent to the nh=h(<∼n,∼oN>) sigH=sign(nh,∼pkT) T CU via the DGW . The T CU adds vehicle-specific in<∼n,sigN,∼oN,sigH> formation ∼oN and signs verify(sigN,∼n,pubUC) a hash of the combined nh=h(<∼n,∼oN>) data ⟨∼n, ∼oN ⟩ with its priverify(sigH,nh,pubT) vate key ∼pkT . The data is then transmitted to the manufacturer’s Backend and the Fig. 3: BMS Synchronization Protocol corresponding BMS-Service T arget, which validates the BMS data and vehicular information integrity verif y(. . . ), concluding the protocol.

Security Properties We define the protocol’s security properties (SPs) under the specified threat model (see Sect. 2.1), including resistance to an active attacker and partial compromise scenarios. Secrecy of transmitted data The secrecy property requires that for every nonce (∼n, ∼oN ) in any protocol execution, if at no time an entity’s private key is revealed from the public key infrastructure (PKI), then there exists no time point at which an adversary knows the nonces. Consequently, BMS and vehicular data must remain unknown to the adversary, if no private key is leaked. Authenticity of UseCase messages The authenticity property5 requires that for any protocol execution ending with the target receiving the nonces, if at 4 5

From the perspective of the target, i.e. receiver, service. See List. 1.

Process-Mining for Formal Security Verification of Automotive Architectures

7

no prior time point an entity’s private key was revealed, there must exist an earlier time point at which the U seCase initiated the protocol run with the same nonce ∼n. In other words, the BMS data received by the target must have been sent (and generated) by the U seCase.

3

Identifying Impact of Component Compromise

We introduce our approach for the impact identification of component compromise through Attack Resilience Hyperproperty analysis, as an essential foundation for the following contributions. This enables analysis of complex compromise scenarios with fine-grained permission models and multiple security properties (SPs) across all possible respective combinations. 3.1

Approach Formalization

We subsequently formalize the components necessary for ARH analysis. This formalization builds on our prior work on ARHs [9]. We first define ANAs, comprising the architecture and its application protocols. We then extend this with domain-specific CRASH-model attacker model elements, SPs, and a model of protocol executions, including component states, compromise scenarios and adversarial behavior. An ANA is a directed graph A = (E, L, D), with nodes E representing entities such as ECUs or services, edges L ⊆ E × E as directed communication links, and domains D as network segments. For each e ∈ E, we require (e, e) ∈ L, providing self-links for modeling internal computations. For each domain d ∈ D, a special node ed ∈ E without links is included to support compromise modeling. A message m = (l, n) ∈ L × N is a tuple with link l ∈ L (communication partners) and contents n ∈ N 6 , forming the finite set of all messages M . An entity’s e ∈ E internal computations, such as cryptographic operations on messages, are represented by internal messages ((e, e), n), enabling new values and stored knowledge from a finite set K. To model dynamic knowledge possession, we use a deterministic finite-state automaton (DFA) [31] with state set Q = S × P(K) for finite state set S. The state’s components (s, K ′ ) ∈ Q represent an entity’s internal state s ∈ S and current knowledge K ′ ⊆ K. The DFA is a tuple (Q, A, q0 , δ, F ) with Q = S×P(K) for finite S, action alphabet A ⊆ M , initial state q0 = (s0 , k0 ) ∈ Q with initial state s0 and knowledge k0 , transition function δ∶ Q × A → Q, and set of final states F ⊆ Q. The transition function δ extends to ∆∶ Q × A∗ → Q via ∆(q, ε) = q and ∆(q, aw) = ∆(δ(q, a), w) for all q ∈ Q, a ∈ A, and w ∈ A∗ . Final states F are unused. Each entity e ∈ E is associated with a DFA T (e), modeling its dynamic behavior via message contents; automata are not used for domains d ∈ E. Transitions in T (e) = (Q, A, q0 , δ, F ) occur only on messages involving the entity. We assume A = M and δ(q, a) = q for any message a ∈ A not involving entity e. Thus, 6

Typically a nonce from a set N of random numbers.

8

J. Figge et al.

the state of T (e) remains unchanged for messages where e is neither sender nor receiver. For convenience, we assume a special message content tick = 0, which, when sent as (l, tick) with l ∈ L, causes no reaction, i.e. it does not change any entity’s knowledge or state. A protocol is a finite message sequence w ∈ M ∗ . Every entity e ∈ E reacts as described below; domain nodes ed with d ∈ D are irrelevant because they lack links, i.e. not occur in regular protocol execution. Let T (e) = (Q, M, q0 , δ, F ) be the DFA of e, with knowledge after protocol execution w given by K(e, w) = K ′ , where ∆(q0 , w) = (s, K ′ ). A protocol w is valid if for every prefix w′ ((s, r), n) with final message ((s, r), n), we have n ∈ K(s, w′ ). We define the set of attacker capabilities, i.e. possible permission combinations, as P = {∅, r, w, rw}7 . Recall that E denotes the components (entities or domains). A compromise is a mapping c ∶ E → P . In other words, a compromise assigns attacker capabilities to each component. For convenience, we denote the compromised components as dom(c) = { e ∈ E ∣ c(e) ≠ ∅ }. We use our CRASH-model (see Fig. 1). For any entity e ∈ E compromised with read permission r or rw, all messages to or from e can be intercepted. Similarly, messages ((s, r), n) involving a read-compromised domain d ∈ D can be intercepted, i.e. c(ed ) ∈ {r, rw} and {s, r} ∩ d ≠ ∅. The adversary also has full access to the knowledge of readcompromised entities. In other words, any message content n sent to or from a read-compromised entity or domain is immediately known to the adversary, along with the knowledge and internal state of read-compromised entities. Additionally, the adversary can inject messages to and from write-compromised entities c(e) ∈ {w, rw} and domains c(ed ) ∈ {w, rw}, on behalf of the compromised components. For such messages, we mark the spoofed endpoint with a tick, yielding ((s′ , r), n) or ((s, r′ ), n), respectively. We use this notation to distinguish cases: non-compromised entities are oblivious to spoofing and react normally, including state and knowledge updates. Compromised entities react only to messages in which they are not marked. Otherwise, all entities, including compromised ones, react to protocol messages normally. This keeps the formalization simple while preserving strong adversarial behavior and capabilities. The adversary may use any possessed knowledge to craft injected messages; it is not limited to the spoofed component’s knowledge. We define an Execution Trace as an even-length message sequence w = m1 m′1 m2 m′2 ⋯mn m′n ∈ M ∗ , where messages m′1 , . . . , m′n are controlled and injected by the adversary. The special message ((e, e), tick) for any compromised entity e ∈ dom(c) lets the adversary refrain from injecting a real message, modeling no reaction or change at that time. An execution trace w is valid for compromise c if ⎧ ⎪ if s ∈/ dom(c) ⎪K(s, w′ ) n∈⎨ ′ ⎪ K(e, w ) otherwise ⎪ ⎩⋃e∈E∶c(e)∈{r,rw} for every prefix w′ ((s, r), n) of w. We define the set of possible SPs as S. 7

Extending the utilized permissions to e.g. execution x and deletion d is conceivable.

Process-Mining for Formal Security Verification of Automotive Architectures

9

For a compromise c, security property S ∈ S, and an execution trace w valid for c, we write w ⊧c S if S holds for w. For a set L of execution traces valid for c, we define L ⊧c S to be true iff w ⊧c S for all w ∈ L. For any language L ⊆ M ∗ , we define C(S, L) = { c ∶ E → P ∣ ∃ w ∈ L valid for c with w ⊧ / c S } as the set of compromises for which some valid w ∈ L violates security property S. The complement C(S, L) = P E ∖ C(S, L) represents compromises, where violations of the security property S do not occur.

3.2

ARH Evaluation and Extension

We use our formalization to analyze ARHs, which enable examining responsibility and involvement in SP invalidation across compromise scenarios. In other words, ARHs identify which components are responsible for or involved in an invalidation. To this end, we need to introduce a partial order on the capabilities in the expected manner ∅ < r < rw as well as ∅ < w < rw, but r </ w </ r.8 For compromises c, c′ ∶ E → P we write c ⪯ c′ if c(e) ≤ c′ (e) for all e ∈ E. Finally, we define c′ − c ∶ E → P by (c′ − c)(e) = ∅ for all e ∈ dom(c) and (c′ − c)(e) = c′ (e) otherwise.

ARH For the analysis, we employ the following ARHs [9]: Necessary but not sufficient (NBNS) identifies individual components in multistep compromises of SP S ∈ S, defined as NBNS = min⪯ {c ∈ C(S, L) ∣ ∃c′ ∈ C(S, L)∶ c ⪯ c′ , c′ − c ∈ C(S, L)}. Never responsible for Compromise (NRFC) comprises scenarios that never contribute to invalidating a SP, defined as NRFC = {c ∈ C(S, L) ∣ ∀c′ ∈ C(S, L)∶ c ⪯ c′ implies c′ − c ∈ C(S, L)}. Minimal Compromise Scenario (MCS) captures the smallest compromises that invalidate a given SP, defined as MCS = min⪯ C(S, L). Single Point of Failure (SPOF) is a special case of MCS, defined as SPOF = {c ∈ C(S, L) ∣ ∣dom(c)∣ = 1}.

Multiple security properties We extend the analysis beyond individual ARH by evaluating multiple SPs simultaneously. This enables comparative analysis of SPs by examining the compromise scenarios and execution traces that lead to their invalidation. Consequently, we can identify weaknesses and ARHs that span multiple SPs. To that end, we define the set S(c, L) ⊆ S of SPs that a given compromise scenario c causes to be invalidated by traces w ∈ L as S(c, L) = {S ∈ S ∣ ∃w ∈ L valid for c with w ⊧ / c S} 8

This is the expected Boolean algebra for the 2 capabilities of read r and write w.

10

J. Figge et al.

Fine Granular Compromise Our proposed adversary CRASH-model (see Sect. 2.1) permits a wide range of attacker actions. We categorize these actions and propose fine-granular compromises to model attacker capabilities. Permissions follow a decomposition into non-empty combinations of read, write access P = {∅, r, w, rw}. We provide the mapping c ∶ E → P between components, i.e. protocol entities or domains and respective permissions granted through compromise. For our example (see Fig. 2), an attacker may have write access to the Internet domain and only read access to the TCU. Arbitrary per-component combinations are allowed; granting all capabilities recovers the previous coarsegrained model. This model better reflects scenario-dependent attacker capabilities (e.g. read-only memory extraction or physical man-in-the-middle injection) and supports verification workflows that identify the minimal permissions required to invalidate a SP and isolate irrelevant permissions.

3.3

ARH-Verification Orchestration Algorithm

Introducing fine-grained attacker capabilities and multiple simultaneous SPs significantly increases the number of scenarios for verification. ARH verification must consider every compromise c ∶ E → P and each security property S ∈ S. Consequently, there are ∣P ∣∣E∣ ⋅ ∣S∣ scenarios to verify. Memory demands are limiting the number of parallel executions of separate verifications. However, the time complexity grows exponentially in the number ∣E∣ of components and the number p of capabilities as ∣P ∣ = 2p . In our example we have p = 2 and thus ∣P ∣ = 4. On the other hand, the time complexity grows only linearly in the number ∣S∣ of SPs, which renders this factor manageable for complexity considerations. Overall, we obtain long runtime and substantial computational demand. In our case study, in which we A ↦ rw A ↦ rw A ↦ rw have 4 entities (ECUs), 3 doB↦r B↦w B ↦ rw mains, 2 permissions, and 2 SP, A↦r A↦w we require the verification of B ↦ rw B↦r (22 )4+3 ⋅ 2 = 32, 768 lemmas A↦r A↦w B↦w B↦r (i.e. individual SPs to be valiA↦r A↦w dated against specific comproB↦r B ↦ rw mise scenarios). Even under the optimistic (and unrealistic) asA ↦ rw B ↦ rw sumption that each verificaA↦r A↦w B↦r B↦w tion takes only one second,9 the total runtime is roughly 32, 768 s > 9 h. Hence, a naive – verification strategy is impracFig. 4: Compromise Graph for ARH- tical for complex ARH analyses and an algorithmic improveVerification Traversal ment is required. 9

Tamarin process has startup and other overheads.

Process-Mining for Formal Security Verification of Automotive Architectures

11

Below we present an algorithmic orchestration optimization that enables verification across all compromise scenarios and supports fine-grained capabilities and multiple SPs. This optimization makes ARH verification for complex adversarial and test scenarios in automotive network architectures feasible and is a necessary prerequisite for PM analyses. We exploit the monotonicity of SP invalidation with respect to compromised entities and domains and their capabilities. If a SP S is invalidated by compromise c, then any c′ with c ⪯ c′ also invalidates S [11]. Instead of verifying all scenarios naively, we can thus simply identify the minimal scenarios MCS that cause violations. To this end, we perform a preorder traversal of the Hasse diagram (see Fig. 4) of the partial order ⪯ starting at the least element, in which no entity is compromised. At each node we invoke Tamarin to verify the SPs (lemmas). If all SPs hold, then the traversal proceeds. Otherwise, for any SP invalidated, we simply mark all larger (with respect to ⪯) scenarios as equally invalidated for that property and skip their (costly) verification. This optimization leverages monotonicity under the compromise order ⪯ and thus avoids redundant checks. Traversal then resumes, and at each node we verify only the properties not already marked invalidated. 3.4

Limitations

The FV of ANAs and their protocols with ARHs enables comprehensive, comparative analysis of complex SP. For complex compromise scenarios, our approach assigns responsibility for SP’s invalidation. We identify which components, under which conditions (read or write access), influence SP invalidation, i.e. who is responsible. A limitation of the current approach is the how : which adversarial interactions cause invalidation in each scenario. Our approach yields many traces across all invalidated scenarios; each scenario can produce multiple distinct traces, which are numerous and difficult to analyze manually.

4

Comprehensive Adversarial Behavior Analysis

We address the main limitation of ARH, enabling deducing the how in addition to the who, by introducing an approach to PM of hypertraces. Our method summarizes attacker behavior leading to SP invalidation, using PM as an additional analysis step based on (ARH) execution traces that invalidate SP.

4.1

Formalization

Below, we formalize the components relevant for applying PM to execution traces. PM concepts in this section are based on [30]. The analysis starts from execution traces w ∈ M ∗ (see Sect. 3), which we convert and aggregate to an event-log.

12

J. Figge et al.

We define the valid sets of execution traces L(S) that invalidate a specific SP S as L(S) = { w ∈ M ∗ ∣ ∃ c ∶ E → P ∶ w ⊧ / c S and w is valid for c }. Prior to aggregating execution traces into an event-log, we formalize the PM components relevant for our analysis. An event ϵ = ⟨a, id, t⟩ is an atomic activity occurrence that contains an activity name a ∈ A from a set of possible activities A, a case identifier id ∈ N that uniquely identifies the process instance to which the event is assigned, and a time-stamp t ∈ R. We let id(ϵ) = id be the identifier of an event ϵ = ⟨a, id, t⟩. The set of all possible events is denoted by E; every ϵ ∈ E is an atomic, timestamped activity occurrence tied to exactly one case identifier. An event trace σ is a finite sequence σ = ⟨ϵ1 , ϵ2 , . . . , ϵn ⟩ of events ϵi ∈ E for all 1 ≤ i ≤ n such that all events in σ belong to the same case; i.e., id(ϵi ) = id(ϵj ) for all 1 ≤ i, j ≤ n. Thus we also write id(σ) = id(ϵ1 ) for the case of the trace. An event trace denotes a single process instance and the set of all possible traces is denoted by E ∗ . An event-log L is a set L = {σ1 , σ2 , . . . , σn } of event traces. Different traces in an event-log represent unique cases: for any σ, σ ′ ∈ L with σ ≠ σ ′ we have id(σ) ≠ id(σ ′ ). A process mining algorithm MA maps event-logs to process models: MA∶ P(E ∗ ) → M, where P(E ∗ ) is the set of all event-logs (sets of event traces) and M is the set of all process models. We abstract internal details and treat MA as a black box that returns a model m ∈ M for a given log L. We define the function fa ∶ M → A to map every message m in an execution trace w ∈ M ∗ to an activity name fa (m) ∈ A. For modeling convenience, we simply let the activity label be the concatenation of the message components, so for a message m = ((s, r), c) we set fa (m) = s ○ r ○ c. Let fid ∶ M ∗ → N return a unique non-negative integer (identifier) for any execution trace w ∈ M ∗ . Finally, let ∆t > 0 be some arbitrary increment. We define the transformation T ∶ M ∗ → E ∗ to map an execution trace w = ⟨m1 , . . . , mn ⟩ and its unique case identifier i = fid (w) to an event trace T (w) = ⟨⟨fa (m1 ), i, 1 ⋅ ∆t ⟩, . . . , ⟨fa (mn ), i, n ⋅ ∆t ⟩⟩. Let L(S) = {w1 , . . . , wn } be the finite set of distinct execution traces obtained by formal verification that invalidate the SP S ∈ S. Each w ∈ L(S) is a distinct counterexample to S. To create a synthetic event-log SL(S), we transform the execution traces of L(S) via T to an event-log. The synthetic event-log SL(S) is the following set of event traces. SL(S) = { T (w) ∣ w ∈ L(S) } This event-log SL(S) is the input to the PM algorithm MA and yields a process model M = MA(SL(S)). T

MA

L(S) ÐÐ→ SL(S) ÐÐÐ→ M . In summary, our method bridges formal verification and process mining via a dedicated pipeline: counterexample traces L(S) are aggregated into a synthetic

Process-Mining for Formal Security Verification of Automotive Architectures

13

event-log SL(S) using the transformation function T , and a PM algorithm MA maps SL(S) to a process model M. 4.2

Classification and Limitations of the Approach

Our approach provides an exploratory contribution to applying PM for securityfocused insights from FV results. To our knowledge, there is no previous related work in this area (see Sect. 6). We leverage PM techniques to achieve high replay fitness and precision, so the discovered model reflects the event-logs and permits only observed behavior (or behavior representing filtered simplifications). Model simplicity should be balanced against the complexity needed to capture real adversarial behavior, which makes the generalization less critical. Furthermore, our overarching goal diverges from typical PM objectives. Our focus is on identifying behavior patterns, individual or collective, rather than scrutinizing entire process flows. Thus, depicting a complete, flawless process flow is out of scope. Understanding relevant (attacker) behavior suffices to address and mitigate potential invalidation.

5

Prototypical Implementation

Our prototypical implementation comprises two components (see Fig. 6). The first is Improved Adversary Compromise Tool (ImpACT), our contribution for in-depth ARH verification with Tamarin. The second is “Reconstructing Origins of Adversarial Damage”-Miner (ROAD-Miner), our contribution enabling PM on FV (hyper)traces. We demonstrate their practical use and the resulting substantial benefits through our case study. 5.1

“ImpACT”

We present our prototype Improved Adversary Compromise Tool (ImpACT), a direct evolution of our previous work Extended Adversary Compromise Tool (ExACT) [9]. ImpACT, built on a Node.js tech stack, enables fully automated ARH verificaFig. 5: ImpACT tion and further analysis by processing interim outputs. As a wrapper around Tamarin, Improved Adversary Compromise Tool (ImpACT) provides pre- and post-processing for formal models of ANAs and their protocols, including the SP to verify, using Tamarin’s security protocol theory format as input.

14

J. Figge et al.

RoadMINER Execution of ImpACT begins with ImpACT Architecture & Output and our verification orchestration algorithm Output and Protocol Model Visualization Visualization (see Sect. 3.3), generating a graph of all compromise, capability combinations and traversing it in preorder. For each Algorithmic ARH-Extraction Process Mining Verification scenario (a compromise plus capabilities), pre-processing enriches the base theory with the scenario; controlled veriPreprocessing Preprocessing Preprocessing Generated Postprocessing Postprocessing fication is then executed, and the rePostprocessing Event-Log sults are post-processed via parsing and evaluation. A feedback loop uses per(security)property post-processing results Enriched Enriched Verification Enriched Verification Event-Log Verification Model Model Results Model Results Conversion to guide the traversal. Consequently, we Results verify only those SPs whose lemmas have not already been marked invalid for a preControlled Tamarin Prover Controlled Controlled viously examined subset, improving runVerification Verification Verification time. After Tamarin verification, postprocessing converts Tamarin-specific output into a reusable, machine-readable forFig. 6: ImpACT / RoadMINER mat augmenting it with analyses and compromise details. Using this data, ARH verification is performed, assessing all SP across all scenarios. Within the web interface (see Fig. 5), ARH results are presented in a concise overview. The interface has two views: On the left, is a graph, where each node represents one ARH result for a given scenario (compromised entities, domains with capabilities) and lemma, and is colored accordingly. Nodes with similar characteristics and identical SP are clustered via a physics-based10 layout, and edges encode order relations between scenarios. On the right, a detailed table lists the ARH results per scenario, including sub-tables for evaluated SPs and their associated traces. The header bar enables filtering, e.g. by compromise size, included entities/domains, SPs, and ARH outcomes.

5.2

ROAD-Miner

“Reconstructing Origins of Adversarial Damage”-Miner (ROAD-Miner) follows ImpACT’s post-processing of Tamarin results (see Fig. 6) to generate synthetic event-logs that capture attacker behavior invalidating SP. Beyond attribution of compromise focused ARH analysis, our focus here is the sequence of steps required to violate a given SP. We use verification results, i.e. SP-invalidating traces, for event-log creation (see Sect. 4). Although our approach is tool-agnostic, Tamarin, which is utilized for the prototype, does not provide traces directly. However, we leverage Tamarin’s ability to render trace graphs, not only via DOT/Graphviz, but also via experimental JSON output. We provide a custom parser for the undocumented JSON 10

I.e. gravity simulation via d3js

Process-Mining for Formal Security Verification of Automotive Architectures

15

format enabling structured trace graph generation. For Eventlog Conversion, we first filter out traces that do not depict SP invalidation. We exploit that trace graphs are structured as a directed acyclic graph (DAG). Using the trace graphs of each invalidated lemma we utilize a topological sort to obtain ordered trace steps. We apply this to all counterexample traces of the respective SP and collect them into sets. From these sets of ordered steps we extract event-log–relevant information (e.g. activity, affected component). Each trace receives a unique ID and incremental time-stamps are assigned by step order and case. Finally, event-logs are exported as separate CSV files per SP. The PM analysis can be performed on these event-logs. For this step, we use Process Mining Toolkit (ProM) [1], though any PM tool suffices. In ProM, we e.g. apply interactive Data-aware Heuristics Mine (iDHM) [19] and Convert log to directly follows graph [16] modules after converting CSV to eXtensible Event Stream (XES) and applying filters. The ROAD-Miner results provide evaluations including directly-follows graphs (DFGs), dependency graphs, process trees, Petri nets, and causal nets, enabling users to trace attacker behavior leading to SP invalidation, i.e. the specific required steps.

5.3

Evaluation of Case Study

Our contributions, implemented in the prototypical tools ImpACT and ROAD-Miner, are assessed via a case study on uploading BMS data to the backend (see Sect. 2). We demonstrate their value by evaluating secrecy of transmitted data and authenticity of communication between the UseCase and Target (see Sect. 2.1) within the case study protocol. We analyze the results produced by ImpACT and presented in the web interface. Fig. 7: Filtered ImpACT Result-Graph Beyond the comprehensive tabular analysis (see Fig. 5), we highlight the concise, accessible presentation of ImpACT results (see Fig. 7)11 . For the result evaluation, we use the ability to filter ARH outcomes for Minimal Compromise Subset (purple), Single Point 11

Results are dynamically highlighted for readability, which the screenshot does not capture.

16

J. Figge et al.

of Failure (pink), and Necessary but not Sufficient (yellow).12 The results group into three clusters, reflecting the two verified lemmas (SP) and their invalidation by the respective compromises. The first cluster covers secrecy invalidation: confidentiality of UseCase provided data ∼n and TCU -provided information ∼oN , composed of Single Point of Failure ARH components. For this SP, each minimal compromise scenario has a single element, so secrecy can be breached by compromising just one component. This invalidation requires only read compromise, either of the ECUs TCU or Target, or the CarInternetFacing or Backend domains. This is expected in the protocol’s context: the TCU supplies the additional information for invalidation ∼oN only in later stages. Thus, only components at or beyond the TCU in the protocol execution suffice to breach the property. Write access is not required for knowledge extraction. In contrast to the secrecy SP, authenticity (see List. 1) results split into two clusters. The first cluster contains single-component elements whose compromise is necessary but not sufficient for invalidation. Notably, only compromising the UseCase is read -based; all other related scenarios are write-based. These appear in the second cluster, where each write-based compromise combined with the UseCase read-compromise forms a Minimal Compromise Subset that invalidates authenticity. The ability to evaluate multiple SPs simultaneously enables comparison of component involvement. It is apparent that, aside from the CarInternetFacing domain and the TCU appearing in multi-component compromises for authenticity, the components required for invalidation diverge. Furthermore, the common components require read permissions for secrecy but write permissions for authenticity. To break authenticity, the UseCase must be impersonated through injection of a malicious message. This requires a read-based compromise of the UseCase to extract its private key ∼pkU C and message injection in the protocol flow before TCU processing . Our extended ARH analysis with lemma authenticity_of_use_case: " All useCase target nonce #j . ImpACT supports analysis of comEndWithNonce(useCase,target,nonce)@j plex ANA, comparatively examining & (not Ex entity #r . PkiPrivatekeyReveal( entity)@r) component roles in invalidating mul==> Ex #i . tiple SPs under fine-grained permisInitiateTransport(useCase,target,nonce)@i & #i < #j " sions, answering “who is responsible?”. For secrecy, the behavior enabled by Listing 1: Authenticity Lemma the compromises that lead to SP invalidation, i.e. “how is the SP invalidated?”, can still be intuitively inferred. This already becomes challenging when evaluating authenticity. To address this, we extend the analysis with ROAD-Miner to identify behavior that invalidates message authenticity. We use PM to capture not only the “What” but also the “How” and synthesize adversarial behaviors across all compromise scenarios. ROAD-Miner uses ImpACT’s intermediate results as the 12

Compromise scenarios regularly verified and invalidated, as well as those labeled Never responsible for Compromise, are not of interest here.

Process-Mining for Formal Security Verification of Automotive Architectures

17

Fig. 8: Authenticity Violating Causal-Net basis for analysis, converting and aggregating them into synthetic event-logs. To ease processing, we provide logfiles in XES format. The event-log was then imported into PM software; we used the open-source ProM. We filtered the event-log to improve clarity. Steps irrelevant to invalidation (e.g. component initialization and PKI registration) were excluded, assumed established before protocol start and attacker actions. Afterward, we analyzed the authenticity eventlog with the iDHM module [19] and produced a Causal net (see Fig. 8) and a DFG (see Fig. 9). We condense all adversarial behavior that invalidates the authenticity SP, the adversarial and protocol steps of every invalidating compromise scenario trace in the Tamarin results, into the corresponding graphs via PM. This higher information density provides a comprehensive overview of all possible attacks and their required steps. Both graphs resemble bottomup PM approaches: the Fig. 9: Authenticity violating DFG Causal net uses the Flexible Heuristic Miner dependency heuristic and Cohen’s Kappa as the conditional heuristic with default settings, and the DFG is generated with event name as the event classifier and event classes as the variant.

18

J. Figge et al.

Using FV-based ARH analysis, we identify compromised components causing SP invalidation. The PM result graphs (see Fig. 8 and Fig. 9) clarify attacker intervention points for breaking authenticity in the protocol: Compromising the UseCase private key ∼pkU C is the invalidation prerequisite and start of the PM graphs. This matches the ARH “necessary but not sufficient” for UseCase read compromise. The adversary generates a spoofed nonce and signs it with the compromised key. Consistent with the ARH analysis, a write compromise of the TCU, DGW, or a vehicular domain (Inner or InternetFacing) lets the adversary inject the spoofed nonce, thus invalidating authenticity. This aligns with the ARH “Minimal Compromise Subset” results. The injection must occur before the TCU in the protocol run, since it adds additional information and also signs the UseCase nonce. Thereafter, the protocol proceeds normally.

5.4

Correctness and Limitations of Results

Our case study shows that our approach augments ARH evaluation of invalidation responsibility by illustrating attacker strategies with ROAD-Miner. We extend ARH analysis to comparative assessment of SPs and to attribute invalidation to specific, permission-based compromises. The complex analysis required is enabled by our verification-orchestration algorithm. We summarize and condense numerous non-machine-readable Tamarin traces with PM, producing clear and analyzable models. We provide a concise, machine-analyzable summary of invalidating traces using PM. The diverse results are, aside from minor details, content-identical and reflect actual behavior in the Tamarin traces. Our comparison of Tamarin-identified traces with the constructed process models supports performance assessment: There is no generalization; the model captures only attacker behavior in invalidating traces and maintains precision; only trace-contained activities are present. From a security architect’s perspective, we achieve a meaningful balance between simplicity (simplifying relations and filtering activities) and replay fitness (including all relevant steps as activities). Using PM requires trade-offs for complex relationships (e.g. many invalidating traces) in one graph. With effective representations (e.g. DFG) and pre-filtering irrelevant steps, density reduces significantly. A balance between complexity and simplified relationships must be maintained. Given expected partial compromises in automotive systems, focusing only on protecting critical components is insufficient to prevent SP invalidation. From a security architect’s perspective, PM graphs help evaluate attacker behavior and prevent invalidating steps. Beyond the alignment between compromise scenarios and attacker behavior observed in PM, correctness can be verified intuitively: First, identify invalidating attacker behavior in the PM results. Leverage PM features (e.g. DFGs) to highlight frequent invalidating behaviors. Then refine the protocol to prevent the behavior. Finally, rerun analysis with ImpACT and ROAD-Miner to confirm the cause for invalidation is no longer present.

Process-Mining for Formal Security Verification of Automotive Architectures

6

19

Related Work

Our contribution is a fine-grained model of attacker capabilities for component compromise in automotive network architectures. [7] use a similar approach, using “attacker privileges” to constrain actions (e.g. read, write) on components such as ECUs. In contrast to their focus on attack-tree generation, we utilize this approach to define a fine-grained attacker model and its capabilities for security protocol verification. We propose CRASH-model, an automotiveand cyber–physical system-specific extension of the DY-model adversary model that includes component and network-segment compromise and the injection or extraction of entity-internal knowledge. While [23] extends the DY-model for cyber–physical systems (hardware/physical attacks) and [3] integrates computational aspects, our approach captures properties crucial for modeling adversaries in automotive network architectures. Our contribution improves feasibility and performance (runtime and efficiency) in analyzing ARHs, focusing on security hyperproperties and network architectures via security protocol verification. In contrast to [10], which verifies HP of hardware modules using automata-based algorithms in HyperLTL and HyperCTL∗ , and [22], which proposes an algorithm for ∀∃-safety in infinite-state software systems, our work targets security-specific HP. Our work extracts extended security-property information, including adversarial attack patterns, via process mining (PM) of synthetic event-logs from security protocol verification traces. PM has been applied to security; [29] analyzed audit trails using the α-algorithm to detect violations. However, to our knowledge, no prior work uses outputs of formal or security protocol verification tools, focused on SPs, as input to PM. [5] use statistical model checking to simulate event-logs and PM to build a “diff” model highlighting discrepancies between expected and observed behavior. Their analysis targets real-world physical threat models (e.g. bank robberies) rather than network architectures or communication protocols. Prior work has explored the reverse direction: combining PM with formal methods. [28] employ event logs as input for model checking, specifically leveraging LTL-based techniques. [21] utilized PM to derive labeled transition systems. Furthermore, [13] integrate compliance rules into process models for checking and visualizing results directly within the model.

7

Conclusion and Outlook

This section concludes by distilling this work’s contributions and positioning them in terms of their significance and limitations. We propose a novel adversarial model CRASH-model C1, representing a strong active attacker tailored to fit and capture the specifics of the automotive domain. Consequently, we answered RQ1 and established part of the formal foundation for C2. Although the attacker model is tailored to automotive use cases due to domain-specific customization, it can be generalized to cyber–physical systems

20

J. Figge et al.

and, more broadly, to network architectures. We enable impact identification for component compromise C2 through improved ARH analysis, enabling finer-grained properties in more complex ANAs. We achieve this with a novel ARH verification-orchestration algorithm C2.1 that substantially extends Attack Resilience Hyperproperty (ARH) analysis capabilities to complex automotive network architectures (ANAs) and answers RQ2. It also enables comparative multi-security property (SP) analysis C2.2 (answering RQ3) and a fine-grained adversarial permission model C2.3 (answering RQ4). This extended ARH analysis attributes SP invalidations to permissions and components (entities, domains) in ANAs compromise scenarios. It reveals which component–permission combinations, as compromise scenarios, invalidate which SP. A limitation is that it identifies relevant components but not the attacker behavior causing invalidation. We address this limitation through comprehensive adversarial-behavior analysis C3, answering RQ5. Leveraging ARH verification results, we synthesize event-logs (C3.2) upon which we apply process mining (PM) (C3.1). This novel approach, bridging FV and PM, reveals attacker behavior leading to SPs invalidations, enabling systematic ANA hardening. To demonstrate real-world applicability of our contributions, we verify the security of an example ANA’s battery management system protocol via a case study. We operationalize C1–C3 with two prototypes, Improved Adversary Compromise Tool (ImpACT) and “Reconstructing Origins of Adversarial Damage”Miner (ROAD-Miner), comprising C4. The case study evaluation confirms substantial benefits for formal security verification of ANAs. However, given the prototype nature of the implementation, the full potential of ImpACT and ROADMiner has not yet been fully realized. We outline future research directions that build on our contributions and help remove current limitations. Fundamentally, ImpACT and ROAD-Miner can be integrated into a cohesive, fully automated tool, utilizing PM libraries, like e.g. PM4Py [4] rather than a GUI tool. We have intentionally deferred this to allow qualitative, case-specific log filtering during pre-processing. Further implementation is required for more advanced automation. This automation is a promising research direction, towards improving design and verification of ANAs and security protocols. Moreover, further insights could be gained through more sophisticated PM analyses. Rather than running analyses outside the PM toolchain, advanced evaluations could be embedded directly in the PM workflow, e.g. scoring, categorizing, and identifying attacker behavior patterns. Additionally, further exploration of extended PM applications is worthwhile. For instance, PM could support creating general or domain-specific artifacts (e.g. threat and risk analyses (TARAs)), deriving attack trees, and informing component-specific threat and risk assessments.

Disclosure of Interests. The authors have no competing interests to declare that are relevant to the content of this article.

Process-Mining for Formal Security Verification of Automotive Architectures

21

References 1. der Aalst, W.M.P., v., Dongen, B.F., v., Günther, C., Rozinat, A., Verbeek, H., Weijters, A.: ProM : The process mining toolkit. Proc. BPM 2009 Demonstr. Track BPMDemos 2009 Ulm Ger. Sept. 8 2009 pp. 1–4 (2009) 2. ASAM e.V.: Asam Sovd Service-Oriented Vehicle Diagnostics (Jun 2022) 3. Basin, D., Cremers, C.: Know Your Enemy: Compromising Adversaries in Protocol Analysis. ACM Trans. Inf. Syst. Secur. 17(2), 1–31 (Nov 2014). https://doi.org/10.1145/2658996 4. Berti, A., Van Zelst, S., Schuster, D.: PM4Py: A process mining library for Python. Software Impacts 17, 100556 (Sep 2023). https://doi.org/10.1016/j.simpa.2023.100556 5. Casaluce, R., Burratin, A., Chiaromonte, F., Lluch-Lafuente, A., Vandin, A.: Enhancing Threat Model Validation: A White-Box Approach based on Statistical Model Checking and Process Mining. In: DAMOCLES@AVI (Jan 2024) 6. Clarke, E.M., Klieber, W., Nováček, M., Zuliani, P.: Model Checking and the State Explosion Problem. In: Meyer, B., Nordio, M. (eds.) Tools for Practical Software Verification, vol. 7682, pp. 1–30. Springer Berlin Heidelberg, Berlin, Heidelberg (2012). https://doi.org/10.1007/978-3-642-35746-6_1 7. Dürrwang, J., Sommer, F., Kriesten, R.: Automation in Automotive Security by Using Attacker Privileges. In: ESCAR 2021 Eur. Frankfurt, Germany (Nov 2021) 8. Figge, J., Knuplesch, D.: Applications of Formal Verification Techniques for Security in Automotive Diagnostics - a Literature-Survey (Nov 2024) 9. Figge, J., Knuplesch, D., Maletti, A., Zuvic, D.: Attack Resilience Hyperproperties: Formal Security Analysis of (Automotive) Network Architectures Under Active Compromise. In: Bianculli, D., Gómez-Martínez, E. (eds.) Software Engineering and Formal Methods, vol. 16192, pp. 15–33. Springer Nature Switzerland, Cham (2026). https://doi.org/10.1007/978-3-032-10444-1_2 10. Finkbeiner, B., Rabe, M.N., Sánchez, C.: Algorithms for Model Checking HyperLTL and HyperCTL$$^*$$. In: Kroening, D., Păsăreanu, C.S. (eds.) Comput. Aided Verification. pp. 30–48. Springer International Publishing, Cham (2015). https://doi.org/10.1007/978-3-319-21690-4_3 11. Girol, G., Hirschi, L., Sasse, R., Jackson, D., Cremers, C., Basin, D.: A Spectral Analysis of Noise: A Comprehensive, Automated, Formal Analysis of DiffieHellman Protocols. In: 29th USENIX Security Symposium (USENIX Security 20). pp. 1857–1874 (2020) 12. Huelsewies, M.: Server-Based Architecture - Transformation in Products (Jul 2021) 13. Knuplesch, D., Ly, L.T., Rinderle-Ma, S., Pfeifer, H., Dadam, P.: On Enabling Data-Aware Compliance Checking of Business Process Models. In: Parsons, J., Saeki, M., Shoval, P., Woo, C., Wand, Y. (eds.) Conceptual Modeling – ER 2010, vol. 6412, pp. 332–346. Springer Berlin Heidelberg, Berlin, Heidelberg (2010). https://doi.org/10.1007/978-3-642-16373-9_24 14. Lampe, B., Meng, W.: Intrusion Detection in the Automotive Domain: A Comprehensive Review. IEEE Commun. Surv. Tutor. 25(4), 2356–2426 (2023). https://doi.org/10.1109/COMST.2023.3309864 15. Lauser, T., Zelle, D., Krauß, C.: Security Analysis of Automotive Protocols. Comput. Sci. Cars Symp. pp. 1–12 (Dec 2020). https://doi.org/10.1145/3385958.3430482 16. Leemans, S.J.J., Fahland, D., van der Aalst, W.M.P.: Scalable process discovery and conformance checking. Softw Syst Model 17(2), 599–631 (May 2018). https://doi.org/10.1007/s10270-016-0545-x

22

J. Figge et al.

17. Lohmiller, N., Kaniewski, S., Menth, M., Heer, T.: A Survey of Post-Quantum Cryptography Migration in Vehicles. IEEE Access 13, 10160–10176 (2025). https://doi.org/10.1109/ACCESS.2025.3528562 18. Lowe, G.: A hierarchy of authentication specifications. In: Proc. 10th Comput. Secur. Found. Workshop. pp. 31–43. IEEE Comput. Soc. Press, Rockport, MA, USA (1997). https://doi.org/10.1109/CSFW.1997.596782 19. Mannhardt, F., De Leoni, M., Reijers, H.A.: Heuristic mining revamped: An interactive, data-aware, and conformance-aware miner. In: 15th Int. Conf. Bus. Process Manag. BPM 2017. pp. 1–5. CEUR-WS. org (2017) 20. Marksteiner, S.F., Schmittner, C., Christl, K., Nickovic, D., Sjödin, M., Sirjani, M.: From TARA to Test: Automated Automotive Cybersecurity Test Generation Out of Threat Modeling. In: 7th CSCS. pp. 1–10. ACM, Darmstadt Germany (Dec 2023). https://doi.org/10.1145/3631204.3631864 21. Martinelli, F., Mercaldo, F., Nardone, V., Orlando, A., Santone, A., Vaglini, G.: Model Checking Based Approach for Compliance Checking. Inf. Technol. Control 48(2), 278–298 (Jun 2019). https://doi.org/10.5755/j01.itc.48.2.21724 22. Nießen, T., Weissenbacher, G.: Finding counterexamples to ∀∃ hyperproperties (Jan 2024). https://doi.org/10.34726/5455 23. Rocchetto, M., Tippenhauer, N.O.: CPDY: Extending the Dolev-Yao Attacker with Physical-Layer Interactions (Jul 2016). https://doi.org/10.48550/arXiv.1607.02562 24. Seo, J., Kwak, J., Kim, S.: Formally Verified Software Update Management System in Automotive. Proc. Inaug. Int. Symp. Veh. Secur. Priv. (2023). https://doi.org/10.14722/vehiclesec.2023.23087 25. Seo, J., Kwak, J., Kim, S.: Formally Verified Software Update Management System in Automotive. Veh. 2023 (2023). https://doi.org/10.14722/vehiclesec.2023.23087 26. Uptane Standards Group: Uptane: Securing delivery of software updates for ground vehicles. https://uptane.org/assets/files/uptane_first_whitepaper_7821efd12526ce69d174eb215e0ecdad29dd.pdf (Jun 2021) 27. Vamour, C.: Security of Over-the-Air Software Update towards SDV (Sep 2023) 28. van der Aalst, W.M.P., de Beer, H.T., van Dongen, B.F.: Process Mining and Verification of Properties: An Approach Based on Temporal Logic. In: Meersman, R., Tari, Z. (eds.) Move Meaningful Internet Syst. 2005 CoopIS DOA ODBASE. pp. 130–147. Springer, Berlin, Heidelberg (2005). https://doi.org/10.1007/11575771_11 29. van der Aalst, W.M.P., de Medeiros, A.K.A.: Process Mining and Security: Detecting Anomalous Process Executions and Checking Process Conformance. Electronic Notes in Theoretical Computer Science 121, 3–21 (Feb 2005). https://doi.org/10.1016/j.entcs.2004.10.013 30. Van Der Aalst, W.M.P., Carmona, J. (eds.): Process Mining Handbook, Lecture Notes in Business Information Processing, vol. 448. Springer International Publishing, Cham (2022). https://doi.org/10.1007/978-3-031-08848-3 31. Yu, S.: Regular Languages. In: Rozenberg, G., Salomaa, A. (eds.) Handbook of Formal Languages: Volume 1 Word, Language, Grammar, pp. 41–110. Springer, Berlin, Heidelberg (1997). https://doi.org/10.1007/978-3-642-59136-5_2