【IPSec】深度探讨：形式化证明、密码敏捷性与后量子

前七篇把架构、握手、密钥、ESP、xfrm、strongSwan 与运维钉在可核对来源上。本文转入仍有文献与标准记录的争论：IKEv2 被自动验证工具说出了什么、算法协商的代价、后量子混合 KE 改了哪些状态机，以及相对 WireGuard 深度篇 如何选型。

一、谱系：从架构到「可证明」

RFC 4301 架构（SPD/SAD）
  → IKEv2 RFC 4306 / 5996 / 7296
    → 符号模型分析（Cremers, ESORICS 2011, Scyther）
    → PQ 扩展与 Tamarin（Gazdag et al., 2021；IKE_INTERMEDIATE 等）
    → 工程框架 RFC 9370（Multiple Key Exchanges in IKEv2）

Canetti–Krawczyk（CRYPTO 2002）等更早工作分析过 IKE 签名模式的密码学游戏；Cremers 2011 则用协议验证工具在更广的子协议交互与对手模型下扫 IKEv1/IKEv2。二者层次不同：前者偏密码学归约直觉，后者偏状态机与认证性质的自动检验。

二、争论一：Cremers 2011 发现了什么

Cremers, Key Exchange in IPsec revisited: Formal Analysis of IKEv1 and IKEv2（ESORICS 2011）：

• 会话密钥保密性：在所建模型下，未发现针对 IKE 所建会话密钥保密的重大缺口（摘要表述：no significant weaknesses on the secrecy of the session keys）。
• 认证性质：报告了若干此前未强调的认证弱点；在部分场景下，强相互认证不能想当然成立，并与反射等对手能力相关——尤其当预共享密钥等用法使角色对称时，需要按规范与部署仔细约束。

工程读法（与论文结论分开）：

• 不要把「通过了 Scyther 模型」理解成「任意 soft 配置都安全」。
• 部署上避免含糊的 ID/角色对称 PSK 拓扑；证书部署核对 ID 与证书绑定。
• 形式化结果依赖模型假设（完美密码学、对提议选择的抽象等）；扩展（EAP、MOBIKE、厂商私有 Notify）不在同一证明范围内。

这与 WireGuard 侧 Dowling–Paterson 的摩擦不同：那里是计算模型下 confirmation 与模块化证明的张力；这里是符号模型下认证性质的边界。两边都不是「协议已炸」，而是「宣传口径常大于可证口径」。

三、争论二：密码敏捷性

IPsec/IKEv2 默认拥抱协商：SA 载荷里一长串 proposal，响应方选一。好处是互通与算法迁移不必改协议号；坏处是：

• 配置面出现「弱套件仍在列表」→ 降级风险。
• 实现必须正确处理 NO_PROPOSAL_CHOSEN、Cookie、重试，状态机更长。
• 审计时「实际选定了什么」要靠日志与 list-sas，不能看配置文件里的愿望清单。

WireGuard（NDSS 2017）故意拒绝 cipher suite negotiation，用版本化与消息类型演进代替运行时套件讨价还价（见 WireGuard 深度篇）。

开放张力：监管与多厂商互联常强制走 IPsec 的协商世界；绿色地带单栈可以用 WireGuard 把敏捷性推到发行流程。

四、争论三：后量子与 RFC 9370

经典 IKEv2 的 DH/ECDH 面对比量子 retrospectively 解密威胁。工程回应不是「明天删掉 IKE」，而是 混合密钥交换：经典份额与 PQ KEM 份额一同混入密钥派生。

• RFC 9370（Multiple Key Exchanges in IKEv2）提供在 IKEv2 中组合多次密钥交换的通用框架。
• Gazdag et al.（2021） 对 IKEv2 握手在量子设定下建 Tamarin 模型，并以 IKE_INTERMEDIATE 等扩展展示状态机变更如何被纳入自动证明；模型聚焦核心状态机，实现细节（分片等）作黑盒。

相对 WireGuard 可选 PSK「偏执层」（NDSS §V-B）：IPsec 路线更接近 标准化混合 KE + 可协商算法；报文更大、往返/中间交换可能增加，运维要为 MTU 与中间盒再付成本。

五、选型收束

在本系列与 WireGuard 系列都读完的前提下：

VPN 工程对比 给场景表；本系列补的是：选 IPsec 时你买下的是 SPD/SAD/IKE 三张表与协商面，选 WireGuard 时你拒绝的也正是它们。

六、开放问题（留给后续，非本系列缺口）

• 生产强Swan/Libreswan 对 RFC 9370 的互操作矩阵随版本变化，需按发行说明核对。
• 高并发 Child SA rekey 与 xfrm 插入在多核上的尾延迟，缺本站统一口径实测。
• ZTNA 控制面与 IPsec/WG 数据面的拼接，见零信任系列边界，本文不展开产品清单。

参考资料

核心论文

• Cremers, C. Key Exchange in IPsec revisited: Formal Analysis of IKEv1 and IKEv2. ESORICS 2011.
• Canetti, R. & Krawczyk, H. Security Analysis of IKE’s Signature-Based Key-Exchange Protocol. CRYPTO 2002.
• Gazdag, S.-L., et al. A formal analysis of IKEv2’s post-quantum extension. 2021.

规范

• RFC 7296；RFC 9370。

对照

• Donenfeld, J. A. WireGuard. NDSS 2017.
• WireGuard 深度探讨
• VPN 技术工程对比