Secure Conformance Checking using Token-based Replay and Homomorphic Encryption

Aquí se presenta un resumen técnico detallado del artículo "Verificación de conformidad segura usando replay basado en tokens y cifrado homomórfico".

1. Planteamiento del Problema

La verificación de conformidad es una operación central en la minería de procesos que compara un registro de eventos (comportamiento real) contra un modelo de proceso (comportamiento esperado) para identificar desviaciones. Tradicionalmente, esto requiere que tanto el propietario del modelo como el propietario del registro compartan sus datos en texto plano con un analista de negocios.

Sin embargo, en escenarios como la fabricación personalizada o las colaboraciones interorganizacionales, las partes a menudo desean proteger información sensible:

• Propietarios del modelo pueden querer mantener en secreto su lógica de procesos propietaria (por ejemplo, flujos de trabajo de producción).
• Propietarios del registro pueden querer proteger datos sensibles de ejecución (por ejemplo, detalles de pedidos de clientes) del propietario del modelo.

El desafío es realizar la verificación de conformidad (específicamente el replay basado en tokens) sobre datos cifrados sin revelar el modelo de proceso subyacente ni el registro de eventos a la otra parte, manteniendo al mismo tiempo la capacidad de calcular métricas de ajuste (desviaciones).

2. Metodología

Los autores proponen un marco seguro utilizando Cifrado Homomórfico (CH) y una reformulación del algoritmo de replay basado en tokens mediante álgebra lineal (operaciones de matriz y vector).

Conceptos Clave

• Replay Basado en Tokens: Un algoritmo que "reproduce" las trazas del registro de eventos en una red de Petri. Rastrea los tokens consumidos, producidos, faltantes (para habilitar transiciones) y restantes (sobrantes al final).
• Cifrado Homomórfico (CH): Específicamente, los autores utilizan Concrete de Zama (basado en TFHE), que soporta operaciones aritméticas (suma, resta, multiplicación) y comparaciones (mínimo/máximo) sobre enteros cifrados sin descifrarlos.
• Arquitectura Cliente-Servidor:
  • Cliente (Propietario del registro): Posee el registro de eventos. Cifra la marca actual y el siguiente evento (transición) a disparar. Envía estos datos al servidor.
  • Servidor (Propietario del modelo): Posee el modelo de red de Petri. Realiza el paso de replay sobre datos cifrados utilizando matrices precalculadas. Devuelve la nueva marca cifrada y los contadores locales.
  • Privacidad: El servidor nunca ve el registro en texto plano; el cliente nunca ve la estructura del modelo en texto plano más allá de lo inferido del replay.

Reformulación Algorítmica

Para hacer compatible el replay basado en tokens con el CH, los autores reemplazaron el "juego de tokens" tradicional (que depende de lógica condicional y bifurcaciones) con multiplicación de matrices y operaciones vectoriales.

1. Precálculo (Lado del Servidor):

   • La red de Petri se convierte en una Matriz de Incidencia ($N$).
   • Se construye una Matriz de Dinámica ($E$) para representar todas las posibles "habilitaciones" (combinaciones de marcas actuales y transiciones).
   • Una Matriz de Secuencias de Disparo ($S$) almacena los vectores de Parikh (conteos de transiciones) para secuencias de disparo válidas.
   • Una Matriz de Preconjunto ($P$) almacena los lugares de entrada para cada transición.

2. Paso de Replay (Ejecución Segura):

   • Verificación de Habilitación: El cliente envía la marca actual cifrada ($M$) y el siguiente evento cifrado ($t$). El servidor calcula un vector selector ($sel$) usando multiplicación de matrices: $E \cdot [M, t]^T$. Esto determina si la transición está habilitada directamente o requiere transiciones silenciosas ($\tau$).
   • Manejo de Tokens Faltantes: Si la transición no está habilitada, el algoritmo calcula los "tokens faltantes" ($\pi$) requeridos desde la matriz de preconjunto $P$.
   • Actualización Unificada de Marca: Para evitar declaraciones condicionales if/else (que filtran información en CH), los autores combinan la lógica de "ajuste" y "no ajuste" en una sola ecuación:
     $$M' = (M + N \cdot \sigma^T) \cdot \text{sum}(sel) + (M + \pi^T + N \cdot t^T) \cdot (1 - \text{sum}(sel))$$
     Aquí, $\text{sum}(sel)$ actúa como un interruptor binario (1 si habilitado, 0 si no).
   • Cálculo de Contadores: El algoritmo calcula los tokens faltantes ($m$), consumidos ($c$), producidos ($p$) y restantes ($r$) usando diferencias vectoriales y enmascaramiento condicional (multiplicando por 0 o 1 basado en el interruptor).

3. Cálculo de Ajuste:

   • Después de procesar todos los eventos en una traza, el cliente descifra los contadores finales y calcula la puntuación de ajuste usando la fórmula estándar:
     $$f = \frac{1}{2}\left(1 - \frac{m}{c}\right) + \frac{1}{2}\left(1 - \frac{r}{p}\right)$$

3. Contribuciones Clave

1. Primer Replay Basado en Tokens Seguro: Este es el primer trabajo que aplica cifrado homomórfico específicamente al algoritmo de verificación de conformidad por replay basado en tokens.
2. Reformulación Basada en Matrices: Los autores transformaron con éxito el juego de tokens no lineal y dependiente del estado en una formulación algebraica lineal adecuada para el cifrado homomórfico, eliminando la necesidad de lógica de bifurcación.
3. Arquitectura de Preservación de Privacidad: Un protocolo cliente-servidor donde el propietario del modelo procesa trazas cifradas sin aprender el contenido de la traza, y el propietario del registro no aprende nada sobre la estructura del modelo más allá de los resultados del replay.
4. Implementación y Evaluación: Un prototipo funcional implementado en Python utilizando el marco Concrete de Zama, demostrando la viabilidad del enfoque.

4. Resultados

Los autores evaluaron el prototipo utilizando un registro de eventos sintético y un modelo de red de Petri (del libro Process Mining y tutoriales de PM4Py).

• Rendimiento (Texto Plano vs. Cifrado):
  • Datos en Texto Plano (CLR): El tiempo de ejecución fue de milisegundos.
  • Datos Cifrados (SEC): Los tiempos de ejecución oscilaron entre 7.8 y 15.8 segundos para trazas sin cálculos de contadores de tokens.
  • Cifrado con Contadores (SEC+): Los tiempos de ejecución oscilaron entre 19.3 y 37.4 segundos.
• Insights de Optimización:
  • Una versión inicial que calculaba los contadores ($p, c, m, r$) dentro de la función del lado del servidor tardó 35 a 84 minutos.
  • Los autores identificaron que esta ralentización se debía a que el compilador de CH (Concrete) utilizaba por defecto enteros de 16 bits para los valores de retorno, causando una sobrecarga masiva. Al mover la acumulación de contadores al lado del cliente (descifrando resultados intermedios), redujeron el tiempo a menos de 40 segundos.
• Escalabilidad: El método manejó con éxito trazas de longitudes variables (de 4 a 13 eventos) y tanto trazas ajustadas como no ajustadas.

5. Significado y Trabajo Futuro

• Significado: El artículo demuestra que la verificación de conformidad segura es prácticamente viable. Permite a las organizaciones verificar el cumplimiento de procesos (por ejemplo, en cadenas de suministro o atención médica) sin comprometer secretos comerciales o la privacidad de los pacientes. El cambio de la lógica de bifurcación a las operaciones matriciales es una contribución teórica crítica para aplicar CH a la minería de procesos.
• Limitaciones:
  • Rendimiento: Aunque está por debajo de un minuto, la ejecución cifrada es significativamente más lenta que el texto plano (órdenes de magnitud).
  • Inundación de Tokens: La implementación actual no aborda completamente el problema de la "inundación de tokens" (donde los lugares acumulan >1 token) en el dominio cifrado.
  • Precisión: La dependencia de la precisión de enteros en los marcos de CH limita la complejidad de las operaciones.
• Direcciones Futuras:
  • Pruebas con registros de eventos de la vida real.
  • Abordar la inundación de tokens en el dominio cifrado.
  • Explorar otras plataformas de CH para optimizar la compensación entre precisión y rendimiento.
  • Implementar una versión completa de red cliente-servidor para analizar los costos de comunicación.

En conclusión, el artículo proporciona una prueba de concepto robusta para la minería de procesos segura, demostrando que el cifrado homomórfico puede adaptarse eficazmente a tareas algorítmicas complejas como el replay basado en tokens mediante una reformulación algebraica.