CryptoZoo：用于简化归约证明的交互式工具

### CryptoZoo：用于归约证明的查看器 #### 1. 引言 归约证明是一种让自己和他人相信密码学设计安全属性的方法。在验证、交流和理解复杂系统的证明方面，密码学界有不同的技术和风格，下面简要回顾： - **黑盒原语**：黑盒原语是支持模块化证明和信息隐藏的抽象概念。例如，具有选择明文攻击下不可区分性（IND - CPA）的对称加密方案（SE），允许构建使用SE的系统，而无需深入了解AES密码和合适的密码模式的细节。复杂系统的密码学证明通常会使用多个这样的黑盒原语，模块化证明往往先抽象出子系统，证明其安全性，然后以黑盒方式将大系统的安全性归约到子系统。 - **通用可组合性**：Canetti的通用组合框架（UC）将考虑对抗性选择输入的思想应用于协议，为通过有用的中间概念证明协议安全性提供了基础。定义UC中的安全性只需指定一个理想功能，无需重新发明对抗模型。此外，Maurer的抽象密码学框架和Rosulek的《密码学的乐趣》也采用了类似方法，并鼓励使用可视化组件来跟进证明。 - **游戏跳跃**：Shoup提出的游戏跳跃技术将系统安全性形式化的两个游戏之间的不可区分性大证明拆分为一系列较小的不可区分性步骤，每个步骤可单独证明，这些步骤的引理序列确立了后续游戏对之间的不可区分性，从而意味着所讨论的两个游戏的不可区分性。 - **基于代码的游戏跳跃**：Bellare和Rogaway将代码引入游戏跳跃证明，伪代码使两个后续游戏可以并列展示，便于检查代码的具体变化。这种方式具有很强的可视化组件，能吸引读者关注游戏跳跃中的变化，同时让读者随时获取相关代码。 - **模块化代码编写**：在实际协议中，基于代码的游戏和基于代码的游戏跳跃经常被使用。一些工作会将代码精心打包成子例程，以确保归约的合理性。例如，Bellare、Hoang和Rogaway对姚氏混淆方案的证明。若归约R与较小游戏$Game_{small}^b$交互，对于对手A与之交互的较大游戏$Game_{big}^b$，当$b\in\{0, 1\}$时，若$R → Game_{small}^b ≡ Game_{big}^b$，则归约R是合理的。 - **状态分离证明**：Brzuska等人进一步发展了模块化代码编写，将游戏的伪代码结构化为有状态的代码块，这些代码块可以相互调用，但不能访问彼此的状态，即状态分离。若$Game_{big}^b$、归约R和$Game_{small}^b$都通过代码包的调用图定义，可比较“粘合”后的图$R → Game_{small}^b$和$Game_{big}^b$的图。若两个调用图相等，则上述归约合理性等式成立。此外，通过在$Game_{big}^b$的图中画一条切割线即可定义归约R，无需证明归约的合理性和编写归约代码。 #### 2. 相关工作 可视化工具在密码学和计算机科学教学中很常见： - **Vamonos**：结合可视化和（伪）代码方面来传达算法的正确性。 - **ProtoViz和GRACE**：专注于协议中的消息流。 - **Coq和Lean等证明辅助工具的编辑器**：用户提供进一步的证明步骤，会看到仍需证明的陈述。 - **Tamarin**：协议安全性证明器，可显示其内部推理图并逐步更新。 - **prooftree插件**：用于Coq，可帮助以结构化方式直观探索中间声明之间的依赖关系。 - **Alectryon**：允许在文本证明描述和形式验证的证明脚本之间自由切换，提供交互式HTML文档，详细呈现完整证明。 #### 3. 状态分离证明 状态分离证明（SSP）方法不仅规定了游戏跳跃证明的证明风格，还规定了定义风格。与UC框架类似，SSP风格的定义将安全性规定为两个游戏（通常是真实游戏和理想游戏）之间的不可区分性。不可区分性对于可组合性很有用，因为即使对于选择消息攻击下的（强）不可伪造性（UNF - CMA），游戏跳跃通常会用基于日志的理想签名验证替换真实签名验证，使不可区分性游戏之间的归约更直接。 在SSP和UC中，对手是启动系统的主要算法。在UC中，对手通过向环境、模拟器或协议方发送消息来激活它们；在SSP风格的游戏中，对手通过向游戏进行预言机查询来激活游戏。对于游戏Game，用$Pr[1 = A^{O_1,O_2} → Game]$表示对手A与Game的预言机$O_1$和$O_2$交互时返回1的概率，预言机通过操作Game状态的伪代码定义。 以长度加倍的伪随机生成器（PRG）$g : \{0, 1\}^λ → \{0, 1\}^{2λ}$为例，其安全性形式化为一个具有两个GET预言机的游戏： - **理想游戏**：由两个较小的游戏$Key_0$和$Key_1$并行组合而成，$Key_0$和$Key_1$的$GET_0$和$GET_1$预言机分别采样并返回一个均匀随机字符串给对手。 - **真实游戏**：定义两个包$Prg_0$和$Prg_1$，它们的$GET_0$和$GET_1$预言机通过GET预言机从Key包中获取一个密钥，应用PRG g，然后分别返回结果的左半部分和右半部分。 以下是相关代码： ```plaintext Keyid Parameters λ : sec. param State x : string GETid if x = ⊥: x ←$ {0, 1}λ return x Prgid0 Parameters λ : sec. param g : PRG State no state GETid0 x ←GETid() z ←g(x) y ←z1.. λ/2 return y Prgid1 Parameters λ : sec. param g : PRG State no state GETid1 x ←GETid() z ←g(x) y ←z( λ/2 +1)..λ return y ``` PRG的安全性定义如下： **定义1（伪随机生成器）**：一个多项式时间可计算的确定性函数$g : \{0, 1\}^* → \{0, 1\}^*$，对于所有$x ∈ \{0, 1\}^*$，$|g(x)| = 2 |x|$，若对于所有索引$id ∈ \{0, 1\}^*$和所有概率多项式时间（PPT）对手A，以下优势是关于λ的可忽略函数，则g是一个PRG： $Adv(A, G_{prg0}^{id}, G_{prg1}^{id}) := |Pr[1 = A → G_{prg0}^{id}] - Pr[1 = A → G_{prg1}^{id}]|$ 包和对手隐式接收安全参数λ，优势$Adv(A, G_{prg0}^{id}, G_{prg1}^{id})$将值$λ ∈ N$映射到区间$[0, 1]$中的一个数。 为了避免重复定义，允许Key包携带一个位串$id ∈ \{0, 1\}^*$作为索引，并修改预言机和包的名称以消除歧义。 此外，还可以定义伪随机函数（PRF），这里使用根据构造定义游戏的有用约定。 下面用mermaid绘制一个简单的流程图，展示PRG游戏的基本流程： ```mermaid graph TD; A[对手] -->|查询| B[GETid预言机]; B -->|获取密钥x| C{游戏类型}; C -->|真实游戏| D[Prgid0/Prgid1预言机]; C -->|理想游戏| E[Keyid预言机]; D -->|应用PRG并返回部分结果| A; E -->|返回随机字符串| A; ``` #### 4. SSP查看器 为解决基于纸张呈现的局限性，设计了用于SSP的证明查看器CryptoZoo。它在左窗格呈现游戏的声明和调用图，右窗格呈现基于代码的定义，右窗格始终可用，实现了代码链接而无需重复代码，不破坏流程，也无需在当前上下文中滚动离开证明步骤。点击单个包会在代码窗格中突出显示相关代码。 CryptoZoo还解决了数学证明和密码学系统信息呈现方面的障碍： - **信息链接**：除代码外，证明步骤会引用不同方面，包括先前的引理和定义。CryptoZoo将密码学定义和声明链接起来，以便快速检索相关事实，而不丢失当前上下文。 - **信息隐藏**：由于人类记忆有限，读者通常关注当前任务直接有用的事实和信息。CryptoZoo允许用户隐藏文本、定义、引理、声明及其证明，例如专注于特定子树。 - **合理性和结构**：证明由声明和引理构成证明树（或有向无环图）。CryptoZoo使证明树在证明的每个点都可见和明确，同时提供高级树结构和推荐的阅读顺序，让读者可以自由偏离。 #### 5. 案例研究 提供了三个SSP证明查看器的案例研究： - **对称加密**：证明标准的基于游戏的选择明文攻击下不可区分性（IND - CPA）概念与基于模拟的对称加密安全性是等价的。 - **Goldreich - Goldwasser - Micali（GGM）定理**：对（恒定深度）版本的GGM定理进行状态分离证明，该定理使用伪随机生成器（PRG）以树结构构造将PRG转换为伪随机函数（PRF）。此证明涉及二维混合论证，即对树的深度和宽度进行混合论证。使用证明查看器后，该证明变得直观，这也是第一个在SSP中形式化的GGM证明，有助于理解GGM和SSP。 - **姚氏混淆方案**：呈现Brzuska和Oechsner版本的姚氏混淆方案的证明，该方案涵盖分层结构的电路，证明也涉及二维混合论证，对混淆电路的宽度和深度进行论证。虽然该证明仍不简单，但结构得到了显著简化，证明查看工具对于管理大量代码很有用。 下面是案例研究的简单表格总结： |案例研究|内容|特点| | ---- | ---- | ---- | |对称加密|证明IND - CPA和基于模拟的对称加密安全性等价|简单示例| |GGM定理|状态分离证明PRG到PRF的转换|涉及二维混合论证，有助于理解GGM和SSP| |姚氏混淆方案|分层电路的证明|涉及二维混合论证，简化结构，便于管理代码| ### CryptoZoo：用于归约证明的查看器 #### 6. 案例研究细节分析 - **对称加密案例** - **证明思路**：通过构建一系列游戏，逐步将基于游戏的IND - CPA概念向基于模拟的安全性概念转化。在这个过程中，利用状态分离证明的方法，将复杂的证明拆分成多个小步骤，每个步骤对应一个游戏的转换。 - **具体步骤** 1. 定义初始的基于游戏的IND - CPA游戏，该游戏包含真实加密过程和对手的交互。 2. 引入中间游戏，在这些游戏中逐步改变加密过程，使其更接近模拟过程。例如，使用一些基于日志的操作来替换部分真实的加密操作。 3. 最终构建出基于模拟的游戏，证明这个游戏与初始的IND - CPA游戏是不可区分的，从而完成等价性证明。 下面用mermaid绘制一个流程图展示对称加密证明的大致流程： ```mermaid graph TD; A[IND - CPA游戏] --> B[中间游戏1]; B --> C[中间游戏2]; C --> D[基于模拟的游戏]; A -.->|不可区分| D; ``` - **GGM定理案例** - **证明难点**：该证明涉及二维混合论证，即需要同时考虑树的深度和宽度。传统的证明方法在处理这种复杂的二维结构时会变得非常困难，而状态分离证明通过将代码模块化，使得每个模块只处理局部的信息，降低了证明的复杂度。 - **证明过程** 1. **初始化**：定义初始的伪随机生成器（PRG）和相关的游戏。 2. **深度混合论证**：从树的根节点开始，逐步向下进行混合论证。在每一层，通过改变部分节点的输出，使其从真实的PRG输出变为随机输出，证明相邻两层之间的不可区分性。 3. **宽度混合论证**：在每一层内部，对节点的宽度进行混合论证。同样，通过逐步改变节点的输出，证明相邻节点之间的不可区分性。 4. **综合论证**：结合深度和宽度的混合论证，证明整个树结构的不可区分性，从而完成PRG到PRF的转换证明。 以下是一个简单的表格，总结GGM定理证明的关键步骤： |步骤|描述| | ---- | ---- | |初始化|定义PRG和相关游戏| |深度混合论证|从根节点向下，证明相邻两层的不可区分性| |宽度混合论证|在每一层内部，证明相邻节点的不可区分性| |综合论证|结合深度和宽度论证，完成转换证明| - **姚氏混淆方案案例** - **方案特点**：该方案涵盖分层结构的电路，每个层都有不同的功能和操作。证明过程需要考虑电路的宽度和深度，同样涉及二维混合论证。 - **证明改进**：使用状态分离证明和CryptoZoo查看器，将复杂的代码和证明过程进行模块化和可视化。通过点击不同的模块，可以快速查看相关的代码和证明细节，大大提高了证明的可理解性和可管理性。 #### 7. 总结与展望 综上所述，CryptoZoo作为用于归约证明的查看器，在密码学证明领域具有重要的意义： - **优势总结** - **解决呈现问题**：解决了基于纸张呈现证明的局限性，实现了代码链接、信息隐藏和证明树的可视化，使证明过程更加清晰和易于理解。 - **支持复杂证明**：对于涉及复杂概念和二维混合论证的证明，如GGM定理和姚氏混淆方案的证明，提供了有效的辅助工具，降低了证明的难度。 - **促进学习和研究**：通过案例研究，展示了其在教学和研究中的应用价值，有助于初学者理解复杂的密码学概念和证明方法。 - **未来展望** - **功能扩展**：可以进一步扩展CryptoZoo的功能，例如支持更多类型的证明方法和协议，提供更强大的代码分析和验证工具。 - **应用推广**：将其应用到更多的密码学研究和教学场景中，促进密码学领域的发展和交流。 - **用户反馈**：收集用户的反馈，不断优化界面和功能，提高用户体验。 以下是一个简单的列表，总结CryptoZoo的未来发展方向： 1. 扩展功能，支持更多证明方法和协议。 2. 推广应用，应用到更多密码学场景。 3. 收集反馈，优化界面和功能。 总的来说，CryptoZoo为密码学证明提供了一个强大的工具，有望在未来的密码学研究和教学中发挥更大的作用。