5.1 BAN 逻辑手推一页纸

5.1 BAN 逻辑手推一页纸

本节摘要：1989 年的 BAN 逻辑第一次把"谁相信什么"变成可以按规则推演的对象，开创了协议形式化分析的整个领域。本节给出四条核心规则，把 NS 对称版本完整推一遍纸面推理，然后正面拆解它最大的软肋——理想化步骤的主观性。读完你能对一个小协议独立完成信念推理，并知道这类结论该怎么降级使用。

为什么信念可以被推理

协议分析的困难在于参与者的"信任状态"看不见摸不着：B 收到一条消息后，他相信了什么？BAN 逻辑的回答是把信任状态写成符号公式，再给一组保持真值的推理规则。它的基本对象有三类：公式 P 相信 X（记作 P 相信 X）、公式 P 收到过 X、公式 X 是新鲜的（刚生成而非重放）。三条公理式的出发点：持有加密密钥并收到密文则相信密文出自加密者、看到自己刚生成的临时值出现在消息里则相信消息是新近构造的、可信第三方说过的话可以被采信。

这套思路的革命性不在规则本身，而在它把"协议是否达成认证"从直觉问题变成了推导问题：从初始信念出发，逐条消息应用规则，看能否推出目标信念（"B 相信 A 相信共享密钥 K"）。推不出来，要么协议真有缝隙，要么规则不够用——两种情况都比"感觉还行"前进了一大步。

四条规则与一次完整手推

核心规则四条，每条一行就能写完：

【BAN 核心规则 · 手推卡片】
R1 消息含义:   P 相信 K 属于 P 和 Q, 且 P 收到用 K 加密的 X
              → P 相信 Q 曾说过 X
R2 临时值校验: P 相信 X 是新鲜的, 且 P 相信 Q 曾说过 X
              → P 相信 Q 现在仍相信 X
R3 仲裁规则:   P 相信 Q 对 X 有管辖权, 且 P 相信 Q 现在相信 X
              → P 相信 X
R4 收到规则:   P 收到 {X} 用 P 的密钥加密, 且 P 持有解密钥
              → P 收到 X（逐层拆包）
​

拿 NS 对称版本推一遍（协议：A 想与 B 建立会话，可信服务器 S 居中分发会话密钥 Kab 与 A 的新鲜临时值 Na）。初始信念：A 相信自己与 S 的长期密钥、B 相信自己与 S 的长期密钥、A 相信自己的临时值新鲜。推演如下：

【NS 对称版 · BAN 推演实录】
步骤 1  A 收到 S 发来的、用 A 与 S 的长期密钥加密的 {Kab, A 的临时值, ...}
        由 R4 拆包, 由 R1（A 相信长期钥, 密文必出自 S）
        → A 相信 S 说过: Kab 可用, 且与自己的临时值绑定
步骤 2  A 的临时值是自己刚生成的 → A 相信它新鲜
        由 R2 → A 相信 S 现在仍相信 Kab 有效     ← 新鲜性把"曾说过"升级为"现在说"
步骤 3  A 把 {用 Kab 加密的自己的身份与临时值} 转给 B
        B 收到, 由 R4 拆包 —— 但 B 初始并不相信 Kab！
        B 此时只知道: "某个持有 Kab 的人发来了这条消息"
步骤 4  B 收到 S 发来的 {Kab, A 的身份, ...}（用 B 与 S 的长期密钥加密）
        由 R1 → B 相信 S 说过 Kab 属于 A 与 B     ← B 的信任由此建立
步骤 5  目标信念: B 相信 A 现在仍相信 Kab
        由步骤 3 的密文 + B 相信 Kab + A 的临时值新鲜（由转发的密文传递）
        由 R1、R2 → B 相信 A 现在仍相信 Kab       ← 认证目标达成
​

推演的价值在步骤 3 的卡顿处最明显：B 在收到服务器消息之前，对那条转发的密文"知道它被某密钥加密过"却不知道该信谁——这个卡顿精确对应了协议里消息顺序的真实依赖。推理过程就是在把协议文本翻译成信任流。

手推练习：一个推不通的变体

规则只有配上反例才真正上手。看一个对 NS 对称版本做的"省事"改写：设计者觉得服务器转发两条消息太啰嗦，合并成一条——服务器把会话密钥与身份信息装进同一张票据，发给 A，由 A 转交给 B：

【变体协议 · 一步合并版】
消息1  S -> A : {用 A 与 S 的长期钥加密: Kab, B 的身份}
消息2  A -> B : {用 Kab 加密: A 的身份, A 的新鲜临时值 Na}

B 的目标: 确认 A 在线且 Kab 可用
B 初始知道: 什么都不知道 —— 它没和 S 建立过任何信任, 也没持有 Kab
（推演时先假定 Kab 已到达 B 手上, 看后续信念能否建立）
​

按四条规则推 B 的信念，推到第二步就卡死：B 收到消息 2，能拆开（假设 Kab 已 Somehow 到手），但 R1 要求"B 相信 Kab 属于 A 和 B"才能推出"A 说过这段话"——变体里 B 的这条初始信念从未被任何消息建立。纸面推不通，暴露的正是协议的真缺陷：B 缺一条来自可信第三方的密钥确认消息，没有它，任何知道 Kab 的人（包括曾经的合法使用者）发的消息，B 都无从分辨新旧与真伪——重放与冒充在这里畅通无阻。原版 NS 多出来的那条"服务器单独发给 B"的消息，恰恰就是在给 B 建立这条初始信念。

这个练习示范了纸面推演的正确打开方式：它不是验尸工具，是设计过程中的快速试错——每加一条消息前，先问问它给谁的哪条信念供了货；一条不给任何信念供货的消息，要么是冗余，要么说明你在用它传递的信息从未被任何人验证过。

理想化：最大的软肋，也是最重要的教训

BAN 推演有个前提动作叫理想化：把协议消息翻译成逻辑公式，比如把"消息里含名字 A"翻译成"S 声明 Kab 可用于 A 与 B 的会话"。问题来了——翻译的尺度没有标准。同样的消息文本，翻译得宽，漏洞被翻译没了；翻译得严，正常协议也推不通。NS 公钥版本在 BAN 框架下当年曾被推为"安全"，几年后 Lowe 找出了漏洞——理想化步骤把攻击者需要的"会话拼接自由"在翻译时抹掉了。这是形式化方法史上最著名的一次"模型通过、现实失败"。

教训值得单独成段：形式化方法验证的是"你写下的模型"，不是"你心里的协议"。工具与逻辑只对喂给它们的形式负责；模型与真实协议文本之间每一次翻译，都是一次可能引入偏差的人为判断。这并非否定 BAN——它的正确用法是快筛：纸面推不通的协议一定有问题；纸面推得通的协议，还需要状态探索工具与计算层面的检验（5.2、6.2 节）。三层检验各自 narrowing（缩小）不确定性的范围，没有一层可以单独盖章。

💡 一个实用的降级使用守则：BAN 类推理的结论表述应当是"在理想化 X 之下，信念 Y 可导出"，而不是"协议 Y 安全"。把理想化写进结论，等于把模型假设挂在结论上——这是从 3.1 节到现在反复出现的同一条纪律，只是换到了逻辑层面。

后继体系正是冲着这个软肋去的。GNY 在规则里补上了"未加密消息也能携带可识别信息"的推理能力，并区分"消息里的项是自己生成还是收到"；SVO 把理想化步骤换成了一套有语义依据的翻译规则；ATKR 等后续变体继续收窄翻译的主观空间。演进的总方向值得注意：每修补一次主观性，规则集就膨胀一圈，手推成本就上涨一截——这正是后来重心转向自动化工具的内在原因。人不该把脑力花在"按规则机械推演"上，那是机器的活；人该花脑力的地方是审读模型与解读反例，第 5 章后面两节就在讲这个分工。

本节要点回顾

• 信念可推理：把"谁相信什么"写成公式，用四条规则（消息含义、临时值校验、仲裁、收到拆包）从初始信念推目标信念。
• 新鲜性是升级器：临时值校验把"对方曾说过"升级为"对方现在仍相信"，认证目标依赖这一跳。
• 推演卡顿即依赖点：推理走不通的地方精确对应协议的消息顺序依赖，纸面推演因此有真实的诊断价值。
• 理想化是 BAN 的阿喀琉斯之踵：翻译尺度无标准，NS 公钥版"逻辑通过、现实失败"是永久性教材。
• 结论必须降级使用：推通了只说明模型内自洽，后续还要状态探索与计算层面的检验。

下一节进入当代主力工具：把协议写成 ProVerif 模型，让机器穷尽所有会话拼接——5.1 节纸面推不完的空间，机器几分钟能扫完。