Secure Conformance Checking using Token-based Replay and Homomorphic Encryption

以下是论文《基于令牌重放与同态加密的安全一致性检查》的详细技术总结。

1. 问题陈述

一致性检查是流程挖掘中的核心操作，它将事件日志（实际行为）与流程模型（预期行为）进行比较，以识别偏差。传统上，这需要模型所有者和日志所有者将他们的数据以明文形式共享给业务分析师。

然而，在定制制造或跨组织协作等场景中，各方通常希望保护敏感信息：

• 模型所有者可能希望保守其专有流程逻辑（例如生产工作流）的秘密。
• 日志所有者可能希望保护敏感的执行数据（例如客户订单详情）不被模型所有者获取。

挑战在于如何在加密数据上执行一致性检查（具体为基于令牌的重放），而不向另一方揭示底层流程模型或事件日志，同时保持计算适应性指标（偏差）的能力。

2. 方法论

作者提出了一种使用**同态加密（HE）**的安全框架，并利用线性代数（矩阵和向量运算）对基于令牌的重放算法进行了重构。

核心概念

• 基于令牌的重放： 一种在佩特里网（Petri net）上“重放”事件日志轨迹的算法。它追踪被消耗的令牌、产生的令牌、缺失的令牌（用于使转换生效）以及剩余的令牌（结束时遗留的）。
• 同态加密（HE）： 具体而言，作者利用了基于 TFHE 的Zama Concrete，它支持在加密整数上执行算术运算（加法、减法、乘法）和比较运算（最小值/最大值），而无需解密。
• 客户端 - 服务器架构：
  • 客户端（日志所有者）： 持有事件日志。加密当前标记（marking）和下一个要触发的转换（事件）。将这些发送给服务器。
  • 服务器（模型所有者）： 持有佩特里网模型。使用预计算的矩阵在加密数据上执行重放步骤。返回新的加密标记和本地计数器。
  • 隐私性： 服务器从未看到明文日志；客户端除了从重放中推断出的内容外，从未看到明文模型结构。

算法重构

为了使基于令牌的重放与同态加密兼容，作者用矩阵乘法和向量运算取代了传统的“令牌游戏”（后者依赖于条件逻辑和分支）。

1. 预计算（服务器端）：

   • 将佩特里网转换为关联矩阵（$N$）。
   • 构建**动态矩阵（$E$）**以表示所有可能的“使能”（当前标记和转换的组合）。
   • **触发序列矩阵（$S$）**存储有效触发序列的帕里向量（Parikh vectors，即转换计数）。
   • **预设矩阵（$P$）**存储每个转换的输入库所。

2. 重放步骤（安全执行）：

   • 使能检查： 客户端发送加密的当前标记（$M$）和加密的下一个事件（$t$）。服务器使用矩阵乘法计算**选择向量（$sel$）**：$E \cdot [M, t]^T$。这确定转换是直接使能还是需要静默转换（$\tau$）。
   • 处理缺失令牌： 如果转换未使能，算法根据预设矩阵 $P$ 计算所需的“缺失令牌”（$\pi$）。
   • 统一标记更新： 为了避免在 HE 中泄露信息的条件 if/else 语句，作者将“拟合”和“不拟合”逻辑合并为单个方程：
     $$M' = (M + N \cdot \sigma^T) \cdot \text{sum}(sel) + (M + \pi^T + N \cdot t^T) \cdot (1 - \text{sum}(sel))$$
     其中，$\text{sum}(sel)$ 充当二进制开关（如果使能则为 1，否则为 0）。
   • 计数器计算： 算法使用向量差和条件掩码（基于开关乘以 0 或 1）计算缺失（$m$）、消耗（$c$）、产生（$p$）和剩余（$r$）的令牌。

3. 适应性计算：

   • 在处理完轨迹中的所有事件后，客户端解密最终计数器，并使用标准公式计算适应性分数：
     $$f = \frac{1}{2}\left(1 - \frac{m}{c}\right) + \frac{1}{2}\left(1 - \frac{r}{p}\right)$$

3. 主要贡献

1. 首个安全基于令牌的重放： 这是首次将同态加密专门应用于基于令牌的重放一致性检查算法的工作。
2. 基于矩阵的重构： 作者成功地将非线性的、状态依赖的令牌游戏转换为适合同态加密的线性代数公式，消除了对分支逻辑的需求。
3. 隐私保护架构： 一种客户端 - 服务器协议，其中模型所有者处理加密轨迹而不了解轨迹内容，日志所有者除了重放结果外对模型结构一无所知。
4. 实现与评估： 使用 Zama 的 Concrete 框架在 Python 中实现了工作原型，证明了该方法的可行性。

4. 结果

作者使用合成事件日志和佩特里网模型（来自《流程挖掘》一书和 PM4Py 教程）评估了原型。

• 性能（明文与加密）：
  • 明文数据（CLR）： 执行时间在毫秒级。
  • 加密数据（SEC）： 对于不包含令牌计数器计算的轨迹，执行时间范围为7.8 到 15.8 秒。
  • 带计数器的加密（SEC+）： 执行时间范围为19.3 到 37.4 秒。
• 优化见解：
  • 一个在服务器端函数内部计算计数器（$p, c, m, r$）的初始版本耗时35 到 84 分钟。
  • 作者发现这种 slowdown 是由于 HE 编译器（Concrete）默认将返回值设为 16 位整数，导致巨大的开销。通过将计数器累积移至客户端（解密中间结果），他们将时间减少到 40 秒以内。
• 可扩展性： 该方法成功处理了不同长度（4 到 13 个事件）的轨迹，以及拟合和非拟合轨迹。

5. 意义与未来工作

• 意义： 该论文证明了安全一致性检查在实际中是可行的。它使组织能够在不泄露商业秘密或患者隐私的情况下验证流程合规性（例如在供应链或医疗保健中）。从分支逻辑向矩阵运算的转变是将 HE 应用于流程挖掘的关键理论贡献。
• 局限性：
  • 性能： 虽然加密执行在不到一分钟内完成，但比明文慢得多（数量级差异）。
  • 令牌泛滥： 当前的实现尚未完全解决加密域中的“令牌泛滥”问题（即库所累积超过 1 个令牌）。
  • 精度： 对 HE 框架中整数精度的依赖限制了操作的复杂性。
• 未来方向：
  • 使用真实事件日志进行测试。
  • 解决加密域中的令牌泛滥问题。
  • 探索其他 HE 平台以优化精度与性能之间的权衡。
  • 实现完整的客户端 - 服务器网络版本以分析通信成本。

总之，该论文为安全流程挖掘提供了强有力的概念验证，证明了通过代数重构，同态加密可以有效地适应基于令牌的重放等复杂算法任务。