💻 computer science

Formal Verification of Probing Security via Conditional Independence

本文提出了一种针对掩码密码算法探测安全性的新颖形式化验证方法，该方法利用概率分离逻辑（Lilac）在非干扰属性与条件独立性之间建立联系。

原作者： Satoshi Kura, Katsuyuki Takashima

发布于 2026-05-25

📖 1 分钟阅读☕ 轻松阅读

原作者： Satoshi Kura, Katsuyuki Takashima

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

想象一下，你正试图在一个繁忙且嘈杂的厨房里保护一份秘密食谱。在密码学世界中，这份“秘密食谱”就是私钥，而“噪音”则是侧信道攻击。攻击者并非试图破解数学难题，而是试图在计算机进行数值运算时窥探那些“泄露”（如功耗或时间延迟），以此猜测你的秘密。

为了阻止这种情况，密码学家使用一种称为**掩码（Masking）**的技术。将掩码想象成把你的秘密食谱撕成 $t+1$ 张纸片（份额）。你将其中一张纸片交给 $t+1$ 位不同的厨师。只要窃听者只能窥探到 $t$ 张纸片（或更少），他们看到的就只是一堆随机乱码。由于至少缺少一张关键纸片，他们无法还原食谱。

然而，要证明一个复杂的食谱（算法）真正安全是极其困难的。如果你试图手工检查，可能会漏掉微小的泄露，导致整个安全系统失效。这正是本文发挥作用的地方。

问题：检查“泄露”

作者希望构建一个形式化证明（数学保证），以确认掩码算法是安全的。传统上，这是通过“模拟器”概念完成的。

模拟器的思路：想象一个魔法盒子（模拟器），它试图精确重现窃听者所看到的内容。如果这个魔法盒子能够仅利用公开信息（如配料表）且从未见过秘密食谱的纸片，就创造出完全相同的“泄露”，那么该真实算法就是安全的。窃听者不会获得任何新信息。

但手工构建这些模拟器容易出错。作者希望找到一种更好的证明方法。

解决方案：一种新的逻辑工具（Lilac）

作者建立了“模拟器”与条件独立性概念之间的联系。

类比：想象你试图猜测朋友的生日（秘密）。
- 场景 A：你知道他们的年龄和出生月份（公开信息）。
- 场景 B：你还知道他们的秘密日记条目（秘密信息）。
- 条件独立性：如果你已经知道了年龄和月份，那么知道日记条目不会改变你对生日的猜测，那么在该年龄/月份条件下，日记与生日就是“条件独立”的。

本文证明：如果存在一个模拟器，那么在给定公开信息的情况下，秘密与泄露就是条件独立的。

为了在数学上验证这一点，他们使用了一种名为Lilac的工具。

Lilac 是什么？ 将 Lilac 想象成一本极其严格、功能强大的概率规则手册。它就像一场逻辑游戏，你必须证明两堆牌（随机变量）是相互独立洗牌的。
分离合取（Separating Conjunction）：在这本规则手册中，有一个特殊符号（像魔杖一样），它表示：“这两堆牌完全分离，互不影响。”
创新点：作者为该规则手册添加了新规则来处理“条件化”（即“在……条件下”的部分）。这使得他们能够证明，即使窃听者看到了一些数据，由于他们已拥有公开数据，这些数据也不会揭示秘密。

他们实际做了什么

作者不仅讨论了理论，还构建了一个系统，利用这种新逻辑来验证真实的密码学算法。他们将这种方法应用于现代加密中使用的三个特定“组件”（构建模块）：

MINIADDREPNOISE：一种用于向数据添加随机噪声的工具（就像在汤里加盐以掩盖原始味道）。他们证明，即使攻击者窥探了部分加盐的汤，也无法推断出原始味道。
REFRESH：一种工具，它接收秘密的碎纸片并重新洗牌，使其看起来焕然一新，防止攻击者随时间追踪它们。他们证明了这种重新洗牌是安全的。
SECMULT（安全乘法）：一种将两个秘密数字相乘而不泄露结果直到最后的工具。这是最难保护的操作之一。他们证明了这种乘法能够抵御"t-探测”攻击。

核心结论

本文声称，通过将“模拟器”的复杂概念转化为“条件独立性”的语言，他们可以利用Lilac逻辑系统自动且严格地验证这些密码学工具的安全性。

他们通过为MINIADDREPNOISE、REFRESH和SECMULT编写形式化证明，成功展示了这一点，表明这些特定算法满足保护秘密免受侧信道攻击所需的严格安全要求。他们并未声称能解决所有未来的安全问题或将此应用于医疗设备；他们的工作严格限于使用新的逻辑框架来证明这些特定密码学数学运算的安全性。

技术摘要：通过条件独立性形式化验证探测安全性

问题陈述

侧信道攻击对密码方案的安全性构成了重大威胁，促使掩码（masking）作为一种对策被广泛采用。掩码将秘密值分割为多个份额，以确保任何中间值子集的泄露都不会揭示底层秘密。然而，证明掩码算法的安全性，特别是在ISW 探测模型（其中攻击者可以探测最多 $t$ 个中间值）下，手动进行证明极易出错。多项手动安全证明中已发现缺陷，因此亟需形式化验证。

虽然概率分离逻辑已成功应用于验证输入独立性等属性（例如在一次性密码本中），但尚未被用于验证掩码算法的探测安全性（具体为 $t$ -非干扰性）。现有的形式化验证工具通常依赖基于替换的方法或类型推断，这可能缺乏掩码所固有的复杂条件独立性推理所需的模块化或表达能力。

方法论

这项工作提出了一种新颖的形式化验证方法，通过建立基于模拟器的安全定义与条件独立性之间的严格联系。该方法依赖于Lilac，这是一种专为推理条件独立性而设计的概率分离逻辑。

1. 理论基础：模拟器与条件独立性

作者将标准的基于模拟器的非干扰定义重述为条件独立性的形式。

基于模拟器的观点：如果对于攻击者观测到的任意探针集合 $O$ ，都存在一个模拟器能够仅使用输入份额的子集 $I$ 生成 $O$ 的分布，而无需访问其余的秘密份额，则该掩码算法是安全的。
条件独立性的观点：这一安全要求等价于断言：在给定公共输入份额 $I$ 的情况下，观测值 $O$ 与秘密输入份额（ $\Delta \setminus I$ ）是条件独立的。形式上，这表示为 $O \perp (\Delta \setminus I) \mid I$ 。

论文证明，这一等价性在 Lilac 的语义框架内成立，该框架利用概率空间的独立组合和通过分解（disintegration）进行的条件化来建模概率独立性。

2. Lilac 的扩展

为了将 Lilac 应用于探测安全性，作者扩展了该逻辑，增加了原始 Lilac 表述中未包含的特定证明规则：

半图公理（Semi-Graphoid Axioms）：论文证明了条件独立性的半图公理（对称性、分解性、弱并集性和收缩性）在 Lilac 语义内成立。这些公理对于在证明过程中操作条件独立性陈述至关重要。
组合规则：引入了新规则以处理非干扰属性的组合，特别是针对顺序组合和 for 循环。这些规则允许对由更小部件构建的复杂算法进行模块化验证。
所有权与弱化：额外的规则促进了关于随机变量所有权的推理，以及在处理未共享输入或变量子集时非干扰属性的弱化。

3. 验证框架

验证过程包括：

将用概率编程语言APPL编写的掩码算法转换为 Lilac 内的霍拉三元组（Hoare triples）。
利用已建立的等价性（定理 V.1），将 $(I, O)$ -非干扰性的验证简化为证明特定的条件独立性霍拉三元组：
$\{ \text{own } \Delta \} \ M \ \{ Y. \ C_{x \leftarrow I}(\text{own}(\Delta \setminus I) * \text{own } O) \}$
应用扩展后的证明规则集（包括新的半图公理和组合规则）来推导所需的蕴含关系。

主要贡献

形式化联系：论文建立了基于模拟器的探测安全定义与 Lilac 中可表达的条件独立性属性之间的形式等价性。这填补了密码学安全概念与概率分离逻辑之间的鸿沟。
Lilac 的扩展：作者提供了一套验证掩码算法所需的额外证明规则，包括条件独立性的半图公理以及用于顺序组合和循环的组合规则。
案例研究：通过使用 Lilac 形式化验证三个关键算法的探测安全性，证明了该方法的有效性：
- MINIADDREPNOISE：一个为掩码值添加均匀噪声的子程序。
- REFRESH：一个用于刷新份额以防止泄露累积的基础算法。
- SECMULT：一种标准的掩码乘法算法。
- ADDREPNOISEER：在Raccoon签名方案（NIST 后量子密码标准化候选方案）中使用的一个变体，证明其满足 $t$ -带未共享输入的强非干扰性（ $t$ -SNIU）属性。

结果

论文成功推导出了目标算法的霍拉三元组，确认了它们的非干扰属性。

对于MINIADDREPNOISE，证明表明输出份额在给定观测输入的情况下，与未观测的输入份额是条件独立的。
对于REFRESH，证明验证了该算法满足 $t$ -强非干扰性（ $t$ -SNI），这是一种比标准非干扰性更强的属性，对于高阶掩码中的组合性至关重要。
对于SECMULT和ADDREPNOISEER，证明利用新的组合规则来处理这些算法固有的嵌套循环和复杂数据依赖关系。

ADDREPNOISEER的验证尤为显著，因为它验证了 Raccoon 签名方案安全证明中的关键组件，该证明依赖于 $t$ -SNIU 属性。

意义与主张

作者声称，这项工作首次将概率分离逻辑（特别是 Lilac）应用于掩码算法探测安全性的形式化验证。通过将安全证明转化为条件独立性推理，该方法为现有的基于替换或类型推断的工具提供了一种模块化且逻辑严谨的替代方案。

论文强调，虽然将模拟器与条件独立性联系起来的基本概念很简单，但由于该逻辑依赖于独立组合而非标准乘积概率空间，其在 Lilac 中的形式化在技术上并非易事。主要定理的成功推导及其在现实世界密码组件（Raccoon）上的应用表明，该框架对于验证复杂的、高阶的掩码方案是可行的。

这项工作在其范围上保持适度，指出当前的结果仅限于探测安全性的信息论设定。作者指出，将方法扩展到计算设定以及在交互式定理证明器中实现该方法，是未来工作的重要方向。他们还建议，该框架可应用于其他基于模拟器的安全属性，例如安全多方计算中发现的属性。