5.3 攻击迹解读与协议修补

5.3 攻击迹解读与协议修补

本节摘要：验证器输出攻击迹只是工作的开始：反例可能是真缺陷，也可能是模型失误的假阳性，区分两者需要一套系统的读法。本节给攻击迹的逐段解读清单——会话拼接、重放、类型缺陷、建模疏漏四类信号——以及修补后的回归验证流程。读完你能把机器的案卷翻译成工程决定，并把修补过的协议重新送上被告席。

攻击迹到底是什么

一条攻击迹是验证器找到的完整反例执行序列：哪些会话在何时启动、每条消息携带什么、敌手在哪一步注入了什么、最终哪个事件在哪些条件下发生从而违反了查询。它本质上是机器写好的一份案卷——证据链完整到每一步都可人工重演。要建立的第一直觉是：攻击迹不等于现实攻击。它是符号世界里的反例：证明"在模型的假设与抽象下，查询可被违反"。把反例变成现实攻击，需要回答三个问题——模型省略的细节会不会恰好挡住这条路径？攻击需要的会话组合在现实中能构造吗？违反的命题在安全声明里真的被承诺过吗？三问之后，攻击迹才能定性。

反例的另一面同样常见：假阳性。模型写错一个字段、把一个该保密的值声明成公开、抽象时合并了两条本不同的消息——验证器都会勤勤恳恳地找出反例，只是反例攻击的是你的模型而非你的协议。业内做建模验证的经验比例大致是：前几轮输出的反例多数是模型问题，模型迭代稳定之后，剩下的反例才值得当真。所以拿到第一条攻击迹的正确反应不是改协议，而是先审模型。

四类信号的读法

逐段读攻击迹时，以下四类信号对应四种最常见的情形，处理动作各不相同。

信号一：会话拼接。 攻击迹里出现两个会话，敌手把甲会话的消息转发进乙会话——这是真缺陷的标准信号（3.1 节的攻击迹就是教科书样本）。判断要点：检查被拼接的消息里是否缺少"把内容与会话上下文绑定"的字段（对象身份、会话标识、消息角色标签）。若是，修补方向是显式绑定；若字段其实存在，就轮到信号四——检查模型是否漏译了这个字段。

信号二：重放。 攻击迹里同一条旧消息被原样投递两次并都被接受。判断要点：协议是否对每条关键消息声明了新鲜性材料（临时值、序号、时间戳且验证端真的校验）。修补方向是把新鲜性材料纳入被验证的密文与完整性保护之内——只把序号放在明文头部而不纳入校验，等于把门牌号贴在防盗门外面。

信号三：类型缺陷。 攻击迹利用了"同一段比特在协议一处被当作随机数、另一处被当作密钥"之类的多义性。符号模型里这类攻击真实存在（历史上著名的类型缺陷攻击曾把签名对象换位利用），修补方向是给关键数据加类型标签并纳入完整性保护，让每个字段"自称是什么"也被绑定。

信号四：建模疏漏。 反例的路径在协议文本里根本走不通——多译了一个敌手不该有的能力（比如让他伪造了某个该被签名保护的消息），或漏译了一个协议里存在的检查。这是假阳性的典型形态，处理动作是改模型、重跑验证，而不是动协议。判断口诀：拿攻击迹的每一步回协议文本对表，走不通的那步就是模型与现实的分界线。

【攻击迹解读清单 · 会前卡片】
第 1 步  标出攻击迹里有几个会话、各由谁发起
第 2 步  找敌手的注入点: 哪些消息是转发, 哪些是构造
第 3 步  对表协议文本: 每一步在真实协议里是否可行
第 4 步  分类信号: 拼接 / 重放 / 类型缺陷 / 模型疏漏
第 5 步  真缺陷 → 写缺陷报告(触发条件+影响半径+修补建议)
第 6 步  假阳性 → 改模型, 重跑, 记录模型修订史
​

修补与回归：协议的迭代纪律

修补要遵守与写代码相同的回归纪律，且多一条。**多的一条：先修命题再修消息。**拿到真缺陷后，先用 2.3 节模板把被违反的命题重写成"应当成立的版本"（例如把"消息来源可验"升格为"会话归属可验"），再从命题反推需要哪些字段与检查——直接在消息上打补丁而不重写命题，是修补流于表面的主因：补丁可能只堵住了攻击迹里的这一条路径，而命题层面的漏洞还留着别的走法。

回归验证的完整闭环是：修补后的协议重新建模（重点确认新字段进入了签名或完整性保护的覆盖范围）、原查询重跑必须通过、邻接查询一并重跑（修补引入新字段后，可能让原本不相关的性质产生新的交互）、以及把"修补前会失败"的旧攻击迹保留为回归用例——机器验证版的"复现脚本"。最后把整套材料（模型、查询、攻击迹、修订记录）随协议文档一起归档：形式化验证的价值一半在结论，一半在可复现的论证材料本身——它让后来者的每一次质疑都有明确的靶子，这正是 3.1 节"修复便宜、检出昂贵"这条不对称在流程上的解法。

💡 一个衡量团队形式化成熟度的土指标：出事故或换协议版本时，能否在一天内用既有模型重跑全部查询。能，说明模型是活的资产；不能，说明当年那次验证只是一次性的仪式。

一次定性的完整记录：从攻击迹到工程决定

把前面所有动作串成一次真实节奏的工作记录，你会在自己的项目里遇到同样的分岔点。

【定性工作记录 · 示例】
第 1 轮  查询: 会话归属认证
  输出: 攻击迹 —— 敌手把会话甲的第 2 条消息转进会话乙
  对表: 协议文本第 2 步确实不含对象身份 → 走得通 → 真缺陷嫌疑
第 2 轮  审模型: 敌手能力是否多给了? 无。事件埋点是否漏? 无。
  结论: 缺陷成立, 写缺陷报告
  报告: 触发条件(两会话并行+转发), 影响半径(响应方误认发起方),
        修补建议(第 2 条消息密文内加入对象身份字段)
第 3 轮  修补后重建模: 新字段进入加密体 → 重跑原查询, 通过
  邻接查询: "发起方误认响应方"方向的对称查询 → 通过
  新增查询: 新字段被篡改时握手必须失败 → 通过
第 4 轮  归档: 模型 + 查询清单 + 攻击迹(修补前) + 修订记录
  修补前的攻击迹保留为回归用例 —— 机器版的复现脚本
​

这份记录里有三处值得圈点的职业习惯。第一，第 2 轮"审模型"放在"改协议"之前——顺序反了，就是把假阳性当缺陷修，白费一轮开发还污染协议设计。第二，第 3 轮除了原查询还跑了方向对称的邻接查询：修补引入新字段后，原缺陷消失但镜像缺陷可能仍在，只验单方向是修补验证最常见的漏项。第三，第 4 轮把修补前的攻击迹归档而不是删除——它是"这个缺陷真实存在过"的证据，也是未来重构时防退化的免费测试用例。

类型缺陷值得多给两句，因为它是四类信号里最反直觉的。符号世界里数据没有"种类"，一段比特既可以被当作名字拼进消息、也可以被当作密钥用——真实实现里有类型系统挡着，符号模型里没有。历史上确有协议在这条缝上失守：攻击迹显示敌手把本应作为"随机挑战"的字段拿来当解密密钥用，只因两处对同一段数据的解释不同。修补的方向也因此明确：给关键字段加类型标签，并把标签纳入完整性保护范围，让"这段数据自称是什么"本身成为被验证的内容。顺带一提，这也是为什么建模时规范里每个字段的"角色"要如实写——模型里偷懒合并字段，等于亲手拆掉类型防线让工具去撞。

本节要点回顾

• 攻击迹是模型内反例：定性前先过三问——模型省略是否挡路、会话组合现实可构造吗、命题真的被承诺过吗。
• 第一条反例先审模型：建模迭代早期的反例多数是假阳性，攻击的是模型而非协议。
• 四类信号四种动作：拼接补显式绑定、重放补新鲜性纳入保护、类型缺陷补标签绑定、疏漏改模型不动协议。
• 先修命题再修消息：从重写的安全命题反推字段与检查，避免只堵单一攻击路径的表面补丁。
• 回归闭环五件事：重建模、原查询重跑、邻接查询重跑、旧攻击迹作回归用例、全套材料归档。

第 5 章到此把机器请上了被告席对面。下一章面向未来：格基密码把命题的前提换掉之后，协议怎么迁移、混合过渡怎么设计、部署层怎么裁剪——推演室的最后一课是把今天的结论安全地带进明天。