2.1 Dolev-Yao 全能敌手

2.1 Dolev-Yao 全能敌手

本节摘要：1983 年 Dolev 与 Yao 给出的符号敌手模型，至今仍是协议分析的第一语言。本节把敌手的四项网络能力逐条写实，讲清"敌手就是网络本身"这条设定的推演威力，以及它把密码学运算当黑盒带来的天生盲区。读完你能复述模型的两条让步与两条限制，并知道哪些事故该归它管、哪些不在它的辖区。

敌手为什么要是"全能"的

分析协议时第一个诱惑是把敌手想弱一点："正常人哪有本事截获骨干网流量？"这个诱惑必须抵抗，理由有二。其一，协议是基础设施，会被部署在你不知道的网络位置上——咖啡馆的无线、被入侵的路由、恶意的企业代理、被要求留后门的设备；设计时按最坏位置假设，部署时才处处可用。其二，模型弱了，证明出的结论就脆：你能证明"敌手只能偷听时协议安全"，但现实里没人能保证敌手只偷听。

Dolev-Yao 的做法干脆利落：干脆假设敌手就是网络本身。所有消息都经过敌手之手——合法角色发出的每条消息，敌手先收到；他想丢就丢、想改就改、想伪造就伪造、想按原样再发就再发。合法角色只能看到敌手决定转交的内容。这个设定初见令人绝望：连信道都不可信，还谈什么安全？恰恰相反，这是模型最迷人的地方——在这样的世界里证出来的安全性，是分文不少的硬保证。今天任何一份 TLS、Signal、Signal 派生协议的安全论证，默认都在这个沙盘里进行。

四项能力逐条写实

截获：读取所有经过的密文与明文元数据（谁发给谁、什么时候、多长）。注意元数据——长度和时间常常泄露内容之外的敏感信息，这是初学者最容易忽略的让步项。

篡改：修改任何在途消息的任意比特。修改后的消息可能解密失败、签名失效——那没关系，敌手不求成功，只求试。

注入：以任何身份发出新消息，包括冒充合法角色的地址。网络层不提供"这句话真是 A 说的"的服务，那正是密码协议要自己挣来的。

重放：把过去合法的旧消息原样再发一遍。旧消息带着合法的密码学保护，"看起来完全正确"正是它危险的原因。协议必须自带新鲜性机制（临时值、时间戳、会话编号）来拒绝旧话——这解释了为什么第 1 章 NS 协议里每个角色都要生成随机临时值。

图 2-2 Dolev-Yao 敌手能力标注示意：一条消息的完整旅程

两条限制：模型不是万能的

全能是有边界的，两条限制划定了符号模型的辖区。限制一：密码学运算被视为黑盒。敌手解不出没被泄露的密文、伪造不出没被泄露的签名——他只能对已有的消息做"拼接与剪切"：把消息里的字段拆出来、重新组合进新消息。这条简化是符号模型的威力来源（分析变成代数操作，机器可以穷尽），也是它的风险来源：黑盒假设把实现层的一切都豁免了。填充提示攻击这类"通过解密报错的不同反应逐字节抠出明文"的事故，符号模型完全看不见——因为黑盒不允许"解密一半"。同理，弱随机数、时序泄露、侧信道，都不在辖区。第 3 章心脏出血案例会再次敲打这一点。

限制二：不掌控端点。敌手拿不到角色的机器、不入侵角色的内存、不胁迫角色本人。设备中木马后聊天记录被读走，不是协议的失败——协议的承诺从来只到端点边界为止。这条限制在产品宣传里常被偷偷抹掉（"端到端加密，绝对安全"），你要能一眼识别：加密承诺的是传输路径，不是两端设备。

计算模型：另一种让步方式

符号模型之外还有一条平行路线：计算模型不把密码学当黑盒，而是承认敌手是概率多项式时间的图灵机——可以运行任何计算，只要时间不超过安全参数的多项式。于是结论从"绝对不可能"变成"成功概率小到可忽略"（比如低于 2 的负 128 次方）。这个模型能表达"密文长度泄露了信息量"这类精细命题，是可证明安全（6.2 节）的地基。

两个模型的分工可以这样记：符号模型管协议逻辑（消息怎么组合、顺序依赖、重放路径），计算模型管原语强度（这个加密方案在计算上是否语义安全）。协议事故大多出在逻辑层——这正是符号模型成为协议分析第一语言的原因；但符号模型验过的协议，仍可能栽在原语误用和实现上。5.2 节的自动化工具会看到：ProVerif、Tamarin 都是符号模型的机械化，而可证明安全的机械化（如 CryptoVerif）走的是计算路线，两者至今没有完全合流。

常见疑问：模型这么悲观，工程上还怎么干

有读者到这里会想：假设敌手无所不在，那系统还怎么设计、预算怎么排？这里要理清"设计沙盘"与"部署评估"的分工。设计协议时用全能沙盘，是因为协议要在不知道自己会被部署到哪的前提下立保证——这是它的通用性代价，也是通用性收益。而部署评估时（2.2 节的四象限），你完全可以根据自己系统的实际暴露面收窄敌手画像：一个纯内网服务和一个公网服务面对的现实敌手确实不同。两者的关系是：协议保证由强沙盘给出上界承诺，部署决策由现实画像决定下限投入——用强沙盘的协议不浪费，因为它是"怎么部署都不碎"的那一层。

另一个高频疑问：Dolev-Yao 模型会不会把敌手想得太简单——真实攻击者还要用零日漏洞、钓鱼、社会工程？不会太简单，只是分工不同。模型刻意不建模的那些手段（攻端点、攻人、攻实现），对应的是安全工程的其他楼层：设备安全、人员流程、实现审计（3.3 节）。协议层的责任是把"只要端点没丢、密码学没破，逻辑就守得住"做到极致；把人员钓鱼也算进协议模型，等于让一个学科替所有学科背锅。真正的风险评估要给每一层配各自的模型与各自的清单。

一个记账练习：把真实攻击翻译回四项能力

模型要用才会长在手上。拿三个大家都听过的攻击场景做翻译练习。场景一，咖啡馆里有人用抓包工具收集你手机发出的所有数据包——这是截获，零门槛，人人可为。场景二，公开 Wi-Fi 里攻击者把你的 HTTP 请求页面里塞进自己的脚本——这是注入，混合着篡改。场景三，登录请求被原样录下来、五分钟后重发一遍绕过登录——纯粹的重放，注意攻击者始终没有解开任何密文，他只是把"看起来正确"的旧话再说一遍。

翻译的价值在于接下来那一步：对每个场景追问"协议的哪道防线让它失效"。场景一靠传输加密挡住内容（元数据仍在敌手手里——这条让步无法收回）；场景二靠信道完整性与站点身份认证挡住；场景三靠新鲜性机制挡住——时间戳、一次性序号、挑战应答。反过来，如果一次事故里三道防线都没生效，你就能用四项能力的语言精确描述事故：敌手以截获起手、以重放收尾，中间没有遇到新鲜性检查。这套语言在第 5 章会直接变成验证模型的词汇——ProVerif 查询里的敌手，就是今天这四项能力的形式化化身。

练习还有个进阶版：找出一条你所在系统的真实链路，把链路上每个"消息经过的环节"列出来（客户端、代理、网关、服务、队列、日志），然后按"敌手即网络"的设定逐环节标注四项能力的暴露程度。多数人做完会第一次意识到：自己系统的攻击面里，最大的那块不是密码学没选好，而是某个日志副本或调试通道悄悄把"合法消息"整批送到了敌手桌上——重放连原样截获都省了。

本节要点回顾

• 敌手即网络：所有消息经敌手之手，四项能力——截获、篡改、注入、重放——是协议设计的默认沙盘。
• 重放是最隐蔽的一项：旧消息带着完整合法保护，新鲜性机制（临时值、会话编号）是协议的必备器官。
• 元数据也是让步项：谁在何时给谁发了多长的消息，敌手全部可见，长度与时间会泄露内容之外的信息。
• 两条限制划出辖区：密码学黑盒（实现层盲区）与端点不掌控（设备安全另算），超出辖区的承诺都是宣传。
• 符号与计算模型的分工：符号管协议逻辑，计算管原语强度；符号模型验过不等于实现安全。

下一节把这份理论画像翻译成工程动作：拿到一个真实系统，怎么按四步产出一份能用的威胁推演清单，哪些条目最常被高估、哪些最常被低估。