PQ-DAS / leanDA 的形式化验证安全性 - 密码学

PQ-DAS 的形式化验证安全性

感谢 Alex Hicks 提供反馈和讨论。

本文及详细的安全性证明大纲由人类作者撰写，向 Lean 的翻译工作在 AI 的大力帮助下完成。

**免责声明。**这里的 lean 代码证明的是关于抽象方案的命题，其前提是对抽象构建模块的假设。特别地，它并不证明任何生产实现的安全性，也永远无法替代对未来实现的正式审计。

动机与目标

在之前的文章中，我们描述并对一个后量子数据可用性采样（DAS）方案进行了基准测试，该方案由 Reed–Solomon 码、基于哈希的承诺以及 LeanVM 证明系统构建。在本文中，我们报告针对该设计密码学核心的一项机器验证的安全性证明：我们在 Lean 中形式化了该方案并证明了其安全性，使用了 mathlib 和 VCVio，并遵循 Foundations of DAS 论文中的安全定义。

该方案遵循 Foundations 论文第 7 节的 encode-and-prove 构造，后者已经附带一个纸笔形式的安全性证明。然而，我们关心的方案做了一个非平凡的优化：它不在 SNARK 内部证明精确的 Reed–Solomon 成员性，而是只证明一种廉价的概率性成员性检查，其随机性通过 Fiat–Shamir 从承诺中派生（在 SNARK 之外）。本次形式化的主要贡献是为这个优化变体给出了完整的安全性证明。由于随机预言机、SNARK 和 rewinding 之间的相互作用，这个证明有些非平凡。

TL;DR 我们证明了什么

大致来说，我们证明了以下内容：

• **假设。**我们拥有一个擦除码、一个安全的向量承诺、一个随机预言机，以及针对下文所述关系的一个非交互式知识论证。

• **结论。**我们得到一个安全的擦除码承诺方案，即满足 position-binding 和 code-binding，并带有显式的安全性归约。

• **解读。**安全的擦除码承诺意味着由此得到的 DAS 方案是安全的，如 Foundations 论文所示（最后这一编译步骤未被形式化）。

• **代码链接。**在此。

开发中的每一个归约都被写成显式算法，以便人类读者能够通过检查来验证它是高效的。主要定理及其所在位置：

结果	Lean 定理
完备性	Target/Scheme.lean 中的 scheme_perfectlyComplete
Position-binding	Proof/PositionBinding.lean 中的 scheme_positionBinding
Code-binding（模块化形式）	Proof/CodeBinding.lean 中的 scheme_codeBinding
Code-binding（显式界）	Proof/CorollaryCodeBinding.lean 中的 scheme_codeBinding_concrete

方案抽象

**为什么抽象。**我们形式化了方案的一个抽象版本，例如将 Merkle 树抽象为向量承诺，遵循 Foundations 论文的第 7 节。然后我们在对这些抽象构建模块的假设下证明安全性，例如向量承诺的 position-binding。原因在于：(a) 这涵盖了方案的不同变体；(b) 这使得论证更容易形式化。

**与论文中方案的差异。**在 Foundations 论文的第 7 节中，论证系统所证明的关系检查的是对码的精确成员性。而这里，我们只检查与对偶码的一个随机向量的内积，该向量通过 Fiat–Shamir 派生。这使得安全性证明变得非平凡，尤其是因为我们不能依赖向量承诺方案的可提取性。正如我们将看到的，由于该向量是在 SNARK 之外派生的，我们仍然可以证明安全性。

构建模块

该方案使用以下抽象构建模块（每个都在 Assumptions/ 中形式化）：

• 一个擦除码 $\mathcal{C} \subseteq \Gamma^n$，由编码函数 $\Sigma^k \to \Gamma^n$ 给出。我们的结果不需要码的其他性质：重构类的性质只出现在从擦除码承诺到 DAS 的（未形式化的）步骤中。

• 一个满足 position-binding 的向量承诺 $\mathsf{VC} = (\mathsf{Setup}, \mathsf{Com}, \mathsf{Ver})$（Foundations 论文中的定义 16）。我们假设 $\mathsf{Com}$ 和打开算法是确定性的且完美完备的，这对我们关注的主要实例化——即 Merkle 树——成立。

• $\mathcal{C}$ 的一个码检查器 $(\mathcal{L}, \mathsf{Check})$。这是一个新的原语：

  • $\mathcal{L}$ 是一个可以高效采样的有限论域；

  • $\mathsf{Check}(L, c) \to 0/1$ 接受一个论域元素 $L \in \mathcal{L}$ 和一个声称的码字 $c$，并确定性地输出一个比特；

  • **完备性：**如果 $c \in \mathcal{C}$，那么对每个 $L$ 都有 $\mathsf{Check}(L, c) = 1$；

  • $\delta$-可靠性：如果 $c \notin \mathcal{C}$ 是固定的，那么在均匀随机的 $L \in \mathcal{L}$ 下，$\mathsf{Check}(L, c) = 1$ 的概率至多为 $\delta$。

直观上，这建模了之前文章中通过内积进行的 Reed–Solomon 成员性检查。注意可靠性中的量词顺序：非码字是在采样随机性之前固定的。作弊的承诺者可能将其承诺的向量与检查随机性相关联——这正是我们必须在安全性证明中排除的情况。

• 一个映射到码检查器论域 $\mathcal{L}$ 的随机预言机 $\mathsf{H}$。

• 针对下述关系 $\mathcal{R}$ 的一个非交互式知识论证 $\mathsf{AS} = (\mathsf{Setup}, \mathsf{Prove}, \mathsf{Ver})$，满足带直线提取器的知识可靠性（Foundations 论文中的定义 18）。该关系为：

  • 陈述：$(\mathsf{ck}, \mathsf{com}_{\mathsf{VC}}, L)$，即承诺密钥、承诺和检查随机性；

  • **见证：**一个声称的码字 $c \in \Gamma^n$；

  • 约束：$\mathsf{com}_{\mathsf{VC}} = \mathsf{VC}.\mathsf{Com}(\mathsf{ck}, c)$ 且 $\mathsf{Check}(L, c) = 1$。

注意，完整的成员性检查 $c \in \mathcal{C}$ 被有意地排除在关系之外——这正是优化的核心所在。一个建模上的注意事项：该论证系统被视为自身不进行任何随机预言机查询；当用一个内部使用哈希的证明系统实例化它时（如 LeanVM 所做的那样），该哈希必须与 $\mathsf{H}$ 进行域分离。

方案

利用这些构建模块，我们构造了如下擦除码承诺方案（在 Target/Scheme.lean 中形式化为 scheme）：

• $\mathsf{Setup}(1^\lambda) \to \mathsf{ck}$：运行 $\mathsf{ck}{\mathsf{VC}} \leftarrow \mathsf{VC}.\mathsf{Setup}(1^\lambda)$ 和 $\mathsf{par}{\mathsf{AS}} \leftarrow \mathsf{AS}.\mathsf{Setup}(1^\lambda)$，返回 $\mathsf{ck} = (\mathsf{ck}{\mathsf{VC}}, \mathsf{par}{\mathsf{AS}})$。

• $\mathsf{Com}(\mathsf{ck}, m) \to (\mathsf{com}, \mathsf{St})$：

  • 编码 $c = \mathcal{C}(m)$ 并承诺 $\mathsf{com}{\mathsf{VC}} = \mathsf{VC}.\mathsf{Com}(\mathsf{ck}{\mathsf{VC}}, c)$；

  • 派生 $L = \mathsf{H}(\mathsf{com}_{\mathsf{VC}})$；

  • 计算 $\pi = \mathsf{AS}.\mathsf{Prove}(\mathsf{par}{\mathsf{AS}}, (\mathsf{ck}{\mathsf{VC}}, \mathsf{com}_{\mathsf{VC}}, L), c)$；

  • 返回 $\mathsf{com} = (\mathsf{com}_{\mathsf{VC}}, \pi)$。

• $\mathsf{Open}$ 和 $\mathsf{Ver}$：使用 $\mathsf{VC}$ 打开位置；验证时重新计算 $L = \mathsf{H}(\mathsf{com}_{\mathsf{VC}})$，验证 $\pi$，然后再验证打开的内容。

注意，我们只对承诺进行哈希以派生 $L$。多哈希一些内容只会在安全性方面让事情更好。

关于这样的承诺如何转化为 DAS 方案，请参阅 Foundations 论文；只需方案满足 code-binding 和 position-binding 即可，而这正是我们所证明的。

证明大纲

这个证明相当有趣，所以我们在这里概述一下。将其翻译成 lean 需要一些工作量，但不算太多。回顾一下，我们想要证明 position-binding 和 code-binding（定义见 Foundations 论文）。

简单情形：Position-Binding

这直接归约到向量承诺的 position-binding：归约忽略承诺的证明部分，只是转发其余部分（定理 scheme_positionBinding）。

Code-Binding：Foundations 论文中证明的回顾

首先回顾一下如果码检查是完美的（即关系检查精确的码成员性）时的安全性证明：

• 敌手输出一个承诺 $(\mathsf{com}_{\mathsf{VC}}, \pi)$ 以及某些位置的打开值，使得没有任何码字与它们一致；

• 我们从 $\pi$ 中提取出承诺 $\mathsf{com}_{\mathsf{VC}}$ 的一个原像 $c$。由于关系检查精确的码成员性，$c$ 在码中（否则我们就破坏了知识可靠性）；

• 因为 $c$ 在码中且没有码字与这些打开值一致，所以必有一个打开值与 $c$ 不一致——这就破坏了 position-binding。

对于最后一步，position-binding 的一个弱变体就足够了，其中两个打开值之一来自诚实计算的承诺（即对提取出的 $c$ 的承诺）。在形式化中，这个弱变体——以及后面用到的确定性 $\mathsf{Com}$ 的抗碰撞性质——都是从 position-binding 和完备性证明出来的（Assumptions/VectorCommitment.lean）。

主要技术挑战

在我们的方案中，码成员性只是概率性地检查，随机性 $L$ 通过 Fiat–Shamir 从承诺派生。假设片刻承诺是完全可提取的：看到 $\mathsf{com}_{\mathsf{VC}}$ 后我们可以立即获得一个原像 $c$，所有后续的打开值都必须与之一致。那么我们可以为每次随机预言机查询定义一个坏事件——即被查询的承诺提取出一个非码字 $c$，但它却通过了在新采样的答案 $L$ 上的检查——并将每个这样的事件以 $\delta$ 为上界，因为 $c$ 在 $L$ 之前就已确定。

这里有一个问题：把 $\mathsf{Com}$ 想象成一棵 Merkle 树。我们在被证明的关系内部求值 $\mathsf{Com}$，但只有当它的哈希本身被建模为随机预言机时，Merkle 树才可能是完全可提取的——这意味着我们要在被证明的关系内部求值一个随机预言机，而这需要一个相对化的简洁论证，已被证明是不可能的。**我们必须避免这条路线。**附注：这也是为什么 Fiat-Shamir 哈希在 SNARK 之外计算的原因，否则我们将被迫使用相对化论证。

在没有可提取性的情况下，我们没有形式化的保证说 $c$ 在 $L$ 被采样之前就已固定——就我们能证明的范围而言，敌手可能在看到 $L$ 之后才决定打开哪个 $c$。因此我们不能直接应用码检查器的可靠性。

解决方案的直觉

当然还是有希望的：如果敌手在看到 $L$ 之后才决定打开哪个 $c$，那么它同样可能为不同的 $L'$ 打开不同的 $c' \neq c$——而同一承诺的两个不同打开值会破坏绑定性。问题在于归约永远看不到这个假想的另一个 $c'$。解决方案是 rewinding：从敌手产生其承诺的那一点开始运行两次敌手，两次运行中使用独立的检查随机性，从而让假想的 $c'$ 变成现实。

Committed Soundness

我们将分析的核心隔离在一个抽象的安全实验中，我们称之为 committed soundness，它只涉及向量承诺、码、码检查器和随机预言机——论证系统在其中不起作用。敌手获得 $\mathsf{ck}{\mathsf{VC}}$ 和对随机预言机的访问权，并输出一对 $(\mathsf{com}{\mathsf{VC}}, c)$。取 $L = \mathsf{H}(\mathsf{com}_{\mathsf{VC}})$，如果以下条件成立则敌手获胜：

1. $c \notin \mathcal{C}$ 但 $\mathsf{Check}(L, c) = 1$，且

2. $c$ 承诺到 $\mathsf{com}{\mathsf{VC}}$，即 $\mathsf{com}{\mathsf{VC}} = \mathsf{VC}.\mathsf{Com}(\mathsf{ck}_{\mathsf{VC}}, c)$。

这个实验恰好捕捉到了上面指出的差距：敌手可以将 $c$ 与从其承诺派生的挑战相关联。（形式化中还包含一个等价的交互式变体，不含随机预言机，其中游戏本身在敌手提交承诺之后发送一个均匀随机的 $L$；两者通过一个标准论证联系起来，该论证猜测哪个预言机查询决定了挑战，代价是查询次数上的乘法损失。）

从 Committed Soundness 到 Code-Binding

假设片刻没有高效敌手能赢得 committed soundness 游戏。那么 code-binding 就按照与 Foundations 论文相同的模式得出（定理 scheme_codeBinding）。设一个针对 code-binding 的敌手输出一个承诺 $(\mathsf{com}{\mathsf{VC}}, \pi)$ 以及一些打开值，使得没有任何码字与它们一致，并设 $c$ 为在陈述 $(\mathsf{ck}{\mathsf{VC}}, \mathsf{com}_{\mathsf{VC}}, L)$ 处从 $\pi$ 中提取出的见证。以下三种情况恰好发生其一：

• 提取失败（$c$ 不是有效见证）：该运行破坏了论证系统的知识可靠性（归约 $\mathcal{R}_1$）；

• 提取成功但 $c \notin \mathcal{C}$：那么 $c$ 通过了在 $L = \mathsf{H}(\mathsf{com}{\mathsf{VC}})$ 上的检查并承诺到 $\mathsf{com}{\mathsf{VC}}$——这是 committed soundness 游戏的一次获胜（归约 $\mathcal{R}_2$）；

• 提取成功且 $c \in \mathcal{C}$：由于没有码字与这些打开值一致，某个打开值与 $c$ 不一致，破坏了（弱）position-binding（归约 $\mathcal{R}_3$）。

对三种情况取并集界得到

$$\Pr[\text{code-binding broken}] ;\le; \varepsilon_{\mathsf{ks}} + \varepsilon_{\mathsf{cs}} + \varepsilon_{\mathsf{wpb}}.$$

Committed Soundness 游戏的分析

这是我们使用 rewinding 的部分（定理 niCommittedSoundness_forking_bound）。想法是：如果一个敌手以不可忽视的概率赢得游戏，那么——从决定其挑战的那个预言机查询开始第二次重放，并给出一个新的答案——它会以相关概率赢得两次运行。这一点由分叉引理精确刻画，幸运的是 VCVio 库中已经有了这个引理。记 $\mathsf{acc}$ 为最多进行 $Q$ 次预言机查询的敌手的获胜概率，两次运行产生相同的承诺 $\mathsf{com}_{\mathsf{VC}}$、两个独立的挑战 $L \neq L'$ 和两个答案 $c, c'$，我们区分：

• 不同答案（$c \neq c'$）：两者在确定性 $\mathsf{Com}$ 下都承诺到同一个 $\mathsf{com}_{\mathsf{VC}}$——这是一个碰撞，破坏了向量承诺的 position-binding。

• 相同答案（$c = c'$）：此时 $c$ 已经由第一次运行确定——特别是在新的挑战 $L'$ 被采样之前——并且它是一个通过 $\mathsf{Check}(L', c) = 1$ 的非码字。根据码检查器的 $\delta$-可靠性，这种情况发生的概率至多为 $\delta$。

总体而言，分叉分析给出

$$\mathsf{acc} \cdot \left( \frac{\mathsf{acc}}{Q+1} - \frac{1}{|\mathcal{L}|} \right) ;\le; \varepsilon_{\mathsf{coll}} + \delta,$$

其中 $\varepsilon_{\mathsf{coll}}$ 是一个显式碰撞查找归约的成功概率（它反过来又被 position-binding 所约束）。形式化工作的一个惊喜：直接用库的分叉引理分析非交互式游戏，结果比上面概述的经过交互式游戏的两步路线既更简单又在数量上更优。

最终界

组合各部分并求解不等式（定理 scheme_codeBinding_concrete 和 scheme_codeBinding_concrete_posBinding），一个用 $Q$ 次随机预言机查询破坏 code-binding 的敌手满足

$$\Pr[\text{code-binding broken}] ;\le; \varepsilon_{\mathsf{ks}} + \varepsilon_{\mathsf{pb}} + \sqrt{(Q+2)\left(\varepsilon_{\mathsf{pb}}' + \delta + \tfrac{1}{|\mathcal{L}|}\right)},$$

其中 $\varepsilon_{\mathsf{ks}}$ 是知识可靠性误差，$\varepsilon_{\mathsf{pb}}, \varepsilon_{\mathsf{pb}}'$ 是显式归约的 position-binding 误差。（在 Lean 开发中，该界以精确的平方形式陈述，避免了平方根。）

**关于定量方面的说明。**平方根损失和因子 $Q$ 是基于 rewinding 的 Fiat–Shamir 派生随机性分析所固有的，它们对参数选择很重要：可证明的安全级别由 $\sqrt{Q \cdot \delta}$ 决定，而不是由 $\delta$ 本身决定。例如，一个 $\delta \approx 2^{-136}$ 的检查器（如我们之前文章中的 Reed–Solomon 实例化）在面对进行 $2^{64}$ 次随机预言机查询的敌手时，可证明提供大约 $36$ 比特的 code-binding 安全性——比启发式估计 $\delta$ 保守得多。也许这是证明技术的产物，如何设置参数仍有待讨论。

未涵盖的内容

本次形式化涵盖了擦除码承诺方案及其两个绑定性质，所有归约均为显式。它不涵盖：从擦除码承诺到完整 DAS 方案的编译（Foundations 论文第 6 节）、具体码检查器实例化的安全性（例如我们之前文章中的重心 Reed–Solomon 检查——一个自然的下一步，因为它的可靠性是一个自包含的多项式恒等式论证），以及论证系统和哈希函数的内部细节，这些属于模型的假设。

• 原文链接： ethresear.ch/t/formally-...
• 鸿途知科网 AI 助手，为大家转译优秀英文文章，如有翻译不通的地方，还请包涵～