Game Hopping in Lean

想象一下你是一位顶尖的锁匠，正试图证明你的新保险库是坚不可摧的。你不会只说“它很强！”而是要展示一系列步骤：“如果你打不开这把小锁，你就打不开这扇门；如果你打不开这扇门，你就打不开这个保险库。”这就是现代密码学的运作方式。专家们使用“游戏”来测试安全性，即黑客试图猜出一个秘密，而系统的安全性是通过证明“破解它就等同于解决一个已知的、不可能完成的谜题”来得到证明的。但问题在于：手工进行这些证明就像是在飓风中试图平衡一座纸牌屋。极易出错，可能会遗漏细微的缝隙或陷入复杂性之中，而且如果你漏掉了一个步骤，整个证明就会崩塌。这就是为什么科学家们一直在寻找一种让计算机检查每一张纸牌的方法，以确保这座纸牌屋屹立不倒。

这就是这篇论文的意义所在。作者在名为 HOPSCOTCH（一个关于跳跃游戏的俏皮名称）的框架内，在一个强大的计算机程序 Lean 4 之中，构建了一个数字工作坊。你可以把 HOPSCHOTCH 想象成一个超级聪明的机器人校对员，它不仅检查你的数学逻辑，还能理解安全证明背后的“故事”。HOPSCOTCH 不会强迫密码学家使用一种奇怪且受限的语言，而是允许他们使用自己进行所有其他数学运算时所用的工具来编写证明。它将“游戏跳跃”（从一个安全场景跳转到下一个场景）的过程，转化为了一个清晰、循序渐进、可供计算机检查、验证甚至辅助自动化的对象。作者不仅构建了这个工具，还用它成功证明了几种著名加密方法的安全性，包括一个复杂的构造——GGM，从而证明了这个“机器人校对员”可以处理现实世界的密码学挑战而不会感到困惑。

大局观：为什么我们需要一个校对机器人

在数字安全领域，我们依赖于“可证明安全性”。这意味着我们不仅仅是希望我们的代码是安全的，而是尝试去证明它。实现这一点的标准方法是“基于游戏的”方法。想象一名保安（系统）和一名窃贼（对手）。保安有一个秘密，而窃贼试图猜出它。为了证明保安是安全的，我们不仅仅说“他很可靠”，而是创建一系列“游戏”或场景：

1. 真实游戏： 窃贼试图破解实际的系统。
2. 跳跃： 我们设想一个略微不同的游戏，它与原游戏几乎相同，但更容易分析。我们证明如果窃贼能在“真实游戏”中获胜，那么他们也能在新的、略有不同的游戏中获胜。
3. 链条： 我们不断地从一个游戏跳向另一个游戏，每次只微调规则，直到达到一个显然不可能获胜的最终游戏（比如连续一百万次正确猜中硬币的正反面）。

如果我们能证明每一个“跳跃”都是安全的，那么整个链条就是安全的。这被称为“游戏跳跃证明”。

问题在于，人类很难完美地做到这一点。这些证明冗长、杂乱且充满细节。一个被遗漏的细节就可能导致整个证明失效，进而导致系统不安全。多年来，研究人员一直试图构建专门的计算机工具来检查这些证明，但这些工具通常说着一种与数学家不同的语言。它们就像是一个只懂“安全术语”却不懂“数学语言”的翻译官，迫使专家们在两者之间来回转换想法，这既缓慢又容易出错。

HOPSCOTCH 登场：通用翻译器

本文的作者 Stefan Dziembowski, Grzegor Fabiański, Daniele Micciancio 和 Rafał Stefański 决定搭建一座桥梁。他们在 Lean 4（一个用于验证数学证明的流行计算机程序）内部创建了 HOPSCOTCH。

HOPSCOTCH 的神奇之处在于：

• 无需新语言： 不同于其他强制你学习一种受限的新编程语言的工具，HOPSCOTCH 让你使用标准的 Lean 来编写证明。这就像是让厨师用自己最喜欢的刀具烹饪，而不是强迫他们使用塑料刀。
• 证明即对象： 在 HOPSCOTCH 中，证明不仅仅是一堆文本，它是一个结构化的对象，就像一个乐高模型。游戏中的每一次“跳跃”都是一个特定的乐高积木。你可以将它们拼在一起，计算机也会检查它们是否完美契合。如果你试图连接两个不匹配的积木，计算机就会说：“不行，这行不通。”
• “抽象”技巧： 这些证明中最难的部分之一是证明两个看起来不同的系统行为完全一致。HOPSCOTCH 使用了一种巧妙的技巧，称为“状态抽象”。想象你有两个机器人，一个内部布线混乱，另一个布线整洁。HOPSCOTCH 允许你绘制一张图（抽象函数），展示混乱的布线如何对应于整洁的布线。如果这张图是正确的，计算机就知道即使这两个机器人的外观不同，其行为也是一致的。

他们实际做了什么以及发现了什么

作者不仅构建了工具，还对其进行了测试。他们使用 HOPSCOTCH 形式化验证了四个主要的密码学概念：

1. 先加密后 MAC (Encrypt-then-MAC)： 一种使消息既保密又防篡改的方法。他们证明了如果底层的加密和“标签”（MAC）是安全的，那么整个系统对于即使是最聪明的黑客也是安全的。
2. ElGamal 加密： 一种利用公钥发送秘密信息的著名方法。他们展示了如何基于一个被称为“判定 Diffie-Hellman (DDH) 假设”的难题来证明其安全性。
3. 单次保密性到 IND-CPA： 他们证明了如果一个系统对于单条消息是安全的，那么它可以被构建为对多条消息也是安全的，这是构建鲁棒加密的关键步骤。
4. GGM 构造： 这是重头戏。GGM 方法将一个简单的随机数生成器转化为一个复杂的“伪随机函数”（一种看起来像真随机数的假随机数生成器）。之前的计算机证明只能处理非常浅层的版本（例如 3 层树结构）。作者使用 HOPSCOTCH 证明了 GGM 的非恒定深度安全性，这意味着它适用于任何规模的树。据他们所知，这是第一个成功验证这种特定复杂构造的通用型计算机证明辅助工具。

他们是如何实现的（“游戏”机制）

论文解释说，HOPSCOTCH 通过将证明分解为特定的步骤或“构造器”来工作：

• 观测等价性 (Observational Equivalence)： 证明两个游戏在外部观察者看来是相同的。
• 归约 (Reductions)： 展示如果能破解游戏 A，就能破解游戏 B。
• 混合序列 (Hybrid Sequences)： 将许多微小的步骤串联在一起。

该框架包含“策略”（自动化助手）来尝试为你解决这些步骤。例如，如果你需要证明两个预言机（游戏系统）是相同的，计算机可能会自动尝试寻找一个“状态抽象”映射。如果它找不到，它会将该步骤留给人类解决，但会保持结构完整，以便人类知道自己处于什么位置。

作者还证明了一个“计算健全性定理”。这是一种高级说法，意思是：“如果计算机说这个证明有效，那么它在现实世界中确实有效。”他们表明，对于 HOPSCOTCH 创建的每一个证明对象，你都可以根据证明中所使用的假设，精确地计算出黑客能获得的“优势”是多少。这确保了计算机不仅仅是在玩自己的游戏，而是给出了一个真实、具体的安全保证。

总结

论文得出结论，HOPSCOTCH 成功地弥合了专用安全工具的便利性与通用数学辅助工具的强大功能之间的鸿沟。它允许密码学家编写更易读、更易检查且不易产生人为错误的证明。虽然作者承认计算机目前还无法检查“黑客”运行速度是否足够快（这是一个被称为“多项式时间”的技术细节），但他们已经为实现全自动、可信的安全证明奠定了基础。

他们还暗示了未来：有了这些结构化的证明对象，很快就有可能利用人工智能来辅助自动编写这些证明，或者将系统扩展到处理涉及“坏事件”和概率的更复杂场景。但就目前而言，主要成就显而易见：他们建立了一种可靠、灵活且强大的方式，让计算机能够帮助我们证明数字秘密的安全。