TLA+：给混合握手协议上一份逻辑保险

FIBEMATE 系列第6篇。前五篇：迁移动因、混合 HTTPS、CBOM 工具链、FPGA NTT 基准、预硅侧信道。这一篇补协议正确性：用 TLA+ 给 C-2 混合握手建状态机，TLC 模型检查 7 条安全性不变式，101,467 个状态零违反。文末词汇注释 6 条，不熟悉 TLA+ 的先跳到最后看一眼再回来。

一、900/900 通过，说明不了什么

上一篇讲混合握手的线上可观测性：应用层路径 C-2（SM2 + ML-KEM-768）在生产服务器上端到端 900/900 通过，p95 78.5ms。数字漂亮，只说明一件事——这条路径在测过的场景下跑通。

它说不明的是协议逻辑本身有没有角案。两个会话会不会派生出同一把密钥？客户端还没认证完，服务端能不能进 active？一次性预密钥会不会被消费两次？这三类是加密消息系统最致命的错误。端到端测试很难主动构造这类边角状态冲突，只能覆盖预设场景——你不知道要构造什么用例。

形式化方法在工程界名声两极：学术装饰，或大杀器。本文的用法两者都不是：两个 .tla 文件加两个 .cfg，TLC 两秒跑完，投入不大，买到的保证很具体。

二、建模：C-2 状态机

C-2 的密钥派生是一个双 PRF 组合器：key_i = HKDF-Extract-SHA256(sm2_ephem_i || mlkem_ss_i)——SM2 临时私钥和 ML-KEM 共享密钥两路熵，缺一路密钥就不成立。TLA+ 模型不碰这两个原语内部，只管组合后的逻辑。

模型里做抽象简化：DeriveKey(i) = i——这不是真实派生代码，是用会话索引编码「不同会话的派生密钥互不相同」这条安全假设；真实实现靠 HKDF 合并两路独立熵源，密钥唯一性由密码学保证，不靠编号。

状态机按真实协议画，2 个并行会话：

密钥状态显式建模：cKeyValue[i] = 0 表示未派生，= i 表示已派生。派生前的值是 0，active 后非零——「没派生密钥就进 active」在状态层面直接可见，K1 抓的就是它。

另一处抽象先记在这里：真实混合握手对 HKDF 的拼接顺序和域分离标签有严格要求，本模型不校验 HKDF 标签——这是模型未覆盖点，与第六节的边界声明一并成立。

三、7 条不变式与 TLC 结果

C2.cfg 挂 7 条不变式：

K3 是核心：密钥独立性的强形式，直接回答第一节的第一个问题。注意它是模型假设，不是 TLC 证出来的结论。 TLC 证明的是：在该假设成立的前提下，状态机不会出现会话密钥复用的逻辑漏洞。真实协议靠密码原语的随机输出——256 位独立采样，碰撞概率 2⁻²⁵⁶——把这条假设转成密码学安全论断。

TLC 结果（4 workers，2 核，2 秒）：

101,467 个状态全部遍历，26,115 个去重后逐一检查 7 条不变式，零违反。3.9E-11 是 TLC 内部状态指纹哈希的碰撞概率——风险在检查工具自身，不是协议安全数字，量级可忽略。本轮只覆盖安全性不变式，活性未验证——握手会不会永远卡住，TLC 这轮没查。

四、两个细节

细节一：操作符优先级。 \A x \in S: P /\ Q => R 在 TLA+ 里解析为 \A x \in S: ((P /\ Q) => R)（/\ 优先级高于 =>）。这次碰巧是想要的语义，但不赌——全部显式加括号。模型检查器的「通过」建立在解析正确上，解析歧义就是假阳性来源。

细节二：O7 定义了但没挂载。 写 OPK 规约时定义了 O7_KeyIdMonotonic（keyId 单调递增，上传不复用），cfg 里没写进 INVARIANT 列表——TLC 只检查 cfg 显式声明的不变式和属性，规约里定义而未挂载的只是文本，一行都不查。文件里躺着一条不变式 ≠ 它在生效。本轮 O1-O6 挂载生效，O7 未挂载，下一轮补。

五、OPK 模型：一次性预密钥不可双花

预密钥建模为三态：available → consumed → burned。每消费一次记入 consumeLog。规模取 MaxUsers = 3、MaxOPKPerUser = 5——这是模型检查的常规取舍：覆盖消费、复用、计数这类交错错误的最小规模；规模加大只让状态数变多，不产生新的交错类别，所以小规模就够抓逻辑 bug。

挂载 6 条不变式：

• O1：同一个 OPK 不出现在两条消费记录里（不可双花）
• O2：每条消费记录对应已上传的 OPK
• O3：可用计数与实际可用集合一致
• O4：consumed 不可再次消费
• O5：消费只从 available 集合发生
• O6：每用户消费总量不超过上传总量

O1 直接回答第一节的第三个问题。O7 定义未挂载，见第四节。TLC 检查通过。

敌手模型说明：规约取 Dolev-Yao 风格抽象——敌手可窃听、重放、注入报文，不攻破密码原语。敌手能力在规约内隐式定义，与第六节的「原语另证」边界一致。

这条模型和第 5 篇的重放防护是一对：重放防护挡网络层的重放包，O1-O6 挡协议层的状态机重复消费。两层各自有证据。

六、边界

• 活性未验证。 本轮只查安全性不变式，未编写、未验证任何 Liveness 属性。Lossy 网络下 ClientKeyFinish 丢失会让 Server 卡在 sentSK——真实协议由 TCP 重传解决，TLA+ 网络抽象层不建模。跑 TLC 传入 -deadlock，含义是关闭死锁状态自动检查；它与活性验证是两件事，本轮两者都未做。Liveness 不变式（<>(双方都进 active)）在审计日志里列为 P1。
• K3 依赖模型假设。 DeriveKey(i)=i 在模型内是假设，在真实协议里是密码学随机性。TLA+ 不为随机性背书。
• 密码学安全性不在范围内。 ML-KEM-768 的 IND-CCA2 属于 FIPS 203 和 EasyCrypt/CryptoVerif 的范畴，TLA+ 不覆盖。这是已知缺口里最重的一条。
• 规模 2 会话。 2 会话是本轮模型的检查规模，不是协议能力上限——真实协议没有这个限制。状态空间随会话数指数增长，结果不能直接外推到 N 会话。小规模模型的价值是提前捕获逻辑缺陷、错误状态跳转、资源双花这类逻辑 bug，不是穷尽生产会话场景。
• HKDF 标签未建模。 拼接顺序与域分离校验不在模型内，见第二节。

TLA+ 买到的保证一句话：如果密码原语安全，则协议逻辑安全。原语本身的安全，另证。

七、成本与适用场景

投入：两个 .tla 加两个 .cfg，TLC 单次 2 秒，一台 2 核机器。学习曲线按周计。

用在：协议状态机、密钥派生逻辑、一次性资源、权限状态转换——逻辑密集、角案致命的层面。不用在：密码原语本身、性能、真实网络行为。

八、结语

900/900 说「测过的路径跑通」，TLC 说「状态空间里没有反例」。两者不互相替代：测试覆盖不了构造不出的用例，模型检查覆盖不了模型没画进去的现实。两个证据放在一起，比单独任何一个都硬。

参考实践

• 规约与配置：fibemate 仓库 docs/tla/C2.tla、C2.cfg、OPK.tla、OPK.cfg
• 审计记录：docs/audit-log/formal-verification-L4_2026-07-14.md（含完整 TLC 输出）
• 工具：github.com/tlaplus/tlaplus（tla2tools.jar，java -cp tla2tools.jar tlc2.TLC C2 -workers 4 -deadlock -nowarning）

词汇注释

• TLA+：Leslie Lamport 的形式化规约语言，用数学描述并发系统的状态与动作。
• TLC：TLA+ 的模型检查器，穷举有限规模的状态空间，逐状态检查不变式。
• 不变式（invariant）：在所有可达状态上都必须为真的性质，违反即协议逻辑有洞。
• 模型检查（model checking）：给定规约和不变式，机器自动穷举验证，无需人工证明。
• IND-CCA2：选择密文攻击下的不可区分性，KEM/公钥加密的标准安全定义。
• 双 PRF 组合器：把两路密钥材料经 PRF（如 HKDF）合并，任一路安全则输出安全。