3.1 Needham-Schroeder 十七年漏洞复盘

3.1 Needham-Schroeder 十七年漏洞复盘

本节摘要：1978 年发表的 NS 公钥认证协议，其认证缝隙直到 1995 年才被 Lowe 找出——期间被无数教材引为范例。本节按固定解剖程序复盘：声称的命题、攻方思路的完整逻辑链、命题被击穿的位置、防御设计的改写。攻方全程只用协议允许的合法消息，这正是本案例最值得咀嚼的地方：协议逻辑的缝隙不需要破解任何密码学。

案例背景：一个被选入教材的协议

回到 1.1 节拆解过的 NS 公钥三步协议：A 发起，用 B 的公钥加密自己的身份和临时值 Na；B 回以 Na 加上自己的临时值 Nb，用 A 的公钥加密；A 解出 Nb 作回执。设计意图漂亮：三步之后，双方各自确认了对方在线、持有对应私钥，且共享两个旁人不知道的临时值，可以派生会话密钥。它结构简洁、思路清晰，被大量教材与综述引用为公钥认证的示范——这个地位恰恰是本案第一个教训：简洁易懂与安全无关，被广泛引用也无关。

按 2.3 节模板写出它声称的命题：在"公钥正确绑定身份"的前提下，敌手无法让 B 相信"自己在与 A 对话"，除非 A 确实参与了该次对话。请记住这个命题的措辞，特别是"公钥正确绑定身份"这个前提——后面的一切都围绕它展开。

攻方思路：完整逻辑链

Lowe 找出的攻击需要三个参与者：诚实的 A、诚实的 B，以及敌手 I。前提只需一条：A 愿意与 I 发起一次正常对话（比如 I 冒充一个合理的服务对象，A 主动找 I 通信——这在现实里毫无难度）。攻击分两个阶段。

第一阶段，I 与 A 做一次正常的 NS 对话，从而持有这次对话的临时值（记为 Na）。这一步没有任何越界：I 与 A 的对话是完全合法的协议执行。

第二阶段，I 转头去找 B，冒充 A 发起对话。关键动作在消息 1：I 把消息 {A, Na}Kb 发给 B——注意这条消息是逐字合法的，NS 协议本身允许任何主体发出这样的消息，A 的身份以密文形式躺在里面，除了 B 没人能看到内容，所以 B 无法从外部区分"这条消息是 A 发的"和"这条消息是 I 转发的"。B 按协议回复 {Na, Nb}Ka，I 解不开 Ka 下的内容，但协议不需要他解开：他把这条消息原样转给 A。A 一看，里面有自己的 Na，按协议理解为"B 在与自己对话"，于是尽责地解出 Nb、加密后交还——但交还给谁？交还给 I（因为 A 以为当前对话对象是 I）。I 拿到 {Nb}Kb，转手交给 B。B 解出 Nb，与自己发出的一致，认证完成：B 坚信自己刚刚与 A 完成了一次协议握手，而 A 从头到尾以为自己在和 I 对话。

图 3-2 Lowe 攻击时序：两条协议会话拼出一条错误认证

解剖：命题的哪个要素被击穿

回看命题："在公钥正确绑定身份的前提下，敌手无法让 B 误信 A 参与了对话。"攻击里公钥绑定没有任何问题——I 的公钥就是 I 的，A、B 的也都是真的。被击穿的是不可行陈述的措辞：设计者心里想的命题是"A 与 B 之间的对话"，但协议机制实际能保证的是"每条消息出自某个持有对应私钥的人"——这两者之间隔着"消息里是否显式写明对话双方"这道缝。A 的身份只在消息 1 出现，且藏在只有 B 能解的密文里；B 发出的消息 2、消息 3 里完全没有"我在和谁说话"这个字段。没有显式绑定，认证机制就只能对"消息的密码学来源"负责，对"会话的整体归属"失职。

这个教训被概括为 Lowe 自己提出的匹配性（agreement）概念：真正的认证要求"两条会话的消息在双方视角里逐条对应、包括对方身份字段一致"，而不是弱得多的"消息能通过密码学验证"。今天所有协议规范里"在消息中显式包含双方身份与角色"的写法，都可以追溯到本案——TLS 1.3 握手里你会看到身份信息被反复织入每一条需要它的消息，那不是冗余，是本案交的学费。

防御变式与修复成本

修复本身便宜得令人心酸：在消息 2 里写上 B 的名字（{Nb, B}Ka），I 的拼接立刻失效——A 收到写着 B 的回执时，会发现自己正在执行的对话（对象是 I）与回执声称的对象（B）对不上，攻击链断在第二步。改动是一个字段，检出漏洞用了十七年。不对称的成本结构正是协议分析这门学科存在的理由：防住一个逻辑缝隙的代价是写一个字段，而找出它的代价若靠人肉试错，可能是十七年——5.2 节会演示，符号验证工具在模型正确的前提下几分钟能找到同一个缝隙。

还有一个值得单独强调的变式教训：NS 当年还有对称密钥版本（依赖可信服务器），那个版本经 BAN 逻辑分析后补充了改动；而公钥版本的漏洞恰恰说明同一族协议的两个变体不能因为"长得像"就共享安全结论——每个变体都是独立协议，需要独立验证。这个纪律在今天依然常被违反：换了信道环境、换了消息方向就宣称"安全性同原协议"，是安全评审里最应该拦下来的表述。

攻击迹预览：用第 5 章的语言复述本案

本案还有一个值得提前预支的价值：它是符号验证工具的"标准考题"，今天任何一个验证工具的教程几乎都拿它做第一个演示。用 5.2 节会介绍的语言，机器给出的攻击迹大致长下面这个样子——现在不必逐行读懂，只需要感受两件事：攻击被压缩成几行机械的会话拼接；每一步都对应上文人工推演的某个动作。

【Lowe 攻击 · 机器攻击迹的形态（简化示意）】
会话1: A 与 I 执行 NS → I 获得语句 {A, Na} 用 I 的公钥加密
会话2: I 冒充 A 向 B 发起 → 发送 {A, Na} 用 B 的公钥加密
  B 应答 {Na, Nb} 用 A 的公钥加密 → I 无法解密 → 原样转发给 A
会话1: A 视其为对话第 2 步 → 应答 {Nb} 用 I 的公钥加密
会话2: I 将其改封转交 B → B 验证 Nb 一致
结论: B 相信与 A 完成认证, 但 A 的对话对象是 I —— 认证命题被违反
​

两件事值得咀嚼。第一，人工十七年、机器几分钟，差距不在智力而在穷尽：人会不自觉地假设"A 不会同时和两个人跑协议"，机器没有这种社交礼仪，它把所有会话的所有拼接方式都试了一遍。第二，攻击迹的可读性依赖你今天练的手感——会话、消息、临时值这些记账词汇正是 5.2 节建模的原材料。这也是本册把人工推排放机器之前的理由：没有手推经验的人拿到攻击迹，读到的只是一串符号。

顺手回答一个读者此刻多半在想的问题：这么著名的协议、这么多的引用者，为什么十七年没人撞上这个攻击？答案有两条，都不体面。一是攻击超出直觉的搜索空间——人会下意识假设"会话是独立、成对的"，而拼接攻击恰恰活在会话的组合里，人脑不枚举组合；二是工具缺位——当年没有能在无界会话上穷尽搜索的验证器，BAN 逻辑推的是单个会话内的信念流，恰好对会话间拼接免疫。两条合起来就是本章存在的理由：直觉有结构性盲区，盲区需要机器补位——这个论断到第 5 章会变成可操作的流程。

本节要点回顾

• 攻击全程合法：Lowe 攻击只用"发起合法对话 + 转发解不开的密文"，没有任何密码学被破解——逻辑缝隙与数学难度无关。
• 病根是隐式绑定：消息里不显式写对话对象，两段合法会话就能被敌手拼接成一次错误认证。
• 命题措辞即防线："每条消息来源可验"与"会话整体归属正确"是两个强弱悬殊的命题，认证要的是后者（匹配性）。
• 修复便宜、检出昂贵：加一个身份字段即可封死，但人肉检出花了十七年——这正是形式化工具的价值论证。
• 变体需独立验证：对称版本与公钥版本的安全结论互不覆盖，"长得像"不是安全论证。

下一节的 WEP 案例把镜头从逻辑层移到原语层：协议没走错任何一步，但选材与拼装的三处误用互相放大，最终整条产品线失守。