【密码学百科】协议安全性分析：形式化验证与符号模型

密码协议是现代网络安全的基石。然而，即使协议中使用的每一个密码原语本身是安全的，协议作为一个整体仍然可能存在致命的逻辑漏洞。这些漏洞往往隐藏在消息交换的时序、参与者身份绑定、新鲜性保证等看似无关紧要的细节之中，仅凭人类直觉几乎无法完全排除。

正是这种”原语安全不等于协议安全”的深刻教训，催生了密码协议形式化分析这一领域。本文聚焦于形式化分析的核心方法论：首先通过经典案例说明形式化分析的必要性，然后系统讲解 Dolev-Yao 符号模型和 BAN 逻辑等理论基础，再深度对比 ProVerif、Tamarin 和 Spin 三大验证工具的建模范式与能力边界，最后以 TLS 1.2 三重握手漏洞为完整案例，展示形式化工具如何从建模、查询到攻击发现的全过程。

一、为什么需要形式化协议分析

先看一张图，把这一节的关键关系串起来。

flowchart LR
    A[协议模型] --> B[攻击者假设]
    B --> C[形式化工具]
    C --> D[发现攻击或证明]
    D --> E[修复设计]

密码协议分析之所以成为一个独立的研究领域，根本原因在于协议设计中的漏洞具有极强的隐蔽性。这一点最早通过 Needham-Schroeder 公钥协议的经典案例被充分揭示。

1978 年，Roger Needham 和 Michael Schroeder 提出了一个看似简单而优雅的公钥认证协议。该协议旨在让两个参与者 Alice 和 Bob 通过公钥加密实现双向认证。协议的消息流如下：

1. Alice → Bob：\(\{N_A, A\}_{K_B}\)（Alice 将自己的随机数 \(N_A\) 和身份 \(A\) 用 Bob 的公钥加密后发送）
2. Bob → Alice：\(\{N_A, N_B\}_{K_A}\)（Bob 解密后获得 \(N_A\)，生成自己的随机数 \(N_B\)，用 Alice 的公钥加密后返回）
3. Alice → Bob：\(\{N_B\}_{K_B}\)（Alice 解密后获得 \(N_B\)，用 Bob 的公钥加密后回传给 Bob）

直觉上，这个协议看起来是安全的：Alice 通过第二步中收到的 \(N_A\) 确认 Bob 收到了她的消息，Bob 通过第三步中收到的 \(N_B\) 确认 Alice 收到了他的消息。然而，这个协议在公开发表后的整整 17 年间，没有人发现其中的漏洞。直到 1995 年，Gavin Lowe 利用模型检测工具 FDR(Failures-Divergences Refinement)对该协议进行形式化分析时，才发现了一个中间人攻击。

攻击场景如下：假设攻击者 Mallory 拥有合法的公钥，当 Alice 试图与 Mallory 建立会话时：

1. Alice → Mallory：\(\{N_A, A\}_{K_M}\)
2. Mallory 解密获得 \(N_A\)，伪装成 Alice 向 Bob 发起会话：Mallory(伪装 Alice) → Bob：\(\{N_A, A\}_{K_B}\)
3. Bob → Alice(实际发给 Mallory)：\(\{N_A, N_B\}_{K_A}\)
4. Mallory 无法解密此消息，但可以将其转发给 Alice：Mallory → Alice：\(\{N_A, N_B\}_{K_A}\)
5. Alice 认为这是 Mallory 回复的第二步消息，于是回复：Alice → Mallory：\(\{N_B\}_{K_M}\)
6. Mallory 解密获得 \(N_B\)，完成与 Bob 的协议：Mallory(伪装 Alice) → Bob：\(\{N_B\}_{K_B}\)

攻击完成后，Bob 确信自己在与 Alice 通信，但实际上他的会话是 Mallory 操纵的。根本原因在于第二步消息 \(\{N_A, N_B\}_{K_A}\) 中没有绑定发送方的身份——Bob 没有在回复中表明自己的身份，导致 Alice 无法区分这条消息究竟来自 Bob 还是 Mallory。Lowe 提出的修复方案非常简单：将第二步改为 \(\{N_A, N_B, B\}_{K_A}\)，即在消息中加入 Bob 的身份标识。

这个案例深刻说明了三个关键问题。第一，协议中的安全漏洞可以极其隐蔽，即使是经验丰富的密码学家也可能无法通过直觉发现。第二，漏洞往往不在单个密码原语中，而在消息之间的逻辑关系中——此处的问题是身份绑定的缺失。第三，自动化的形式化分析工具能够系统地搜索攻击空间，发现人类难以察觉的漏洞。

历史上还有大量类似的教训。Denning 和 Sacco 在 1981 年发现了 Needham-Schroeder 对称密钥协议中的重放攻击。Abadi 和 Needham 在 1996 年的经典论文”Prudent Engineering Practice for Cryptographic Protocols”中总结了协议设计中反复出现的错误模式。然而，准则终究只是经验总结，无法替代严格的形式化证明——2014 年发现的 TLS 1.2 三重握手攻击再次证明，即使在经过二十多年实践检验的协议中，形式化分析仍能揭示根本性的设计缺陷（本文第五节将对此进行完整解剖）。

二、Dolev-Yao 符号模型

Dolev-Yao 模型是密码协议形式化分析的基础框架，由 Danny Dolev 和 Andrew Yao 在 1983 年提出。该模型定义了一种符号化的攻击者能力模型，使得协议的安全性分析可以在一个精确定义的数学框架中进行。

Dolev-Yao 模型的核心思想是将密码操作抽象为代数运算，将消息视为形式化项(Formal Term)，并通过一组推导规则描述攻击者的能力。模型包含以下关键假设和组成部分。

消息代数。所有消息被表示为由基本元素通过密码操作构造而成的项。基本元素包括参与者的名字、随机数(Nonce)、密钥等原子项。密码操作包括对称加密 \(\mathsf{senc}(m, k)\)、非对称加密 \(\mathsf{aenc}(m, pk)\)、数字签名 \(\mathsf{sign}(m, sk)\)、哈希 \(\mathsf{h}(m)\)、配对 \(\langle m_1, m_2 \rangle\) 等。这些操作的逆操作也被形式化定义，例如 \(\mathsf{adec}(\mathsf{aenc}(m, pk), sk) = m\) 当且仅当 \(sk\) 是 \(pk\) 对应的私钥。

完美密码假设。这是 Dolev-Yao 模型最核心也是最具争议的假设：密文是不透明的黑盒——攻击者在不知道正确密钥的情况下，无法从密文中获取任何关于明文的信息，也无法伪造密文。加密完全隐藏明文，签名不可伪造，哈希函数是单向且无碰撞的。这一假设使得分析可以完全聚焦于协议的逻辑结构，而不必考虑具体密码算法的实现细节。

网络攻击者模型。Dolev-Yao 攻击者完全控制网络通信信道，可以窃听、拦截、注入、重放和伪装。但攻击者不能直接读取诚实参与者的内部状态，也不能破解密码原语。

攻击者的推导能力。给定攻击者当前的知识集合，攻击者可以通过以下规则推导新消息：(1) 构造和拆分配对；(2) 使用已知密钥进行加密和解密；(3) 使用私钥进行签名；(4) 对已知消息计算哈希。形式化地，这些规则构成一个封闭的推导系统：

\[\frac{m_1, m_2}{\langle m_1, m_2 \rangle} \quad \frac{\langle m_1, m_2 \rangle}{m_1} \quad \frac{\langle m_1, m_2 \rangle}{m_2} \quad \frac{m, k}{\mathsf{senc}(m, k)} \quad \frac{\mathsf{senc}(m, k), k}{m}\]

在这个框架下，协议安全性分析的问题可以精确表述为：给定协议规范和安全性目标(如保密性、认证性)，是否存在一个 Dolev-Yao 攻击者能够违反安全性目标的攻击策略？如果不存在这样的攻击策略，则协议在 Dolev-Yao 模型下是安全的。

Dolev-Yao 模型的优势在于它将复杂的密码学问题转化为组合学或逻辑推理问题，使自动化验证成为可能。其局限性在于完美密码假设无法捕捉密码原语的实现缺陷(如加密方案的延展性、哈希碰撞)。尽管如此，Dolev-Yao 模型在过去四十年中一直是协议分析的主流框架，大量重要的协议漏洞都是在此模型下发现的。

三、BAN 逻辑

BAN 逻辑(Burrows-Abadi-Needham Logic)是最早的协议形式化分析方法之一，由 Michael Burrows、Martin Abadi 和 Roger Needham 在 1989 年提出。它是一种信念逻辑，通过推理协议参与者在执行协议过程中形成的信念来分析协议的认证性质。

BAN 逻辑的核心构造是一组关于信念的谓词：\(P \mid\equiv X\)（P 相信 X）、\(P \triangleleft X\)（P 收到了 X）、\(P \mid\sim X\)（P 曾发送 X）、\(P \Rightarrow X\)（P 对 X 有管辖权）、\(\#(X)\)（X 是新鲜的）。其推理规则包括：

消息含义规则：如果 \(P\) 相信 \(K\) 是与 \(Q\) 的共享密钥，并且 \(P\) 收到了用 \(K\) 加密的消息 \(X\)，则 \(P\) 可以推断 \(Q\) 曾经发送过 \(X\)：

\[\frac{P \mid\equiv P \stackrel{K}{\longleftrightarrow} Q, \quad P \triangleleft \{X\}_K}{P \mid\equiv Q \mid\sim X}\]

新鲜性验证规则：如果 \(P\) 相信 \(X\) 是新鲜的，并且相信 \(Q\) 曾经发送过 \(X\)，则 \(P\) 可以推断 \(Q\) 当前相信 \(X\)：

\[\frac{P \mid\equiv \#(X), \quad P \mid\equiv Q \mid\sim X}{P \mid\equiv Q \mid\equiv X}\]

管辖权规则：如果 \(P\) 相信 \(Q\) 对 \(X\) 有管辖权且 \(Q\) 当前相信 \(X\)，则 \(P\) 也相信 \(X\)：

\[\frac{P \mid\equiv Q \Rightarrow X, \quad P \mid\equiv Q \mid\equiv X}{P \mid\equiv X}\]

使用 BAN 逻辑分析协议的步骤为：(1) 理想化——将协议消息转化为 BAN 逻辑的形式化表示；(2) 列出初始假设——各参与者的初始信念集合；(3) 应用推理规则——逐步推导新的信念；(4) 检验目标——验证推导结果是否满足安全性目标。

BAN 逻辑首次将形式化方法引入协议分析领域，但也存在严重局限性。理想化步骤是非形式化的，不同分析者可能得出不同结论。更关键的是，BAN 逻辑只能推理参与者的信念，无法直接推理攻击者的行为——它能告诉你”如果协议正确执行，参与者会形成什么信念”，但无法告诉你”是否存在攻击者策略使得协议不能正确执行”。其健全性本身也受到质疑：BAN 逻辑可能对存在已知攻击的协议给出”安全”结论。正是这些局限性，推动了密码学界转向基于 Dolev-Yao 模型的自动化验证工具。

四、自动化验证工具：ProVerif、Tamarin 与 Spin

当前密码协议形式化分析的实践主要依赖三类工具，它们代表了三种不同的方法论传统。本节深入介绍各工具的建模范式，然后进行系统化对比。

ProVerif：基于 Horn 子句的全自动验证

ProVerif 由 Bruno Blanchet 于 2001 年开始开发，基于应用 pi 演算(Applied Pi-Calculus)建模协议。协议的每个参与者被建模为一个进程，进程之间通过信道交换消息。密码操作通过函数符号和等式理论描述，例如对称解密 \(\mathsf{sdec}(\mathsf{senc}(m, k), k) = m\) 被表示为一条重写规则。

ProVerif 最重要的技术特点是支持无界数量的并发会话。它通过将协议翻译为 Horn 子句并利用分辨算法进行推理，能够在有限时间内分析任意多个并发会话。代价是 ProVerif 可能产生误报——即协议实际安全时报告可能存在攻击——但不会漏报：如果 ProVerif 说”安全”，那就确实安全。

以下是一个用 ProVerif 建模的共享密钥双向认证协议：

(* 声明信道和类型 *)
free c: channel.                       (* 公开信道，攻击者可监听 *)
type key.
type nonce.

(* 密码原语：对称加密/解密 *)
fun senc(bitstring, key): bitstring.
reduc forall m: bitstring, k: key;
      sdec(senc(m, k), k) = m.

(* 共享密钥 *)
free Kab: key [private].

(* 安全性目标：认证事件 *)
event beginA(nonce).
event endA(nonce).
event beginB(nonce).
event endB(nonce).

(* 认证查询：Bob 完成认证 => Alice 曾发起 *)
query na: nonce; event(endB(na)) ==> event(beginA(na)).
query nb: nonce; event(endA(nb)) ==> event(beginB(nb)).

(* Alice 进程 *)
let processA =
    new na: nonce;                     (* 生成新鲜随机数 *)
    event beginA(na);
    out(c, senc((na, A), Kab));        (* 发送 {Na, A}_Kab *)
    in(c, msg2: bitstring);            (* 接收第二条消息 *)
    let (=na, nb: nonce) = sdec(msg2, Kab) in
    event beginB(nb);                  (* 确认 Bob 参与 *)
    out(c, senc(nb, Kab));             (* 发送 {Nb}_Kab *)
    event endA(nb).

(* Bob 进程 *)
let processB =
    in(c, msg1: bitstring);            (* 接收第一条消息 *)
    let (na: nonce, =A) = sdec(msg1, Kab) in
    event beginA(na);                  (* 确认 Alice 发起 *)
    new nb: nonce;
    event beginB(nb);
    out(c, senc((na, nb), Kab));       (* 发送 {Na, Nb}_Kab *)
    in(c, msg3: bitstring);
    let (=nb) = sdec(msg3, Kab) in
    event endB(na).                    (* Bob 完成认证 *)

(* 主进程：无界并发会话 *)
process
    (!processA | !processB)

其中 ! 表示进程的无界复制，event 用于跟踪协议执行进度，query 指定安全性目标——此处要求认证一致性(Agreement)。ProVerif 运行时会自动探索所有可能的攻击者行为，找到攻击则输出攻击过程，否则证明安全。

Tamarin Prover：基于多集重写的精确验证

Tamarin 由苏黎世联邦理工学院的 Cremers、Basin 等人开发，于 2012 年首次发布。它使用多集重写系统建模协议：系统状态由事实的多集表示，每一步操作是一条重写规则：

\[[\text{前置事实}] \xrightarrow{\text{动作事实}} [\text{后置事实}]\]

例如，Alice 发送第一条消息的规则：

\[[\mathsf{Fr}(na), \mathsf{!Ltk}(A, \mathit{skA})] \xrightarrow{\mathsf{Send}(A, B, na)} [\mathsf{St\_A\_1}(A, B, na), \mathsf{Out}(\mathsf{aenc}(\langle na, A \rangle, \mathit{pkB}))]\]

其中 \(\mathsf{Fr}(na)\) 表示新鲜值，\(\mathsf{!Ltk}\) 前缀 ! 表示持久事实（不被消耗），\(\mathsf{Out}(\cdot)\) 表示向网络发送消息。

Tamarin 的核心优势在于三点。第一，精确性：它既不误报也不漏报，当报告”安全”时结论是精确的，发现攻击时输出完整的攻击轨迹。第二，等式理论：内置了 Diffie-Hellman 指数运算（包括交换律 \(g^{ab} = g^{ba}\)）、双线性配对、异或等代数性质，能够分析依赖于这些性质的协议。第三，交互式与自动化结合：对于复杂协议，用户可以通过引理和证明提示引导搜索方向，类似于交互式定理证明器中的策略。代价是验证可能不终止——对于某些协议，搜索过程可能陷入无限循环。

Spin：基于模型检测的有限状态验证

Spin 由贝尔实验室的 Gerard Holzmann 于 1991 年开发，是通用的模型检测器，使用 Promela(Process Meta-Language)语言建模有限状态并发系统。Spin 通过穷举搜索所有可达状态来验证线性时序逻辑(LTL)性质。

在协议分析中使用 Spin 时，协议参与者和攻击者都被建模为 Promela 进程，消息通过信道传递。以下是 Spin 建模 Needham-Schroeder 协议的核心片段：

/* Needham-Schroeder 协议 Spin 模型片段 */
mtype = { msg1, msg2, msg3, Alice, Bob, Mallory };

typedef Cipher { mtype data1; mtype data2; mtype key };

chan network = [0] of { mtype, Cipher };

active proctype alice() {
    Cipher m;
    /* 发送 {Na, Alice} 加密给 Bob */
    network ! msg1, { Na, Alice, Bob };
    /* 接收回复 */
    network ? msg2, m;
    /* 验证 Na 匹配 */
    assert(m.data1 == Na);
    /* 发送 {Nb} 给 Bob */
    network ! msg3, { m.data2, 0, Bob };
}

Spin 的核心特点是：(1) 对有限状态模型保证终止并给出精确结果；(2) 支持 LTL 性质验证和死锁检测；(3) 不原生支持密码等式理论——用户需要手动编码代数性质为状态，容易出错且可能导致状态爆炸。最关键的限制是 Spin 只能验证有界会话数——用户需要预先指定并发会话的数量上限，如果漏洞只在更多会话并发时出现就会遗漏。

三大工具深度对比

以下从多个关键维度对三款工具进行系统化对比：

以下从表达力、实际发现的漏洞和生态成熟度三个角度进一步深化对比：

工具选择决策框架。 (1) 快速原型验证：使用 ProVerif，其全自动特性和较低的学习曲线使其成为”第一遍检查”的首选。(2) 有状态协议（如 Signal 双棘轮、密钥更新协议）：使用 Tamarin，ProVerif 难以精确建模全局可变状态。(3) 涉及 DH 等代数性质的协议：优先使用 Tamarin，其内建的 DH 等式理论经过充分验证。(4) 有限规模的实现验证（如固定参与者数、固定轮数）：Spin 是合适的选择，尤其当分析者的背景更偏向软件工程时。(5) 分层策略：实践中常常先用 ProVerif 快速排除明显漏洞（数小时），再用 Tamarin 精细建模复杂交互（数天），必要时使用 CryptoVerif 在计算模型下获得归约证明（数周）。

五、案例解剖：用形式化工具发现 TLS 1.2 三重握手漏洞

Needham-Schroeder 攻击发现于 1995 年，读者可能认为此类设计级漏洞已属历史。事实恰恰相反——2014 年 Bhargavan、Delignat-Lavaud、Fournet、Pironti 和 Strub 发现的 TLS 1.2 三重握手攻击证明，即使在经过二十多年实践检验的工业级协议中，形式化分析仍能揭示根本性的设计缺陷。本节以这一漏洞为案例，完整展示从攻击原理到形式化建模、从工具发现到修复验证的全过程。

攻击原理

三重握手攻击的核心目标是在客户端认证场景下，让中间人 Mallory 使得服务器 Bob 接受一个本应属于 Alice 的客户端证书认证。攻击分三个阶段：

阶段 1：Mallory 分别与 Alice 和 Bob 建立独立的 TLS 会话

  Alice <--> Mallory <--> Bob
  会话 S1               会话 S2
  主密钥 MS1            主密钥 MS2

阶段 2：Mallory 操纵 RSA 密钥交换，使两个会话共享相同主密钥

  关键漏洞：TLS 1.2 的主密钥派生公式为
  MS = PRF(PMS, "master secret", ClientRandom || ServerRandom)
  其中不包含服务器身份（证书）！Mallory 可以：
  - 作为 S1 的"服务器"，选择特定参数
  - 作为 S2 的"客户端"，转发 Alice 的参数
  -> 结果：MS1 = MS2 = MS（相同的主密钥）

阶段 3：Mallory 触发重协商（renegotiation），利用共享密钥

  Alice 在 S1 上进行客户端认证（发送证书和签名）
  Mallory 将 Alice 的认证消息通过 S2 转发给 Bob
  由于 MS1 = MS2，Finished 消息的 MAC 验证通过
  -> 结果：Bob 认为 Mallory 的连接已通过 Alice 的客户端证书认证

攻击的根本原因是 TLS 1.2 的主密钥派生和 Finished 消息中没有绑定完整的会话上下文——特别是没有绑定服务器的身份和使用的证书。

用 ProVerif 建模漏洞

研究者使用 ProVerif 建模了 TLS 1.2 的重协商流程。以下是捕捉漏洞本质的简化模型，聚焦于密钥派生不绑定服务器身份这一核心缺陷：

(* TLS 1.2 三重握手漏洞——简化 ProVerif 模型 *)
free c: channel.
type skey.
type pkey.
type nonce.

(* 非对称加密 *)
fun pk(skey): pkey.
fun aenc(bitstring, pkey): bitstring.
reduc forall m: bitstring, sk: skey;
    adec(aenc(m, pk(sk)), sk) = m.

(* 签名 *)
fun sign(bitstring, skey): bitstring.
reduc forall m: bitstring, sk: skey;
    checksign(sign(m, sk), pk(sk)) = m.

(* 漏洞根源：主密钥派生不绑定服务器身份 *)
(* MS = PRF(PMS, ClientRandom, ServerRandom)     *)
(* 注意参数中没有服务器公钥!                      *)
fun prf(bitstring, nonce, nonce): bitstring.

(* MAC 用于 Finished 消息 *)
fun mac(bitstring, bitstring): bitstring.

(* 安全性目标：注入一致性 *)
event ClientAuthTo(pkey, pkey).   (* 客户端认为自己向 pkS 认证 *)
event ServerAccept(pkey, pkey).   (* 服务器接受 pkC 的认证 *)

(* 核心查询：服务器接受客户端认证时，              *)
(* 客户端必须确实打算向该服务器认证                 *)
query pkC: pkey, pkS: pkey;
    event(ServerAccept(pkC, pkS))
    ==> event(ClientAuthTo(pkC, pkS)).

(* 客户端进程：向 targetS 发起握手 *)
let Client(skC: skey, targetS: pkey) =
    new cr: nonce;
    new pms: bitstring;
    out(c, (cr, aenc(pms, targetS)));      (* ClientHello + 加密 PMS *)
    in(c, sr: nonce);                       (* ServerHello *)
    let ms = prf(pms, cr, sr) in
    (* 重协商阶段：客户端认证 *)
    event ClientAuthTo(pk(skC), targetS);
    out(c, (sign((ms, pk(skC)), skC),       (* 客户端证书签名 *)
            mac(ms, (pk(skC), targetS)))).   (* Finished MAC *)

(* 服务器进程 *)
let Server(skS: skey) =
    in(c, (cr: nonce, epms: bitstring));
    let pms = adec(epms, skS) in
    new sr: nonce;
    out(c, sr);
    let ms = prf(pms, cr, sr) in
    (* 接收客户端认证 *)
    in(c, (client_sig: bitstring, client_mac: bitstring));
    let (=ms, pkC: pkey) = checksign(client_sig, pkC) in
    (* 验证 MAC——但 MAC 中的服务器身份未被检查! *)
    event ServerAccept(pkC, pk(skS)).

(* 主进程：诚实客户端与 Mallory 通信，诚实服务器独立运行 *)
process
    new skC: skey; new skS: skey; new skM: skey;
    out(c, pk(skC)); out(c, pk(skS)); out(c, pk(skM));
    ( !Client(skC, pk(skM))    (* Alice 想和 Mallory 通信 *)
    | !Server(skS) )           (* Bob 独立提供服务 *)

ProVerif 在分析此模型时，会自动发现以下攻击轨迹：

ProVerif 输出（简化）：
  RESULT event(ServerAccept(pkC,pkS)) ==> event(ClientAuthTo(pkC,pkS))
         is false.

  攻击轨迹重建：
  1. Client(skC) 向 pk(skM) 发起握手：out(c, (cr, aenc(pms, pk(skM))))
  2. 攻击者解密获得 pms，用 pk(skS) 重新加密：out(c, (cr, aenc(pms, pk(skS))))
  3. Server(skS) 接收并解密，返回 sr
  4. 攻击者将 sr 转发给 Client
  5. 两侧计算 ms = prf(pms, cr, sr)——由于 prf 不含服务器身份，ms 相同!
  6. Client 发出 ClientAuthTo(pk(skC), pk(skM)) 并生成签名和 MAC
  7. 攻击者将客户端认证消息转发给 Server
  8. Server 触发 ServerAccept(pk(skC), pk(skS))
  -> 违反查询：Client 认证目标是 pk(skM)，但 Server 认为客户端向自己认证

核心洞察：攻击之所以成立，是因为 prf(pms, cr, sr) 的计算不包含服务器身份。攻击者作为中间人，可以让两侧计算出相同的主密钥，然后跨会话转发客户端认证消息。

修复与验证

TLS 1.3 通过三个设计变更修复了这一漏洞。在 ProVerif 模型中，修复体现为将密钥派生函数绑定服务器身份：

(* TLS 1.3 修复：主密钥派生绑定完整握手转录 *)
(* 新的 prf 包含服务器公钥作为参数              *)
fun prf_fixed(bitstring, nonce, nonce, pkey): bitstring.

let Client_Fixed(skC: skey, targetS: pkey) =
    new cr: nonce;
    new pms: bitstring;
    out(c, (cr, aenc(pms, targetS)));
    in(c, sr: nonce);
    (* 修复：密钥派生绑定服务器身份 *)
    let ms = prf_fixed(pms, cr, sr, targetS) in
    event ClientAuthTo(pk(skC), targetS);
    out(c, (sign((ms, pk(skC)), skC),
            mac(ms, (pk(skC), targetS)))).

对修复后的模型运行 ProVerif：

RESULT event(ServerAccept(pkC,pkS)) ==> event(ClientAuthTo(pkC,pkS))
       is true.

攻击不再可行：即使攻击者转发相同的 pms、cr、sr，由于 prf_fixed 包含服务器公钥，两侧计算出的主密钥不同，Finished MAC 验证将失败。

TLS 1.3 的实际修复手段更为彻底：(1) 主密钥派生绑定了完整的握手转录哈希(transcript hash)，包含服务器证书和所有握手消息；(2) 完全移除了重协商机制；(3) Finished 消息使用绑定完整会话上下文的 HMAC。这些修复正是在形式化分析指导下做出的设计决策。

这一案例深刻说明了形式化分析的价值：一个在实践中运行了二十多年、被安全专家反复审查过的协议，其密钥绑定缺陷仍然逃过了人类的直觉审查，却无法逃过 ProVerif 的系统化搜索。

六、验证实践：TLS 1.3 与 Signal 协议

TLS 1.3 和 Signal 协议是形式化验证介入协议设计最成功的两个实例。前者展示了形式化方法如何在标准化过程中主动指导设计决策，后者展示了如何精确界定复杂有状态协议的安全性边界。

TLS 1.3：形式化验证驱动的标准化

TLS 1.3 于 2018 年作为 RFC 8446 发布，其设计过程是密码协议形式化验证最成功的实践案例——形式化方法不是在协议发布后被动查找漏洞，而是在设计过程中主动指导决策。

Cremers 等人使用 Tamarin Prover 对 TLS 1.3 的多个草案版本进行了系统分析，覆盖了完整握手、预共享密钥握手、0-RTT 恢复以及客户端认证等模式。分析验证的安全性目标包括密钥保密性、前向安全性、服务器认证、客户端认证、密钥唯一性以及降级保护。

Bhargavan 等人的 miTLS 项目则更进一步——他们不仅验证协议的抽象模型，还验证了用 F* 语言编写的具体 TLS 实现。miTLS 使用 ProVerif 和 CryptoVerif 分别在符号模型和计算模型下验证了 TLS 1.3 密钥交换子协议，其安全性归约到标准密码学假设（如 Diffie-Hellman 假设和 PRF 安全性）。

形式化验证在 TLS 1.3 设计过程中的关键贡献包括：(1) 发现 0-RTT 模式固有的重放攻击风险，促使标准文档明确标注安全性限制；(2) 发现早期草案中降级保护机制的不足，导致 ServerHello 中降级标志位(Downgrade Sentinel)的引入；(3) 验证密钥调度(Key Schedule)设计的正确性，确保不同阶段的密钥具有适当独立性。IETF 标准化过程中的多个设计决策直接受到了形式化分析结果的影响。

Signal 协议：有状态协议的安全性边界

Signal 协议是当今最广泛部署的端到端加密协议，被 WhatsApp、Facebook Messenger、Google Messages 等平台采用。其核心由 X3DH 密钥协商协议和 Double Ratchet 消息加密协议组成，提供前向安全性和后妥协安全性等高级安全特性。

Cohn-Gordon 等人使用 Tamarin 对 X3DH 进行了详细分析，精确界定了在不同密钥泄露场景下的安全性保证。分析表明，X3DH 在身份密钥和临时密钥的组合泄露下仍能保持部分安全性，但如果 Bob 的已签名预密钥私钥被泄露，安全性会受到影响。

对 Double Ratchet 协议的分析尤为深入。Cohn-Gordon、Cremers 等人使用 Tamarin 建模了完整的双棘轮机制，包括乱序消息处理和消息丢失。分析揭示了一个微妙的安全性边界：在对称棘轮阶段（同一方向连续发送多条消息时），后妥协安全性不成立——因为没有新的 DH 交换来注入新的随机性。只有当通信方向切换并触发 DH 棘轮更新后，后妥协安全性才生效。

值得注意的是，Kobeissi、Bhargavan 和 Blanchet 使用 ProVerif 对 Signal 进行了独立分析，从不同方法论角度验证了类似的安全性结论。两个独立团队使用不同工具得到一致结论，极大地增强了社区对 Signal 安全性的信心。这也展示了 ProVerif 和 Tamarin 作为互补工具的价值——ProVerif 快速给出全自动结论，Tamarin 则能更精确地刻画有状态协议的细粒度安全性边界。

七、从符号模型到计算安全性

Dolev-Yao 符号模型通过完美密码假设简化了分析，但真实世界中的密码原语并不完美：加密方案可能泄露明文长度信息，哈希函数可能存在碰撞，数字签名可能具有延展性。计算模型(Computational Model)直接在概率多项式时间框架下分析协议，消息是比特串而非抽象项，安全性通过计算不可区分性定义，提供更强的安全性保证。

连接两个模型的桥梁是计算可靠性(Computational Soundness)。Abadi 和 Rogaway 在 2002 年证明：在特定条件下（密码原语满足 IND-CCA2 等标准安全定义），符号模型下的安全性可以”提升”到计算模型。这使得分析者可以在易于自动化的符号模型中完成证明，再通过该定理获得计算安全性保障。

CryptoVerif（Bruno Blanchet 开发）直接在计算模型下生成安全性证明，使用基于游戏的证明技术，输出包含具体安全性损失的归约证明。EasyCrypt（Gilles Barthe 等人开发）则提供交互式证明框架，支持概率关系 Hoare 逻辑(pRHL)。在实践中，研究者通常采用分层策略：先用 ProVerif/Tamarin 排除逻辑缺陷，再用 CryptoVerif/EasyCrypt 获得计算安全性证明。TLS 1.3 和 Signal 协议的验证都采用了这种分层方法。

八、挑战与展望

尽管形式化验证取得了显著成就，这一领域仍面临根本性挑战。

状态空间爆炸。现代协议包含多种模式、扩展和错误处理路径，完整建模和验证的工作量极其庞大。Tamarin 对 TLS 1.3 完整握手的验证需要数小时计算时间和大量用户引理。对于 5G 认证框架等更复杂的协议，全自动验证极为困难。

协议组合性。现实中的安全系统通常是多个协议的组合，单独验证每个协议并不能保证组合后仍然安全。通用可组合安全性(UC)框架提供了理论方案，但实践中将复杂协议建模为 UC 安全的形式仍极具挑战。

模型与实现的鸿沟。形式化验证通常针对抽象模型，从模型到实现之间可能引入缓冲区溢出、时序侧信道等新漏洞。Project Everest 代表了弥合这一鸿沟的最先进尝试——它构建了从 TLS 协议逻辑到底层密码原语汇编代码的全栈验证实现，已被集成到 Firefox 和 Linux 内核中。

后量子协议分析。后量子密码原语的代数性质与传统原语不同（如基于格的方案存在解密失败的可能性），如何扩展 Tamarin 和 ProVerif 的等式理论以准确建模这些新原语，是当前活跃的研究方向。

密码协议的形式化分析已经从学术研究走向工程实践。从 Needham-Schroeder 的漏洞发现到 TLS 1.3 的设计验证，从 BAN 逻辑的初步探索到 Tamarin 和 ProVerif 的成熟应用，这一领域在四十年间取得了瞩目进展。将形式化方法更深入地融入协议的设计、实现和部署流程——从”在论文中证明安全”转变为”让工具发现攻击”——是这一领域未来发展的核心方向。

密码学百科系列 · 第 53 篇

← 上一篇：公钥密码的可证明安全 | 系列目录 | 下一篇：密码学标准化 →