Secure Conformance Checking using Token-based Replay and Homomorphic Encryption

1. Problem Statement

Conformance checking is a core operation in process mining that compares an event log (actual behavior) against a process model (expected behavior) to identify deviations. Traditionally, this requires both the model owner and the log owner to share their data in plaintext with a business analyst.

However, in scenarios such as custom manufacturing or cross-organizational collaborations, parties often wish to protect sensitive information:

• Model Owners may want to keep their proprietary process logic (e.g., production workflows) secret.
• Log Owners may want to protect sensitive execution data (e.g., customer order details) from the model owner.

The challenge is to perform conformance checking (specifically token-based replay) on encrypted data without revealing the underlying process model or the event log to the other party, while maintaining the ability to calculate fitness metrics (deviations).

2. Methodology

The authors propose a secure framework using Homomorphic Encryption (HE) and a reformulation of the token-based replay algorithm using linear algebra (matrix and vector operations).

Core Concepts

• Token-Based Replay: An algorithm that "replays" event log traces on a Petri net. It tracks tokens consumed, produced, missing (to enable transitions), and remaining (leftover at the end).
• Homomorphic Encryption (HE): Specifically, the authors utilize Zama's Concrete (based on TFHE), which supports arithmetic operations (addition, subtraction, multiplication) and comparisons (min/max) on encrypted integers without decryption.
• Client-Server Architecture:
  • Client (Log Owner): Holds the event log. Encrypts the current marking and the next event (transition) to be fired. Sends these to the server.
  • Server (Model Owner): Holds the Petri net model. Performs the replay step on encrypted data using precomputed matrices. Returns the new encrypted marking and local counters.
  • Privacy: The server never sees the plaintext log; the client never sees the plaintext model structure beyond what is inferred from the replay.

Algorithmic Reformulation

To make token-based replay compatible with HE, the authors replaced the traditional "token game" (which relies on conditional logic and branching) with matrix multiplication and vector operations.

1. Precomputation (Server Side):

   • The Petri net is converted into an Incidence Matrix ($N$).
   • A Dynamics Matrix ($E$) is constructed to represent all possible "enablements" (combinations of current markings and transitions).
   • A Firing Sequences Matrix ($S$) stores the Parikh vectors (transition counts) for valid firing sequences.
   • A Preset Matrix ($P$) stores the input places for every transition.

2. Replay Step (Secure Execution):

   • Enablement Check: The client sends the encrypted current marking ($M$) and the encrypted next event ($t$). The server computes a selector vector ($sel$) using matrix multiplication: $E \cdot [M, t]^T$. This determines if the transition is enabled directly or requires silent transitions ($\tau$).
   • Handling Missing Tokens: If the transition is not enabled, the algorithm calculates the "missing tokens" ($\pi$) required from the preset matrix $P$.
   • Unified Marking Update: To avoid conditional if/else statements (which leak information in HE), the authors combine the "fitting" and "unfitting" logic into a single equation:
     $$M' = (M + N \cdot \sigma^T) \cdot \text{sum}(sel) + (M + \pi^T + N \cdot t^T) \cdot (1 - \text{sum}(sel))$$
     Here, $\text{sum}(sel)$ acts as a binary switch (1 if enabled, 0 if not).
   • Counter Calculation: The algorithm computes missing ($m$), consumed ($c$), produced ($p$), and remaining ($r$) tokens using vector differences and conditional masking (multiplying by 0 or 1 based on the switch).

3. Fitness Calculation:

   • After processing all events in a trace, the client decrypts the final counters and computes the fitness score using the standard formula:
     $$f = \frac{1}{2}\left(1 - \frac{m}{c}\right) + \frac{1}{2}\left(1 - \frac{r}{p}\right)$$

3. Key Contributions

1. First Secure Token-Based Replay: This is the first work to apply homomorphic encryption specifically to the token-based replay conformance checking algorithm.
2. Matrix-Based Reformulation: The authors successfully transformed the non-linear, state-dependent token game into a linear algebraic formulation suitable for homomorphic encryption, eliminating the need for branching logic.
3. Privacy-Preserving Architecture: A client-server protocol where the model owner processes encrypted traces without learning the trace content, and the log owner learns nothing about the model structure beyond the replay results.
4. Implementation & Evaluation: A working prototype implemented in Python using Zama's Concrete framework, demonstrating the feasibility of the approach.

4. Results

The authors evaluated the prototype using a synthetic event log and a Petri net model (from the book Process Mining and PM4Py tutorials).

• Performance (Clear vs. Encrypted):
  • Clear Data (CLR): Execution time was in milliseconds.
  • Encrypted Data (SEC): Execution times ranged from 7.8 to 15.8 seconds for traces without token counter calculations.
  • Encrypted with Counters (SEC+): Execution times ranged from 19.3 to 37.4 seconds.
• Optimization Insights:
  • An initial version that computed counters ($p, c, m, r$) inside the server-side function took 35 to 84 minutes.
  • The authors identified that this slowdown was due to the HE compiler (Concrete) defaulting to 16-bit integers for return values, causing massive overhead. By moving counter accumulation to the client side (decrypting intermediate results), they reduced the time to under 40 seconds.
• Scalability: The method successfully handled traces of varying lengths (4 to 13 events) and both fitting and non-fitting traces.

5. Significance and Future Work

• Significance: The paper proves that secure conformance checking is practically feasible. It enables organizations to verify process compliance (e.g., in supply chains or healthcare) without compromising trade secrets or patient privacy. The shift from branching logic to matrix operations is a critical theoretical contribution for applying HE to process mining.
• Limitations:
  • Performance: While under a minute, the encrypted execution is significantly slower than plaintext (orders of magnitude).
  • Token Flooding: The current implementation does not fully address the "token flooding" issue (where places accumulate >1 token) in the encrypted domain.
  • Precision: The reliance on integer precision in HE frameworks limits the complexity of operations.
• Future Directions:
  • Testing with real-life event logs.
  • Addressing token flooding in the encrypted domain.
  • Exploring other HE platforms to optimize the trade-off between precision and performance.
  • Implementing a full client-server network version to analyze communication costs.

In conclusion, the paper provides a robust proof-of-concept for secure process mining, demonstrating that homomorphic encryption can be effectively adapted to complex algorithmic tasks like token-based replay through algebraic reformulation.