土法炼钢兴趣小组的博客 · 2026-07-21T00:00:00Z

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

📝

内容提要

用 Cremers ESORICS 2011 的 IKEv2 形式化结论、RFC 9370 混合密钥交换与 Gazdag 等对 PQ 扩展的 Tamarin 分析，对照 WireGuard 的无协商立场，收束何时仍应选择 IPsec。