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

Andreas Maletti; David Knuplesch; Dragan Zuvic; Julius Figge

arxiv: 2604.21606 · v2 · submitted 2026-04-23 · 💻 cs.CR

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

Julius Figge , David Knuplesch , Andreas Maletti , Dragan Zuvic This is my paper

Pith reviewed 2026-05-09 21:22 UTC · model grok-4.3

classification 💻 cs.CR

keywords process mininghypertracesformal security verificationautomotive network architecturesattack resilience hyperpropertiessecurity protocolscounterexample analysisadversary models

0 comments

The pith

A pipeline integrates Attack Resilience Hyperproperties verification with process mining on counterexample traces to scale security analysis for automotive networks.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

This paper tries to establish that formal security verification can be made scalable for realistic automotive network architectures through a combination of an orchestration algorithm for ARH checks and process mining applied to the resulting hypertrace counterexamples. The goal is to not only check if security properties hold but also to automatically aggregate and attribute the attacker behaviors that invalidate them, providing insight into root causes and specific attack paths. A sympathetic reader would care if true because connected vehicles face sophisticated threats from external entities, yet existing methods cannot handle the scale or give actionable explanations for failures in protocols such as battery management data transmission. The method includes a strong active adversary model tailored to the domain and comparative attribution to component compromises.

Core claim

The central claim is that utilizing ARH counterexample traces for process mining allows systematic identification and aggregation of attacker behavior causing security property invalidations, while a verification-orchestration algorithm extends the reach of ARH-based verification to larger architectures. This enables in-depth understanding of root causes and attack paths, along with methods for attributing invalidations to fine-grained component compromises, as shown in a case study on secure transmission of battery management system data.

What carries the argument

Process mining applied to ARH counterexample hypertraces, orchestrated through a new verification algorithm that scales formal checks and supports attribution of failures.

Load-bearing premise

That the hypertraces produced by ARH verification contain sufficient information to be mined into accurate and actionable representations of real attacker behavior in automotive settings.

What would settle it

Demonstrating the method on an automotive network where either the orchestration algorithm cannot complete verification within feasible time or the process-mined models fail to identify attack paths that match known vulnerabilities.

Figures

Figures reproduced from arXiv: 2604.21606 by Andreas Maletti, David Knuplesch, Dragan Zuvic, Julius Figge.

**Figure 1.** Figure 1: CRASH-model At its core, the CRASHmodel introduces two key changes. These changes focus on entity and domain compromise and align with our threat model, which considers physical 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 … view at source ↗

**Figure 2.** Figure 2: Exemplary ANA Our exemplary ANA (see [PITH_FULL_IMAGE:figures/full_fig_p005_2.png] view at source ↗

**Figure 3.** Figure 3: BMS Synchronization Protocol The BMS UseCase monitors relevant battery parameters to be transmitted to the backend and stores them as data ∼n. The data ∼n is signed by the BMS with its private key ∼pkUC and sent to the T CU via the DGW. The T CU adds vehicle-specific information ∼oN and signs a hash of the combined data ⟨∼n, ∼oN⟩ with its private key ∼pkT. The data is then transmitted to the manufact… view at source ↗

**Figure 4.** Figure 4: Compromise Graph for ARHVerification Traversal In our case study, in which we have 4 entities (ECUs), 3 domains, 2 permissions, and 2 SP, we require the verification of (2 2 ) 4+3 ⋅ 2 = 32, 768 lemmas (i.e. individual SPs to be validated against specific compromise scenarios). Even under the optimistic (and unrealistic) assumption that each verification takes only one second,9 the total runtime is ro… view at source ↗

**Figure 5.** Figure 5: 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 verification and further analysis by processing interim outputs. As a wrapper around Tamarin, Improved Adversary Compromise Tool (ImpACT) provides pre- and post-processin… view at source ↗

**Figure 6.** Figure 6: ImpACT / RoadMINER Execution of ImpACT begins with our verification orchestration algorithm (see Sect. 3.3), generating a graph of all compromise, capability combinations and traversing it in preorder. For each scenario (a compromise plus capabilities), pre-processing enriches the base theory with the scenario; controlled verification is then executed, and the results are post-processed via parsing and… view at source ↗

**Figure 7.** Figure 7: Filtered ImpACT Result-Graph 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 … view at source ↗

**Figure 8.** Figure 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 estab… view at source ↗

**Figure 9.** Figure 9: Authenticity violating DFG Afterward, we analyzed the authenticity eventlog with the iDHM module [19] and produced a Causal net (see [PITH_FULL_IMAGE:figures/full_fig_p017_9.png] view at source ↗

read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

They run process mining on ARH counterexample hypertraces to attribute security violations to specific compromises in automotive networks and back it with a prototype on battery management data.

read the letter

The paper's main contribution is extending Attack Resilience Hyperproperties verification with an orchestration algorithm for scaling and then feeding the resulting counterexample hypertraces into process mining. This produces aggregated models of attacker behavior that explain which component compromises invalidate the security properties. The approach is demonstrated on a concrete automotive case: secure transmission of battery management system data under a domain-specific active adversary model that accounts for persistent external connectivity and on-board compute power. They also ship a prototype, which moves the work beyond pure description. The integration of process mining with hypertraces is new relative to the ARH literature they cite and gives a practical way to turn raw counterexamples into comparative root-cause insights. That part is useful for anyone who has run formal checks and then struggled to interpret the traces. The soft spots are in the level of detail provided on the orchestration algorithm itself and on the quantitative outcomes of the mining step. It is not yet clear how much state-space reduction the orchestration actually delivers on networks larger than the case study, or how closely the mined process models match observable real-world attack paths. The case study is a solid existence proof but remains narrow in scope. Readers working on formal methods for embedded or automotive security will find the pipeline worth examining. It is the kind of paper that combines two established techniques in a domain-specific way and supplies enough implementation to be worth refereeing. I would send it to review rather than desk reject.

Referee Report

0 major / 2 minor

Summary. The paper introduces a domain-specific strong active adversary model for automotive networks and substantially extends Attack Resilience Hyperproperties (ARHs) by adding a verification-orchestration algorithm. It further integrates formal verification with process mining applied to ARH counterexample hypertraces, enabling systematic identification and aggregation of attacker behaviors that invalidate security properties, along with comparative attribution of invalidations to component compromises. The approach is demonstrated via a prototype implementation and a case study on secure battery-management-system data transmission within an automotive network architecture.

Significance. If the pipeline and prototype perform as described, the work offers a meaningful advance by bridging formal hyperproperty verification with process mining to produce actionable models of attack paths and root causes in complex automotive systems. The concrete prototype and end-to-end case study on battery-management data transmission constitute a strength, supplying a falsifiable demonstration rather than purely theoretical claims.

minor comments (2)

[Abstract] Abstract: the phrase 'ne-grained' is a typographical error and should read 'fine-grained'.
[Abstract] The abstract states that the orchestration algorithm renders verification scalable, yet provides no quantitative metrics (e.g., trace volume handled, runtime, or comparison against baseline ARH verification); adding such data from the case study would strengthen the central scalability claim.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive assessment of our work, the recognition of its significance in bridging formal hyperproperty verification with process mining for automotive security analysis, and the recommendation for minor revision. We appreciate the constructive feedback and will incorporate all suggested improvements in the revised manuscript.

Circularity Check

0 steps flagged

No significant circularity; methodological extensions on prior ARH base

full rationale

The paper describes a pipeline that extends Attack Resilience Hyperproperties (ARHs) with a new verification-orchestration algorithm, attribution methods, and process mining on counterexample hypertraces. No equations, derivations, or fitted parameters are presented that reduce to self-definition or tautology. The central claims rest on concrete prototype implementation and case-study demonstration rather than any self-referential reduction. Self-citation to prior ARH work is present but not load-bearing for the new contributions, which are independently described and evaluated.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 2 invented entities

Abstract-only information yields minimal ledger entries; the work relies on standard formal verification assumptions and introduces new algorithmic components without independent evidence.

axioms (2)

domain assumption Standard assumptions of formal security protocol verification hold for automotive networks
The paper extends ARH-based verification, presupposing the underlying formal framework.
domain assumption A strong active adversary model is appropriate for internet-connected vehicles
Explicitly introduced as tailored to the automotive domain.

invented entities (2)

Verification-orchestration algorithm no independent evidence
purpose: To extend ARH verification for scalability in complex networks
New algorithmic component described for orchestrating verification.
Process-mining pipeline on ARH hypertraces no independent evidence
purpose: To aggregate attacker behaviors and attribute compromises
Novel integration presented as the core methodological advance.

pith-pipeline@v0.9.0 · 5496 in / 1422 out tokens · 43446 ms · 2026-05-09T21:22:13.480092+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

30 extracted references · 30 canonical work pages

[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)

work page 2009
[2]

ASAM e.V.: Asam Sovd Service-Oriented Vehicle Diagnostics (Jun 2022)

work page 2022
[3]

ACM Trans

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

work page doi:10.1145/2658996 2014
[4]

PM4Py: A process mining library for Python.Softw

Berti, A., Van Zelst, S., Schuster, D.: PM4Py: A process min- ing library for Python. Software Impacts17, 100556 (Sep 2023). https://doi.org/10.1016/j.simpa.2023.100556

work page doi:10.1016/j.simpa.2023.100556 2023
[5]

In: DAMOCLES@AVI (Jan 2024)

Casaluce, R., Burratin, A., Chiaromonte, F., Lluch-Lafuente, A., Vandin, A.: En- hancing Threat Model Validation: A White-Box Approach based on Statistical Model Checking and Process Mining. In: DAMOCLES@AVI (Jan 2024)

work page 2024
[6]

In: Meyer, B., Nordio, M

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

work page doi:10.1007/978-3-642-35746-6_1 2012
[7]

In: ESCAR 2021 Eur

Dürrwang, J., Sommer, F., Kriesten, R.: Automation in Automotive Security by Using Attacker Privileges. In: ESCAR 2021 Eur. Frankfurt, Germany (Nov 2021)

work page 2021
[8]

Figge, J., Knuplesch, D.: Applications of Formal Verification Techniques for Secu- rity in Automotive Diagnostics - a Literature-Survey (Nov 2024)

work page 2024
[9]

In: Bianculli, D., Gómez-Martínez, E

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...

work page doi:10.1007/978-3-032-10444-1_2 2026
[10]

In: Kroening, D., Păsăreanu, C.S

Finkbeiner, B., Rabe, M.N., Sánchez, C.: Algorithms for Model Checking Hyper- LTL 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

work page doi:10.1007/978-3-319-21690-4_3 2015
[11]

In: 29th USENIX Security Symposium (USENIX Security 20)

Girol, G., Hirschi, L., Sasse, R., Jackson, D., Cremers, C., Basin, D.: A Spec- tral Analysis of Noise: A Comprehensive, Automated, Formal Analysis of Diffie- Hellman Protocols. In: 29th USENIX Security Symposium (USENIX Security 20). pp. 1857–1874 (2020)

work page 2020
[12]

Huelsewies, M.: Server-Based Architecture - Transformation in Products (Jul 2021)

work page 2021
[13]

In: Parsons, J., Saeki, M., Shoval, P., Woo, C., Wand, Y

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

work page doi:10.1007/978-3-642-16373-9_24 2010
[14]

IEEE Commun

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

work page doi:10.1109/comst.2023.3309864 2023
[15]

Lauser, T., Zelle, D., Krauß, C.: Security Analysis of Automo- tive Protocols. Comput. Sci. Cars Symp. pp. 1–12 (Dec 2020). https://doi.org/10.1145/3385958.3430482

work page doi:10.1145/3385958.3430482 2020
[16]

Softw Syst Model17(2), 599–631 (May 2018)

Leemans, S.J.J., Fahland, D., van der Aalst, W.M.P.: Scalable process discov- ery and conformance checking. Softw Syst Model17(2), 599–631 (May 2018). https://doi.org/10.1007/s10270-016-0545-x 22 J. Figge et al

work page doi:10.1007/s10270-016-0545-x 2018
[17]

IEEE Access13, 10160–10176 (2025)

Lohmiller, N., Kaniewski, S., Menth, M., Heer, T.: A Survey of Post-Quantum Cryptography Migration in Vehicles. IEEE Access13, 10160–10176 (2025). https://doi.org/10.1109/ACCESS.2025.3528562

work page doi:10.1109/access.2025.3528562 2025
[18]

In: Proc

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

work page doi:10.1109/csfw.1997.596782 1997
[19]

In: 15th Int

Mannhardt, F., De Leoni, M., Reijers, H.A.: Heuristic mining revamped: An inter- active, data-aware, and conformance-aware miner. In: 15th Int. Conf. Bus. Process Manag. BPM 2017. pp. 1–5. CEUR-WS. org (2017)

work page 2017
[20]

In: 7th CSCS

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

work page doi:10.1145/3631204.3631864 2023
[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

work page doi:10.5755/j01.itc.48.2.21724 2019
[22]

https://doi.org/10.34726/5455

Nießen, T., Weissenbacher, G.: Finding counterexamples to∀∃hyperproperties (Jan 2024). https://doi.org/10.34726/5455

work page doi:10.34726/5455 2024
[23]

Rocchetto,M.,Tippenhauer,N.O.:CPDY:ExtendingtheDolev-YaoAttackerwith Physical-LayerInteractions(Jul2016).https://doi.org/10.48550/arXiv.1607.02562

work page doi:10.48550/arxiv.1607.02562
[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

work page doi:10.14722/vehiclesec.2023.23087 2023
[26]

https://uptane.org/assets/files/uptane_first_whitepaper_7821- efd12526ce69d174eb215e0ecdad29dd.pdf (Jun 2021)

Uptane Standards Group: Uptane: Securing delivery of software updates for ground vehicles. https://uptane.org/assets/files/uptane_first_whitepaper_7821- efd12526ce69d174eb215e0ecdad29dd.pdf (Jun 2021)

work page 2021
[27]

Vamour, C.: Security of Over-the-Air Software Update towards SDV (Sep 2023)

work page 2023
[28]

In: Meersman, R., Tari, Z

van der Aalst, W.M.P., de Beer, H.T., van Dongen, B.F.: Process Min- ing 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

work page doi:10.1007/11575771_11 2005
[29]

Electronic Notes in Theoretical Computer Science121, 3–21 (Feb 2005)

van der Aalst, W.M.P., de Medeiros, A.K.A.: Process Mining and Secu- rity: Detecting Anomalous Process Executions and Checking Process Confor- mance. Electronic Notes in Theoretical Computer Science121, 3–21 (Feb 2005). https://doi.org/10.1016/j.entcs.2004.10.013

work page doi:10.1016/j.entcs.2004.10.013 2005
[30]

https://doi.org/10.1007/978-3-031-08848-3{\_}9

Van Der Aalst, W.M.P., Carmona, J. (eds.): Process Mining Handbook, Lecture Notes in Business Information Processing, vol. 448. Springer International Pub- lishing, Cham (2022). https://doi.org/10.1007/978-3-031-08848-3

work page doi:10.1007/978-3-031-08848-3 2022
[31]

In: Rozenberg, G., Salomaa, A

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

work page doi:10.1007/978-3-642-59136-5_2 1997

[1] [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)

work page 2009

[2] [2]

ASAM e.V.: Asam Sovd Service-Oriented Vehicle Diagnostics (Jun 2022)

work page 2022

[3] [3]

ACM Trans

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

work page doi:10.1145/2658996 2014

[4] [4]

PM4Py: A process mining library for Python.Softw

Berti, A., Van Zelst, S., Schuster, D.: PM4Py: A process min- ing library for Python. Software Impacts17, 100556 (Sep 2023). https://doi.org/10.1016/j.simpa.2023.100556

work page doi:10.1016/j.simpa.2023.100556 2023

[5] [5]

In: DAMOCLES@AVI (Jan 2024)

Casaluce, R., Burratin, A., Chiaromonte, F., Lluch-Lafuente, A., Vandin, A.: En- hancing Threat Model Validation: A White-Box Approach based on Statistical Model Checking and Process Mining. In: DAMOCLES@AVI (Jan 2024)

work page 2024

[6] [6]

In: Meyer, B., Nordio, M

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

work page doi:10.1007/978-3-642-35746-6_1 2012

[7] [7]

In: ESCAR 2021 Eur

Dürrwang, J., Sommer, F., Kriesten, R.: Automation in Automotive Security by Using Attacker Privileges. In: ESCAR 2021 Eur. Frankfurt, Germany (Nov 2021)

work page 2021

[8] [8]

Figge, J., Knuplesch, D.: Applications of Formal Verification Techniques for Secu- rity in Automotive Diagnostics - a Literature-Survey (Nov 2024)

work page 2024

[9] [9]

In: Bianculli, D., Gómez-Martínez, E

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...

work page doi:10.1007/978-3-032-10444-1_2 2026

[10] [10]

In: Kroening, D., Păsăreanu, C.S

Finkbeiner, B., Rabe, M.N., Sánchez, C.: Algorithms for Model Checking Hyper- LTL 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

work page doi:10.1007/978-3-319-21690-4_3 2015

[11] [11]

In: 29th USENIX Security Symposium (USENIX Security 20)

Girol, G., Hirschi, L., Sasse, R., Jackson, D., Cremers, C., Basin, D.: A Spec- tral Analysis of Noise: A Comprehensive, Automated, Formal Analysis of Diffie- Hellman Protocols. In: 29th USENIX Security Symposium (USENIX Security 20). pp. 1857–1874 (2020)

work page 2020

[12] [12]

Huelsewies, M.: Server-Based Architecture - Transformation in Products (Jul 2021)

work page 2021

[13] [13]

In: Parsons, J., Saeki, M., Shoval, P., Woo, C., Wand, Y

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

work page doi:10.1007/978-3-642-16373-9_24 2010

[14] [14]

IEEE Commun

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

work page doi:10.1109/comst.2023.3309864 2023

[15] [15]

Lauser, T., Zelle, D., Krauß, C.: Security Analysis of Automo- tive Protocols. Comput. Sci. Cars Symp. pp. 1–12 (Dec 2020). https://doi.org/10.1145/3385958.3430482

work page doi:10.1145/3385958.3430482 2020

[16] [16]

Softw Syst Model17(2), 599–631 (May 2018)

Leemans, S.J.J., Fahland, D., van der Aalst, W.M.P.: Scalable process discov- ery and conformance checking. Softw Syst Model17(2), 599–631 (May 2018). https://doi.org/10.1007/s10270-016-0545-x 22 J. Figge et al

work page doi:10.1007/s10270-016-0545-x 2018

[17] [17]

IEEE Access13, 10160–10176 (2025)

Lohmiller, N., Kaniewski, S., Menth, M., Heer, T.: A Survey of Post-Quantum Cryptography Migration in Vehicles. IEEE Access13, 10160–10176 (2025). https://doi.org/10.1109/ACCESS.2025.3528562

work page doi:10.1109/access.2025.3528562 2025

[18] [18]

In: Proc

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

work page doi:10.1109/csfw.1997.596782 1997

[19] [19]

In: 15th Int

Mannhardt, F., De Leoni, M., Reijers, H.A.: Heuristic mining revamped: An inter- active, data-aware, and conformance-aware miner. In: 15th Int. Conf. Bus. Process Manag. BPM 2017. pp. 1–5. CEUR-WS. org (2017)

work page 2017

[20] [20]

In: 7th CSCS

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

work page doi:10.1145/3631204.3631864 2023

[21] [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

work page doi:10.5755/j01.itc.48.2.21724 2019

[22] [22]

https://doi.org/10.34726/5455

Nießen, T., Weissenbacher, G.: Finding counterexamples to∀∃hyperproperties (Jan 2024). https://doi.org/10.34726/5455

work page doi:10.34726/5455 2024

[23] [23]

Rocchetto,M.,Tippenhauer,N.O.:CPDY:ExtendingtheDolev-YaoAttackerwith Physical-LayerInteractions(Jul2016).https://doi.org/10.48550/arXiv.1607.02562

work page doi:10.48550/arxiv.1607.02562

[24] [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

work page doi:10.14722/vehiclesec.2023.23087 2023

[25] [26]

https://uptane.org/assets/files/uptane_first_whitepaper_7821- efd12526ce69d174eb215e0ecdad29dd.pdf (Jun 2021)

Uptane Standards Group: Uptane: Securing delivery of software updates for ground vehicles. https://uptane.org/assets/files/uptane_first_whitepaper_7821- efd12526ce69d174eb215e0ecdad29dd.pdf (Jun 2021)

work page 2021

[26] [27]

Vamour, C.: Security of Over-the-Air Software Update towards SDV (Sep 2023)

work page 2023

[27] [28]

In: Meersman, R., Tari, Z

van der Aalst, W.M.P., de Beer, H.T., van Dongen, B.F.: Process Min- ing 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

work page doi:10.1007/11575771_11 2005

[28] [29]

Electronic Notes in Theoretical Computer Science121, 3–21 (Feb 2005)

van der Aalst, W.M.P., de Medeiros, A.K.A.: Process Mining and Secu- rity: Detecting Anomalous Process Executions and Checking Process Confor- mance. Electronic Notes in Theoretical Computer Science121, 3–21 (Feb 2005). https://doi.org/10.1016/j.entcs.2004.10.013

work page doi:10.1016/j.entcs.2004.10.013 2005

[29] [30]

https://doi.org/10.1007/978-3-031-08848-3{\_}9

Van Der Aalst, W.M.P., Carmona, J. (eds.): Process Mining Handbook, Lecture Notes in Business Information Processing, vol. 448. Springer International Pub- lishing, Cham (2022). https://doi.org/10.1007/978-3-031-08848-3

work page doi:10.1007/978-3-031-08848-3 2022

[30] [31]

In: Rozenberg, G., Salomaa, A

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

work page doi:10.1007/978-3-642-59136-5_2 1997