2.3 把安全目标写成可证明的命题

2.3 把安全目标写成可证明的命题

本节摘要："我们很安全"之所以无法讨论，是因为它不是一个命题。本节给出安全命题的三要素模板——敌手前提、系统假设、不可行陈述——并把"聊天是安全的"这句空话分别改写成机密性、认证性、前向保密三种命题，展示同一句话在不同命题下结论可以完全不同。读完你能把任何安全声明升格为可检验、可反驳、可交给第 5 章机器验证的形式表述。

命题化的意义：让安全声明可以被反驳

科学哲学里有个朴素的判据：不能被反驳的陈述没有信息量。"系统是安全的"无法被反驳——任何事故都能被解释成"那是实现问题，不是协议问题"；也正因此它毫无内容。命题化的全部意义就在于给安全声明装上可反驳的靶子：写明敌手是什么、假设有什么、断言什么不可行，三者齐了，找一个反例才有明确的标准，找到一个反例才有明确的教训。

这个习惯也是贯穿全册的分析主线。第 3 章的名案复盘，每一起都可以概括成"某命题被证伪"：Needham-Schroeder 是认证命题被证伪，WEP 是机密性命题被证伪，心脏出血是实现假设被证伪。读案例时若能先写出"它当初声称的命题长什么样"，再看攻击怎么击中命题的哪个要素，复盘就不再是听故事，而是做解剖。

三要素模板

一个合格的安全命题由三部分构成，缺一不可：

【安全命题三要素模板】
1. 敌手前提   : 敌手具备哪些能力（引用 2.1 节四项能力）、控制哪些节点
2. 系统假设   : 哪些组件被信任、哪些困难问题被假设不可解、随机数质量如何
3. 不可行陈述 : 在前提与假设下, 敌手无法让哪个具体事件发生

示例（机密性命题）:
  在"敌手截获全部网络流量且未获取任何端点私钥"的前提下,
  假设所用加密原语满足语义安全且随机数不可预测,
  敌手无法获知消息内容的任何非平凡信息（除长度与时间外的内容）。

注意: 若删去"未获取任何端点私钥", 命题立即为假 —— 设备被解锁后
本地缓存可读, 内容自然可知。命题的精确性全部体现在前提的措辞上。
​

三个要素里，工程文档最常缺的是第一个。缺了敌手前提的安全声明等于没说——对手是谁都没约定，谈何守住。第二个常被隐含（"当然假设加密是安全的"），但隐含假设恰恰是事故源：6.2 节会看到，历史上不止一次是"假设的困难问题被算力进步打穿"而不是协议逻辑出错。第三个是命题的"牙齿"，措辞必须落到具体事件上（"无法伪造第三条消息的签名"），不能是"无法破坏安全"。

同一句话的三种命题

现在把"聊天是安全的"拆开。它至少可以对应三个不同的命题，敌手前提各不相同，含义天差地别。

机密性命题：敌手截获全部流量、不掌握端点密钥，无法读出消息内容。它承诺的是传输路径上的偷听无效，不承诺设备安全、不承诺服务器不存备份（除非配合端到端设计）。

认证性命题：敌手可注入任意伪造消息，无法让接收方把某条消息误认成指定联系人所发。它承诺的是来源不可冒充，但注意——它不承诺"对方说这话时是自愿的"（被胁迫的发送是合法发送），也不承诺服务器转发的消息没被篡改（那需要端到端完整性）。

前向保密命题：敌手在某一时刻拿到了长期私钥（比如设备被强制解锁），此前的历史会话仍然读不出来。它承诺的是"过去的内容不因今天的钥匙丢失而泄露"——这是三个命题里对设计要求最高的，因为协议必须保证历史会话密钥在用完即毁、且不与长期密钥发生可逆的数学联系。4.2 节的 Signal 双棘轮正是为这个命题而生。

三个命题对照着看，"聊天是安全的"这句话的空洞就现形了：一个只满足机密性命题的系统，在敌手拿到今日私钥时历史全泄（无前向保密），在敌手仿冒联系人发消息时用户毫无防备（无认证性）。没有命题分解的安全声明，等于把三种完全不同的承诺打包成一句无法兑现的口号。

命题的粒度：会话、消息与字段

命题还有粒度维度，初学者常一刀切到"整个系统"。更精确的写法是逐层下降：会话级（本次连接的会话密钥只有两端知道）、消息级（此条消息在未被确认前可被发送方撤回）、字段级（消息头中的路由字段对中间节点可见、正文不可见——这就是 TLS 与端到端加密的分界线所在）。粒度越细，命题越能直接对照协议消息逐条验证，也越容易在第 5 章翻译成机器查询。

粒度层面有个工程上极有用的推论：不同字段可以承担不同命题。一封端到端加密的邮件，正文对服务器保密，但收件人地址必须对服务器可见（否则无法路由）——这在设计上完全正当，前提是命题里写清楚"收件人地址不在机密性承诺范围内"。事故往往不在"哪个字段保密"的决定，而在决定从未被显式写下，用户以为全保密、产品以为全公开，两边的预期都没被命题校准。

💡 检验命题是否写合格的一个土办法：把命题念给同事听，让他扮演敌手，问他"按这个说法，我拿到什么就能赢"。如果他答不出来，说明前提或陈述有含糊；如果他答"拿到今日私钥就能读历史"，那你们要谈的其实是前向保密命题——讨论立刻聚焦。

措辞样例：坏命题与好命题的对照

模板要用在改稿上才见效。下面是一组需求文档里的原句与按三要素改写后的对照，改写前后能差出一张评审桌的讨论质量。

原句:  "聊天消息采用端到端加密, 保证用户隐私安全。"
毛病:  无敌手前提, 无命题边界, "隐私"一词覆盖了内容、元数据、
       联系人关系三个完全不同的承诺。

改写:  "在敌手可截获全部网络流量、但不掌控任何用户设备的前提下,
       消息正文对服务器与链路窃听者保持机密；
       联系人关系图与在线状态不在本承诺范围内（见元数据附录）；
       本承诺不覆盖设备被解锁后的本地存储。"
​

对照里藏着三个实务要点。第一，"不在承诺范围内"的句子和承诺句同样重要——它就是 2.2 节说的运营层残余风险的法律边界，写出来才有人守。第二，改写后的命题每半句都能对着协议消息指认兑现机制："正文对窃听者机密"指着端到端密钥协商，"服务器不可读"指着密钥只在端点派生——命题与机制能互相指认，评审才有抓手。第三，附录意识：把元数据、备份、找回流程各自写成独立小命题，比挤在一句大话里诚实得多，也英勇得多——敢于写"我们不承诺什么"的文档，可信度反而最高。

一个相关的高频追问：命题写得这么细，需求文档岂不要膨胀成一本书？实践经验恰恰相反——命题化省纸。含糊的安全声明需要用大量"兜底话术"对冲（"原则上""一般情况下""在正常使用中"），每一句兜底都是一处没人负责的灰区；命题化的文档把承诺与不承诺各写一遍，灰区显形后要么收编、要么删除，篇幅反而更短。真正膨胀的往往不是命题本身，而是命题背后的兑现机制索引——每个命题指向哪条消息的哪个机制，这类索引表让后续每一轮评审都从"重新讨论安全性"变成"核对兑现情况"，讨论成本一次比一次低。这份索引写完，你会发现它就是 5.2 节机器验证查询的人类可读版。

本节要点回顾

• 可反驳才有信息量：安全声明必须命题化——敌手前提、系统假设、不可行陈述，三要素缺一不可。
• 最常缺的是敌手前提：不约定对手的承诺没有兑现标准。
• 一句话三种命题：机密性管传输路径、认证性管来源不可冒充、前向保密管历史不随今日失钥而泄露，三者互不包含。
• 命题有粒度：会话级、消息级、字段级逐层细化；不同字段承担不同命题是正当设计，但必须显式写下。
• 命题是后续一切的地基：第 3 章用它解剖名案，第 5 章把它翻译成机器可验证的查询。

第 2 章到此立好了沙盘：敌手有了画像，系统有了清单，目标有了命题。下一章请出三位"已故"的当事人——三起经典失守案例，看敌手是怎么在真实历史里把一个个看似严谨的命题逐字证伪的。