跳转到内容
Jason's Study

EasyCrypt — 让密码学家的安全证明能被机器自动检查

是什么

EasyCrypt 是一套让密码学家把”安全性证明”写成程序、由机器自动检查对错的工具。日常类比：以前数学家手写 200 页证明、再让评审人逐行看；EasyCrypt 是把证明翻译成机器能读的语言，再请一位永远不打瞌睡的”自动评审员”来核对。

具体场景：一个新的加密方案出来，作者要证”这个方案安全到什么程度”。这种证明传统上叫游戏跳跃证明（game hopping）——把”攻击者打不破方案”拆成一连串小步，每步只动一点点，最后归约到一个公认困难的数学问题（比如分解大整数）。

EasyCrypt 把这种”一连串小步”写成两个程序之间的关系，再把每一步小改动产生的”验证条件”丢给 SMT solver 自动判。

为什么重要

如果这件事做不到，下面这些今天都不存在：

  • TLS 1.3 协议草案在标准化之前用 EasyCrypt 验过握手安全，避免重蹈 TLS 1.2 多次出 CVE 的覆辙
  • 后量子密码的 NIST 候选方案（FrodoKEM、Kyber 的部分模块）能在选拔阶段拿出”机器证明”作为加分项
  • Signal 协议、安全多方计算（MPC）协议的关键定理被复核，比纯人工审稿可信度高一个量级
  • 把”密码圈天天写 200 页证明、十年还在被审”的工作量，压缩到几千行 EasyCrypt 脚本

更重要的是：它打破了”只有 Coq 老手才能做形式化密码学”的门槛——把交互式定理证明换成”写程序 + 等 SMT 跑”。

核心要点

EasyCrypt 的关键是 三个零件 + 一个想法：

  1. 游戏跳跃法（来自 Shoup 2004）：先把方案的安全性写成 Game_0——攻击者真的去攻击；然后一步步改造游戏，每一步只动一处（如把哈希值替换成均匀随机数），证明相邻两 game 攻击者赢的概率差很小；最后到 Game_n——攻击者除了瞎猜没别的办法。

  2. pRHL（probabilistic Relational Hoare Logic）：用来描述”两个概率程序之间的关系”。普通 Hoare 逻辑讲一个程序：进来满足 P，出去满足 Q；pRHL 讲两个程序：左右两边一起跑，进入时左右状态满足关系 R，出去时满足关系 R-prime。这是描述 game hopping 的天然语言。

  3. SMT 自动化：每一步 hop 产生的”两个游戏在某条件下等价”会被翻译成一阶逻辑命题，丢给 Z3 / Alt-Ergo。SMT 跑通就过；跑不通密码学家改写程序帮 SMT。

那个想法：CertiCrypt（前作，2006）也做这件事，但它是 Coq 里的库，要手写大量交互式 tactic。EasyCrypt 把”高频出现的证明步骤”提炼成独立工具的内置规则，然后把”低层验证”交给 SMT，让密码学家不用学 Coq。

实践案例

案例 1：Hashed ElGamal 加密的 IND-CPA 证明

ElGamal 加密：选随机 r，密文是 (g^r, m XOR H(pk^r))。要证它在随机 oracle 模型下 IND-CPA 安全。

EasyCrypt 里的 game hopping 大致：

  • Game_0：真实 IND-CPA 实验，攻击者选两条消息，挑战者随机选一条加密
  • Game_1：把 H(pk^r) 替换成”如果攻击者从没问过 H(pk^r)，就给均匀随机值”——pRHL 证明两 game 在攻击者没问那个点时完全一样
  • Game_2：把整个密文的右半边换成均匀随机串——攻击者面对均匀随机字节，赢的概率只能是 1/2

每一步都写成一个 pRHL 的引理，SMT 自动验。最后归约到 CDH（Computational Diffie-Hellman 困难假设）。

案例 2：pRHL 在写什么

{ ={glob A, m0, m1} ∧ pk{1} = pk{2} }
  c0 ← Enc(pk, m0)            ~  c1 ← Enc(pk, m1)
{ |Pr[A guesses 0] - Pr[A guesses 1]| ≤ ε }

读法：左边和右边各自是一个程序（左用 m0 加密、右用 m1 加密）；进入时全局状态相等且消息已选；出去时攻击者猜对哪边的概率差不超过 ε。这就是 IND-CPA 的形式定义。

EasyCrypt 把”这条命题对所有概率攻击者都成立”自动翻译成 SMT 可验的小命题。

案例 3：一步 hop 到底在动什么

下面是一段简化到不能再简化的伪代码，假设要把”哈希值”换成”均匀随机串”：

Game_1:                     Game_2:
  k ← KeyGen()                k ← KeyGen()
  r ← {0,1}^n                 r ← {0,1}^n
  h ← H(k, r)                 h ← {0,1}^n         // 直接抽随机
  return Adv(k, r, h)         return Adv(k, r, h)

要证 Game_1 和 Game_2 在攻击者眼里几乎相同。pRHL 的写法：左边状态 = 右边状态、k 和 r 在两边都相等；后置条件是”两边返回值同分布，差距由攻击者询问 H 的次数 q 限制”。

EasyCrypt 把这件事拆成：枚举攻击者询问 H 的所有可能位置 → SMT 验”如果攻击者从没问过 (k, r)，两边完全相等” → SMT 验”问到 (k, r) 的概率 ≤ q / 2^n”。两段都不用人写策略，工具自动跑。

案例 4：和别的工具的分工

工具验什么例子
EasyCrypt数学层：方案 → 困难问题的归约”AES-GCM 在 PRP 假设下安全”
Jasmin实现层：常量时间、无侧信道、汇编正确”这段 AES-GCM 汇编没分支泄露密钥”
ProVerif协议层：消息流不被中间人攻破”TLS 握手的认证性”
F*整合层：用一种语言同时写代码、写规约、做证明”miTLS 完整 TLS 实现”

把它们串起来，才能从”数学定义安全”到”跑在芯片上的代码也安全”。

踩过的坑

  1. SMT 不是万能 oracle：写程序时如果让 SMT 看到太多 quantifier 或非线性算术，它会 timeout / unknown。密码学家要学会”喂给 SMT 它能咽下的形状”——比如把循环展开、把不需要的变量消掉。这反过来要求他懂一点 SMT 内部启发式，不再纯黑盒。

  2. 2011 版本的概率原语很有限：循环、递归、连续分布几乎都不支持。OAEP 的完整证明在论文发表后又花了好几年才补完，因为要先扩工具。

  3. 学习曲线陡到劝退：要同时懂”密码学怎么写 game-based 安全”+“Hoare 逻辑怎么读”+“SMT 怎么投喂”+“EasyCrypt 自己的语法”。社区花了十年写教程降门槛，2020 年左右才出现”密码学博士能在三个月学会用”的状态。

  4. 机器证明 ≠ 现实安全：EasyCrypt 证的是”在你写下的安全模型里这个方案安全”。如果模型漏掉了真实攻击面（侧信道、错误注入、协议组合时的微妙交互），机器证明也救不了你。

  5. 可证不等于审过：EasyCrypt 脚本通过不代表别人能复现你的证明——脚本里可能有大段 admit（占位）、可能依赖某个非标准引理、可能调了一个超时阈值才跑通。社区后来加了”严格模式”和”无 admit”标记，但早期论文里的脚本不一定干净。

  6. 代码和数学的口径要对齐：你证的是论文里的伪代码，但实现是 C/Rust。如果伪代码写错（少了一个边界检查），机器再怎么验也救不回来。这是后来 Jasmin + EasyCrypt 联动想解决的问题。

适用 vs 不适用场景

适用：

  • 新设计的密码方案要给出可信安全证明（IND-CPA / IND-CCA / EUF-CMA 这种标准目标）
  • 标准化场景（TLS、KEM 候选、政府密码标准）需要可重复验证
  • 已有手写证明想”复核一遍”——常常能挖出原证明里的小漏洞

不适用：

  • 验密码代码本身的实现正确性 → 用 Jasmin / Cryptol
  • 验协议层不被中间人 → 用 ProVerif / Tamarin
  • 物理侧信道、量子攻击模型 → 还在研究阶段，工具支持有限
  • 项目预算只够”写完跑通” → 形式化是 2-10 倍工作量

历史小故事（可跳过）

  • 2004：Victor Shoup 写《Sequences of Games》白皮书，把密码圈零散的 game hopping 技巧梳理成方法论。这是”机器化”的前提——先得有规律可循。
  • 2006：Barthe 等人写 CertiCrypt——一个 Coq 库，能在 Coq 里做 game hopping。能跑，但要手写交互式 tactic，密码学家用不动。
  • 2011：EasyCrypt 出现。把 CertiCrypt 里”密码学家用得最频繁”的证明模式提炼成独立工具，把交互式证明换成 SMT 自动化。论文 20 页，CRYPTO 接收。
  • 2013+：miTLS、TLS 1.3 草案、FrodoKEM、Kyber 的安全归约都在 EasyCrypt 里走过。
  • 2020s：MPC 协议（如 SPDZ 系列）、零知识证明（Groth16 的可靠性）也开始用 EasyCrypt 复核。

学到什么

  1. 机器证明的关键不是”更严格”，是”可重复”：手写证明对了也是对了，但每次有人审都要重新读 200 页；机器证明审一次过了，下次工具变了重跑就行。
  2. SMT 自动化 + 高层逻辑 是当代形式化的标配组合：纯交互式证明（Coq、Lean）门槛高；纯 SMT（直接喂 Z3）表达力差。把高层逻辑（pRHL）搭在 SMT 上，能兼顾”密码学家能读”和”机器能跑”。
  3. 专用工具打败通用工具：EasyCrypt 不试图证一切，只证密码归约这一种事。CertiCrypt 用通用 Coq 也能做，但密码学家根本学不动。“窄而深”的工具往往比”宽而通用”的工具更能落地。
  4. 理论 → 工具 → 标准化 的路径：Shoup 2004（理论）→ CertiCrypt 2006（原型）→ EasyCrypt 2011（工具）→ TLS 1.3、NIST PQC（标准）。每一步隔几年，没有捷径。
  5. 关系语义是现代形式化的隐藏主线：pRHL 用”两个程序的关系”表达安全，恰好对应安全性的本质——“区分不出来”。等价、独立、不可区分都是关系性质。一旦把这件事看清，很多看似不同的形式化工作（差分隐私、信息流、密码归约）都长一个样。

延伸阅读

  • 论文 PDF：Barthe-Grégoire-Heraud-Béguelin 2011（20 页，密度高，但前 8 页可读性不错）
  • 工具官网与教程：EasyCrypt 项目主页（含 docker 镜像、入门示例）
  • 背景白皮书：Shoup《Sequences of Games》（2004）——理解 game hopping 思路必读
  • Barthe 等人在 FOSAD 暑期学校的讲义（搜 “Barthe FOSAD EasyCrypt”），比论文友好

关联

  • hoare-logic —— pRHL 是 Hoare 逻辑的概率 + 关系版本
  • isabelle-hol-2002 —— 通用证明助手；EasyCrypt 选了”专用”路线，对照参考
  • lean-prover —— 同代通用证明助手；EasyCrypt 走了和它相反的”窄工具 + SMT”路线
  • fstar —— 把代码、规约、证明放一种语言；EasyCrypt 只管证明这一层
  • stainless-2017 —— 同样”高层逻辑 + SMT”思路，但目标是 Scala 程序而非密码归约
  • proverif-2001 —— 协议层验证，与 EasyCrypt 的数学层验证互补
  • [[tls-1.3]] —— TLS 1.3 标准化过程中用 EasyCrypt / F* 复核过握手安全
  • csp-hoare-1978 —— Hoare 1978 的 CSP，与 Hoare 逻辑同源；EasyCrypt 借的是后者