6.2 可证明安全到底在证明什么

6.2 可证明安全到底在证明什么

本节摘要："这个方案有安全证明"常被当成免检标志，但证明的价值取决于你能不能读懂它证了什么、基于什么假设。本节拆解归约证明的逻辑骨架，教安全位数的正确读法，并演示"假设被打破"时证明如何失效——RSA 事件、离散对数的量子威胁都是现成案例。读完你能评估一个迁移方案的证明资格，而不是被一句"可证明安全"打发。

证明的结构：一个三段论

可证明安全的全部内容是一个三段论。大前提：某个数学问题很难（离散对数、大数分解、格上最短向量）。小前提：若存在敌手能在模型里攻破方案，就能构造出一个算法把敌手当作子程序，用来解那个困难问题。结论：困难问题若真难，敌手就不存在。关键在小前提的构造——它叫归约：把"破方案"转化为"解难题"的机器。证明读起来就是审查这台机器造得对不对：输入（敌手的成功）与输出（难题的解）是否匹配、调用的次数是否在预算内、模拟的环境与真实环境的差距是否可忽略。

三段论的结构立刻暴露了它的两个软肋都是"前提"而非"逻辑"。其一，大前提是假设——"离散对数难"没有被证明，它是几十年无人推翻的经验事实；证明把方案的安全性归约到它，但无法证明它本身。其二，模型是让步的（2.1、2.3 节）——随机预言机模型里那个"完美哈希函数"在现实中并不存在，标准模型更严谨但证明更难。所以"有证明"的真实含义永远是：在某某模型、某某假设下，破坏方案的代价不小于解某某问题的代价。这句话的每个空都要填上才算读懂了证明。

安全位数的读法

评估报告里"128 位安全"这类表述需要校准。位数的含义是：最优已知攻击的工作量约为 2 的 128 次方次运算。三个常见误读要掰正。其一，位数是针对最优已知攻击的——是"我们对这个问题的最好算法有多快"的函数，问题被研究得越透彻，这个数越可信；一个刚提出五年的假设宣称高位数，与一个被攻击了四十年的假设宣称同样位数，含金量不同。其二，位数跨问题不可直接比较——对称密钥的 128 位与格问题的 128 位背后的"最优攻击"研究成熟度不同，迁移评估时要说的是"归约到哪个问题、该问题被攻击了多少年"。其三，位数会随攻击进展下调——历史上的 RSA 假设就经历过参数建议数度上调的过程，选参数要留裕量并跟进行业参数建议的演进。

假设被打破时：证明如何失效

证明的三段论结构决定了失效方式：大前提塌，结论跟着塌——逻辑本身不会错，错的是世界不再满足它的前提。两个现成案例。其一，经典侧的教训：某些基于因数分解假设的参数，随着分解算法与算力的进步被迫一再加长；假设没被"证明为假"，只是"难度曲线"移动了，证明给出的安全位数随之贬值。其二，正在发生的：量子算法（Shor 类算法）让离散对数与大数分解在足够大的量子算力下变为易解——上一章"换前提"的理论内涵就在这里：不是协议逻辑出了错，而是大前提塌了，所有压在这条前提上的证明同时失效。这也是 6.1 节说"迁移不是换算法而是换命题前提"的理论出处。

失效的正确响应也有结构：更换归约目标（换到新的困难问题）、重做归约（新算法的新证明）、重新审查组合（混合方案里两个证明各自的前提独立吗——若两个算法恰好都归约到同一条正在动摇的前提，混合的双保险就是幻觉）。最后这一条是混合方案评估里最容易被跳过、也最致命的一问：双保险的"双"必须指向不同的困难问题，保险才独立。

💡 评估新方案时的一句话模板："该方案在某某模型下，把破坏某某性质的代价归约到某某问题；该问题有某某年的攻击研究史，最优攻击的复杂度被认为如何。"能填满这个模板，评估就及格了；填不满，说明材料没读完。

归约证明的骨架长什么样

读证明之前先看一眼证明的"源代码"形态。真实的证明论文有几十页细节，但骨架都可以压缩成下面这样的伪代码——评审新方案时，你要检验的就是这段骨架的每一行是否成立。

【归约证明骨架 · 伪代码形态】
假设: 问题 P 是难的 (如: 格上最短向量问题无可行解算法)
目标: 方案 S 在模型 M 下满足性质 Q

归约器 R 的构造:
  输入: 一份问题 P 的实例 I
  1. 把 I 巧妙嵌入 S 的公钥与模拟环境       ← 嵌入是否可行?
  2. 把敌手 A 当子程序运行, A 与模拟环境交互
     —— 模拟必须让 A 感觉与真实协议无差别   ← 模拟差距可忽略?
  3. 若 A 攻破 S (以不可忽略概率), 用 A 的输
     出提取出 I 的解                        ← 提取器构造成立?
  4. 统计: A 成功率 ε → R 解 P 成功率约 ε/损耗因子
结论: 若 P 难, 则 ε 必可忽略, 即 S 满足 Q     ∎
​

四个箭头标注处就是审证明时真正要盯的接口。嵌入处决定证明覆盖哪类敌手查询；模拟差距决定模型让步有多大（随机预言机模型的让步就发生在这里）；提取器是"破方案变成解难题"的换能器，构造有漏洞则全证明作废；损耗因子决定安全位数要打几折——归约松的方案，128 位的名义参数折完可能只剩几十位的实际保证。这四问不需要你能重演证明全文，但能让你把"有没有证明"的问题升级为"证明在哪一层可能漏水"的问题——后者才是迁移评审要的回答。

十分钟读完一份证明的流程

给一个可照做的快速审读流程。第一分钟，读定理陈述：抄下"在某某模型下、基于某某假设、方案满足某某性质"的完整句式，空没填全就停下提问。第二到四分钟，找归约方向：确认"假设 A 难则方案 S 安全"的方向没被写反，并找出损耗因子。第五到七分钟，扫模型声明：随机预言机还是标准模型、敌手是静态还是自适应、查询次数有没有界。第八到十分钟，对照参数：论文的安全位数表是在哪个假设强度下算的、与行业参数建议是否一致。十分钟到不了的部分（重演证明细节）本来就不是评审者的义务——评审者的义务是把让步与假设从论文里拎出来、摊在决策桌上。

这套流程与第 5 章的模型声明纪律是同一件事在两个世界的投影：符号验证要写"模型覆盖了什么"，证明评审要写"证明假设了什么"——都是给结论标定适用边界的诚实动作。

最后留一个诚实边界的说明：可证明安全证明不了实现。归约证明的敌手是数学对象，不含侧信道、不含随机数缺陷、不含内存越界——3.3 节的全部教训都在证明的辖区之外。所以"有证明"与"可信部署"之间还隔着实现审计、参数配置与生命周期管理，它们是 6.3 节的地盘。把证明放进整套评估的正确位置：它是"设计层逻辑自洽"的最强证据，是迁移评审的必要条件，但从来不是充分条件。评审会上若有人说"这是可证明安全的所以不用再评"，本节就是你反驳的出处。

本节要点回顾

• 证明是三段论：困难问题假设 + 归约构造 + 结论；两个软肋都在前提——假设未被证明、模型有让步。
• "有证明"的完整句式：在某某模型、某某假设下，破坏代价不小于解某某问题；空没填全等于没读懂。
• 位数三个误读：只针对最优已知攻击、跨问题不可比、会随攻击进展下调——选参数留裕量并跟随演进。
• 假设塌则证明塌：RSA 参数上调与量子威胁都是"前提移动"而非"逻辑出错"；响应是换归约目标、重做证明。
• 混合方案必问独立性：两个算法若归约到同一条动摇的前提，双保险是幻觉。

下一节到部署层收尾：协议与算法的保证如何被一个配置项、一次静默降级、一枚过期证书放倒——最后一公里的守则清单，每条都挂着攻击史的案号。