Secure Conformance Checking using Token-based Replay and Homomorphic Encryption

1. Probleemstelling

Conformance checking is een kerntaak in procesmining waarbij een eventlog (werkelijke gedrag) wordt vergeleken met een procesmodel (verwacht gedrag) om afwijkingen te identificeren. Traditioneel vereist dit dat zowel de eigenaar van het model als de eigenaar van de log hun gegevens in platte tekst delen met een businessanalist.

In scenario's zoals maatwerkproductie of samenwerkingen tussen organisaties willen partijen echter vaak gevoelige informatie beschermen:

• Modeleigenaren willen hun eigendomsrechtelijke proceslogica (bijvoorbeeld productiewerkstromen) geheim houden.
• Logeigenaren willen gevoelige uitvoeringsgegevens (bijvoorbeeld klantbestelgegevens) beschermen tegen de modeleigenaar.

De uitdaging is om conformance checking (specifiek token-based replay) uit te voeren op versleutelde gegevens zonder het onderliggende procesmodel of de eventlog aan de andere partij te onthullen, terwijl de mogelijkheid behouden blijft om fitness-metrics (afwijkingen) te berekenen.

2. Methodologie

De auteurs stellen een beveiligd raamwerk voor met Homomorf Versleuteling (HE) en een herformulering van het token-based replay-algoritme met behulp van lineaire algebra (matrix- en vectorbewerkingen).

Kernconcepten

• Token-Based Replay: Een algoritme dat eventlog-traces "herhaalt" op een Petrinet. Het houdt tokens bij die verbruikt, geproduceerd, ontbrekend (om transities mogelijk te maken) en overgebleven (overblijvend aan het einde) zijn.
• Homomorf Versleuteling (HE): Specifiek gebruiken de auteurs Zama's Concrete (gebaseerd op TFHE), dat rekenkundige bewerkingen (optellen, aftrekken, vermenigvuldigen) en vergelijkingen (min/max) ondersteunt op versleutelde gehele getallen zonder decryptie.
• Client-Server Architectuur:
  • Client (Logeigenaar): Houdt de eventlog. Versleutelt de huidige markering en de volgende gebeurtenis (transitie) die moet worden gefireerd. Stuurt deze naar de server.
  • Server (Model eigenaar): Houdt het Petrinet-model. Voert de replay-stap uit op versleutelde gegevens met behulp van vooraf berekende matrices. Retourneert de nieuwe versleutelde markering en lokale tellers.
  • Privacy: De server ziet nooit de platte tekst-log; de client ziet nooit de platte tekst-modelstructuur, behalve wat kan worden afgeleid uit de replay.

Algoritmische Herformulering

Om token-based replay compatibel te maken met HE, hebben de auteurs de traditionele "token game" (die afhankelijk is van conditionele logica en vertakkingen) vervangen door matrixvermenigvuldiging en vectorbewerkingen.

1. Voorberekening (Serverkant):

   • Het Petrinet wordt omgezet in een Incidentiematrix ($N$).
   • Een Dynamica-matrix ($E$) wordt geconstrueerd om alle mogelijke "activeringen" (combinaties van huidige markeringen en transities) weer te geven.
   • Een Firing Sequences Matrix ($S$) slaat de Parikh-vectoren (transitietellingen) op voor geldige firing-sequenties.
   • Een Preset Matrix ($P$) slaat de invoerplaatsen op voor elke transitie.

2. Replay-stap (Veilige uitvoering):

   • Activeringscontrole: De client stuurt de versleutelde huidige markering ($M$) en de versleutelde volgende gebeurtenis ($t$). De server berekent een selectievector ($sel$) met behulp van matrixvermenigvuldiging: $E \cdot [M, t]^T$. Dit bepaalt of de transitie direct is geactiveerd of dat stille transities ($\tau$) nodig zijn.
   • Omgaan met ontbrekende tokens: Als de transitie niet is geactiveerd, berekent het algoritme de "ontbrekende tokens" ($\pi$) die nodig zijn vanuit de preset-matrix $P$.
   • Gecombineerde markering-update: Om conditionele if/else-statements te vermijden (die informatie lekken in HE), combineren de auteurs de "passende" en "niet-passende" logica in één vergelijking:
     $$M' = (M + N \cdot \sigma^T) \cdot \text{sum}(sel) + (M + \pi^T + N \cdot t^T) \cdot (1 - \text{sum}(sel))$$
     Hier fungeert $\text{sum}(sel)$ als een binaire schakelaar (1 indien geactiveerd, 0 indien niet).
   • Tellerberekening: Het algoritme berekent ontbrekende ($m$), verbruikte ($c$), geproduceerde ($p$) en overgebleven ($r$) tokens met behulp van vectordifferenties en conditionele masking (vermenigvuldigen met 0 of 1 op basis van de schakelaar).

3. Fitness-berekening:

   • Na het verwerken van alle gebeurtenissen in een trace, decrypteert de client de uiteindelijke tellers en berekent de fitness-score met de standaardformule:
     $$f = \frac{1}{2}\left(1 - \frac{m}{c}\right) + \frac{1}{2}\left(1 - \frac{r}{p}\right)$$

3. Belangrijkste Bijdragen

1. Eerste Veilige Token-Based Replay: Dit is het eerste werk dat homomorf versleuteling specifiek toepast op het token-based replay conformance checking-algoritme.
2. Op matrices gebaseerde Herformulering: De auteurs hebben het niet-lineaire, staat-afhankelijke token-spel succesvol omgezet in een lineair algebraïsche formulering die geschikt is voor homomorf versleuteling, waardoor de noodzaak voor vertakkingslogica wordt geëlimineerd.
3. Privacy-bewust Architectuur: Een client-serverprotocol waarbij de modeleigenaar versleutelde traces verwerkt zonder de trace-inhoud te leren, en de logeigenaar niets leert over de modelstructuur buiten de replay-resultaten.
4. Implementatie en Evaluatie: Een werkend prototype geïmplementeerd in Python met het Zama Concrete-framework, dat de haalbaarheid van de aanpak aantoont.

4. Resultaten

De auteurs evalueerden het prototype met een synthetische eventlog en een Petrinet-model (uit het boek Process Mining en PM4Py-tutorials).

• Prestaties (Duidelijk vs. Versleuteld):
  • Duidelijke Data (CLR): Uitvoeringstijd was in milliseconden.
  • Versleutelde Data (SEC): Uitvoeringstijden varieerden van 7,8 tot 15,8 seconden voor traces zonder token-tellerberekeningen.
  • Versleuteld met Tellers (SEC+): Uitvoeringstijden varieerden van 19,3 tot 37,4 seconden.
• Optimalisatie-inzichten:
  • Een eerste versie die tellers ($p, c, m, r$) berekende binnen de serverkant-functie, nam 35 tot 84 minuten in beslag.
  • De auteurs stelden vast dat deze vertraging te wijten was aan de HE-compiler (Concrete) die standaard 16-bits gehele getallen gebruikte voor retourwaarden, wat enorme overhead veroorzaakte. Door de telleraccumulatie naar de clientkant te verplaatsen (door tussenresultaten te decrypteren), verkleinden ze de tijd tot onder de 40 seconden.
• Schaalbaarheid: De methode slaagde erin traces van variërende lengtes (4 tot 13 gebeurtenissen) en zowel passende als niet-passende traces succesvol te verwerken.

5. Betekenis en Toekomstig Werk

• Betekenis: Het paper bewijst dat beveiligde conformance checking praktisch haalbaar is. Het stelt organisaties in staat procescompliance te verifiëren (bijvoorbeeld in toeleveringsketens of gezondheidszorg) zonder handelsgeheimen of patiëntprivacy te compromitteren. De verschuiving van vertakkingslogica naar matrixbewerkingen is een kritieke theoretische bijdrage voor het toepassen van HE op procesmining.
• Beperkingen:
  • Prestaties: Hoewel onder de minuut, is de versleutelde uitvoering aanzienlijk trager dan platte tekst (ordes van grootte).
  • Token Flooden: De huidige implementatie lost het probleem van "token flooding" (waarbij plaatsen >1 token accumuleren) in het versleutelde domein niet volledig op.
  • Precisie: De afhankelijkheid van gehele-getalprecisie in HE-frameworks beperkt de complexiteit van bewerkingen.
• Toekomstige Richtingen:
  • Testen met real-life eventlogs.
  • Het aanpakken van token flooden in het versleutelde domein.
  • Het verkennen van andere HE-platforms om de afweging tussen precisie en prestaties te optimaliseren.
  • Het implementeren van een volledige client-server netwerkvorm om communicatiekosten te analyseren.

Kortom, het paper biedt een robuust proof-of-concept voor beveiligde procesmining, waarbij wordt aangetoond dat homomorf versleuteling effectief kan worden aangepast aan complexe algoritmische taken zoals token-based replay via algebraïsche herformulering.