第 5 章 · 机器审讯：形式化验证实战
第 5 章 · 机器审讯：形式化验证实战
章节摘要：人工推演有天花板——3.1 节的漏洞潜伏了十七年才被找到。本章把推演交给机器：先用 BAN 逻辑练推理的手感（一页纸推完一个小协议），再用 ProVerif 走一遍从协议文本到模型、从模型到结论的完整建模流程，最后学读攻击迹——机器给出的反例如何翻译成协议缺陷、又如何驱动修补。读完你能对一个中小协议独立完成一次符号验证，并判断验证结论的适用边界。
学习目标
读完本章，你应当能够：
- 写出 BAN 逻辑的核心推理规则（消息含义、临时值校验、仲裁规则），并对一个三步协议完成纸面推理；
- 说出 BAN 逻辑的理想化步骤为何是它最大的软肋，以及后续逻辑体系如何修补；
- 把一份协议描述翻译成 ProVerif 模型：角色进程、通道、事件与查询四件套；
- 读懂验证器的三种输出（命题成立、攻击迹、模型问题），并把攻击迹逐步翻译回协议层面的缺陷；
- 对"验证通过"给出诚实的边界声明：模型覆盖了什么、抽象掉了什么、结论不能外推到哪里。
核心概念速览
本章浓缩成一句话：形式化验证把"我们仔细检查过了"变成"在以下模型假设下，此命题已被穷尽地检查"——它不制造安全，它把检查的完备性变成可陈述的事实。
子章节导航
- 5.1 BAN 逻辑手推一页纸：1989 年的开山之作把"信念"变成可推演的对象。本节给四条核心规则，把 1.1 节的 NS 对称版本完整推一遍，再复盘它的理想化软肋——为什么它的结论必须降级使用。
- 5.2 ProVerif 建模推演实录：当代符号验证的主力工具。本节走完建模四件套（进程、通道、事件、查询），给出一个可照抄结构的完整模型示例，讲清"模型错了工具不负责"这条铁律。
- 5.3 攻击迹解读与协议修补：验证器输出攻击迹之后的工作才是真功夫。本节给攻击迹的逐段读法（哪些是会话拼接、哪些是重放、哪些是建模失误的假阳性），以及修补后的回归验证流程。
子章节之间的逻辑关系
三节是"推理 → 自动化 → 解读"的工具进化线：BAN 教会机器之前的人怎么系统地推理（也暴露了人为什么需要机器），ProVerif 把穷尽检查自动化，攻击迹解读则是人机分工的接口——机器找反例，人判断反例是真缺陷还是模型失误。三节合起来回答第 3 章悬置的问题：NS 漏洞能不能在发表当年就被找到——能，而且本章你会亲手做到。
信念推理(5.1) ──暴露人工极限──> 穷尽自动化(5.2) ──产出需要人接──> 攻击迹解读(5.3) │ │ │ 为什么需要机器 机器怎么穷尽 人怎么接机器的案卷
图 5-1 形式化验证工具版图：从信念逻辑到状态探索
选型速查：什么场景请哪位审讯官
| 你的处境 | 合适的工具 | 理由与代价 |
|---|---|---|
| 协议评审会的快速纸面筛查 | BAN 类信念逻辑 | 半小时出结论；理想化主观，结论须降级表述 |
| 认证与密钥协议全自动找漏洞 | ProVerif | 不限会话数、速度快；近似机制可能误报 |
| 有状态协议（计数器、轮次、阶段） | Tamarin | 能表达状态演化；建模与求解更费工 |
| 教学与小型协议推理练习 | BAN 或 Scyther | 规则可见、反馈直观 |
| 修补后的回归验证 | 原工具重跑并加邻接查询 | 贵在模型资产化，一次性使用等于白验证 |
这张表的一句话版：快筛用信念逻辑，定案用模型检测，修补后必须回归——三句话各自对应本章三节。选型最常见的两个错误都值得点名：拿 5.1 的纸面结论当最终判决，3.1 节的历史演示过这种用法的代价；因为"建模也要花工夫"而干脆不做任何验证，那是把"不完美的检查"与"不检查"混为一谈——5.2 节的实录会展示一次入门建模其实只花一个下午。
前置知识与后续延伸
前置是 2.1 节的 Dolev-Yao 四项能力（本章所有模型都在给它们编码）与 4.1 节手推的 TLS 握手（5.2 的模型示例会建模它的一个简化变体）。往后看：6.1 的后量子迁移里，混合密钥交换的正确性论证大量依赖本章的工具与思路；6.3 的部署守则里，"降级路径是否可被操纵"这类检查项本质上就是本章的验证查询在工程清单里的投影。