Needham-Schroeder 协议与攻击

Needham-Schroeder 协议（1978 年）是最早尝试使用可信第三方（TTP）设计密码认证协议的方案之一。其目标是：让 Alice 和 Bob 能够相互认证，并借助与各个主体共享长期密钥的可信身份认证服务器（AS）建立共享会话密钥。该协议早于公钥基础设施，但引入了随机数保证新鲜性、通过可信服务器分发密钥等概念，而这些概念至今仍是 Kerberos 等现代协议的核心。理解 NS 及其缺陷，塑造了整个协议分析领域。

NS 对称密钥协议分为五步。(1) Alice 向 AS 发送 {A, B, Na}，请求与 Bob 通信所需的会话密钥。(2) AS 向 Alice 回复 {Na, B, Kab, {Kab, A}_Kb}_Ka，其中包含会话密钥 Kab 和给 Bob 的票据，全部使用 Alice 的长期密钥 Ka 加密。(3) Alice 将票据 {Kab, A}_Kb 转发给 Bob。(4) Bob 解密票据，提取 Kab，并向 Alice 发送 {Nb}_Kab 作为挑战。(5) Alice 回复 {Nb-1}_Kab，证明自己持有 Kab。随机数 Nb 可防止第 4 步遭到重放。该协议存在一种已知的重放攻击，后来被 Denning 和 Sacco（1981 年）利用。

Denning 和 Sacco（1981 年）发现了一个缺陷：第 2 步中的 AS 响应不具备新鲜性，因为其中没有服务器提供的时间戳或随机数。攻击者 Mallory 如果之前截获过旧的会话密钥 Kab（通过攻破过去的会话），就可以在之后的任何时间将旧票据 {Kab, A}_Kb 重放给 Bob。Bob 收到看似来自 Alice 的合法票据后，会使用已泄露的密钥 Kab 建立会话。Denning 和 Sacco 的修复方案是：在 AS 响应和票据中加入时间戳。Kerberos 采用了这一方案——时间戳被嵌入票据中，以限制票据的有效时间窗口。

NS 公钥协议（同样发表于 1978 年）旨在使用公钥密码学实现两方相互认证。(1) Alice 向 Bob 发送 {Na, A}_PKb（使用 Bob 的公钥加密的随机数 Na）。(2) Bob 回复 {Na, Nb}_PKa（两个随机数，使用 Alice 的公钥加密）。(3) Alice 回复 {Nb}_PKb（将 Bob 的随机数使用他的公钥加密后返回）。交换完成后，双方都持有两个随机数（Na、Nb），可以据此派生会话密钥。该协议看似安全了 17 年，直到 Lowe 在 1995 年发动攻击。

Gavin Lowe（1995 年）使用组合推理失败（FDR）模型检查器发现了一个关键缺陷。Mallory 可以在向诚实的 Bob 转发消息的同时冒充 Bob 欺骗 Alice。第 1 步：Alice 将 {Na, A}_PKm 发送给 Mallory，以为自己正在与 Bob 通信。Mallory 将 {Na, A}_PKb 转发给 Bob。第 2 步：Bob 回复 {Na, Nb}_PKa，Mallory 将其解密后再为 Alice 重新加密：{Na, Nb}_PKa。Alice 解密并提取 Nb。第 3 步：Alice 将 {Nb}_PKm 发送给 Mallory，以为这条消息会发给 Bob。Mallory 将其解密后转发为 {Nb}_PKb 给 Bob。Bob 以为自己已经与 Alice 完成了相互认证，但实际上 Alice 认证的是 Mallory。修复方法是：在第 2 步中，Bob 必须加入自己的身份：{Na, Nb, B}_PKa。

Lowe 对 NSPK 协议的修复方案简单却意义深远：第 2 步中 Bob 的响应必须包含 Bob 的身份 B，使其变为 {Na, Nb, B}_PKa。现在，Alice 收到响应后，会检查其中包含的身份 B 是否与她原本要联系的一方匹配。Mallory 无法替换自己的响应——Mallory 需要 Alice 的私钥，才能构造出能通过 Alice 检查的有效 {Na, Nb, M}_PKa。这个教训被概括为 Needham-Abadi 原则：身份认证消息必须明确绑定发送者的身份，不能仅依赖上下文来识别发送者。

Lowe 发现 NSPK 漏洞时得到了 FDR（失败-发散精化）模型检查器的帮助。该工具会穷举探索所有可能的协议执行，包括对手的干预。这促成了形式化协议分析工具的发展：Proverif 基于应用 π 演算，可以在无限会话中证明或否定身份认证性和保密性。Tamarin Prover 使用多重集重写，并支持 TLS 1.3 和 Signal 等复杂协议。AVISPA 和 Scyther 是其他工具。现代协议设计（TLS 1.3、Signal、Noise）在部署前都会经过形式化验证——这正是 NS/Lowe 事件留下的直接影响。

NS 攻击明确了不同身份认证目标之间的区别。实体认证：证明某一方当前处于活动状态并参与协议（新鲜性很重要）。数据来源认证：证明特定消息由特定一方创建（但不一定意味着该方仍处于活动状态）。Lowe 的攻击破坏了实体认证——Alice 以为自己正在与 Bob 完成身份认证，但实际上她是在与 Mallory 完成身份认证，而 Mallory 只是将消息转发给 Bob。现代协议规范会精确描述目标：“Alice 已向 Bob 证明身份，并且是本次会话的发起方。”目标描述含糊会导致规范不明确，虽然能够通过非正式审查，却无法通过形式化分析。

另一类与 NS 相关的攻击是反射攻击：Mallory 将 Alice 发出的消息重新发送给 Alice。如果协议是对称的（双方使用相同的密钥和消息格式），Alice 可能会把自己的挑战当作 Bob 发来的有效响应。防御方法：使用不同的密钥方向（为每个方向分别使用加密密钥和解密密钥），或在消息中加入角色标识（例如加密方在消息中加入“我是发起方”）。TLS 等现代协议会在 HKDF 派生的密钥中加入特定角色的标签字符串（客户端使用 "c e traffic"，服务器使用 "s hs traffic"），以防止反射。

交错攻击会组合多个并发协议会话中的消息，从而伪造身份认证。如果 Alice 同时运行两个会话，Mallory 可能混合两个会话中的消息，构造出一个看似一致但实际无效的组合会话，并以 Mallory 的身份认证成功。防御方法是会话绑定——每条消息都必须以密码学方式绑定到其会话上下文（例如包含会话 ID，或为每个会话使用唯一密钥）。TLS 通过 Finished 消息防止交错，该消息是针对当前会话完整交互记录计算的 MAC。任何交错的消息都会改变交互记录，使 Finished 值失效。

Needham-Schroeder 协议直接影响了 Kerberos 的设计（使用时间戳防止重放，借鉴了 Denning-Sacco 修复方案）、TLS 的设计（Finished 交互记录 MAC 防止交错和反射）、Signal Protocol 的设计（通过棘轮状态绑定会话），以及 Noise 协议框架的设计（在握手模式中绑定身份）。NS 攻击表明，非正式的安全论证并不充分——每个协议都必须针对主动攻击者进行分析，因为主动攻击者控制网络，并且能够重放、重新排序和修改消息。这种攻击者模型（Dolev-Yao）如今已成为形式化协议验证中的标准模型。

Needham-Schroeder 对称协议（1978 年）引入了基于 TTP 的会话密钥分发。Denning-Sacco 攻击（1981 年）发现了重放漏洞，后来通过 Kerberos 中的时间戳修复。Lowe 在 1995 年通过模型检查发现 NSPK 公钥协议遭受 MITM 攻击，后来通过在消息中加入发送者身份修复。这些攻击确立了形式化验证（Proverif、Tamarin）对协议设计的重要性。关键经验包括：消息必须绑定发送者身份；会话必须彼此隔离；通过按方向派生密钥可以防止反射攻击；通过交互记录 MAC 可以防止交错攻击。