VPN 协议规范能证明什么、不能证明什么

协议文档是各实现之间的契约，认真阅读它会告诉你两个合规对端将交换什么、设计者打算保证哪些性质。但它不会告诉你所连接服务器上运行的是哪个二进制文件、该服务器如何配置，也不会告诉你之后你的账户记录会怎样。这是三类不同的证据，把规范当成三者兼备，正是一个协议名开始做它做不到的事的方式。把三者分开，才是整个练习。

这份文档是论证的起点，而不是结论。

文档究竟规定了什么

对 WireGuard 而言，协议说明定义了 Noise IK 握手、一组固定的原语、报文布局，以及随后承载数据包的传输分帧。对 IKEv2 而言，可比的文档是 RFC 7296，它规定了交换、载荷与提案协商。两种情况的范围都很精确：报文、状态机，以及安全目标得以成立的那些假设。

可选模式让阅读更复杂。对某一种握手成立的性质，未必适用于采用不同认证安排或回退配置的部署。

保证到此为止

形式化分析回答的是关于模型的问题。WireGuard 的验证工作使用 Tamarin 证明器中的符号模型，它能表明该设计在其假设下抵御某些攻击；但它不能表明已交付的用户态实现没有内存安全缺陷。模型与机器之间的这道缝隙，正是真实事故所在。把证明当成实现证书来读，是范畴错误。

前向保密说明了同一条边界。该性质取决于密钥是否按协议意图被销毁，而这属于实现及其环境的性质，而非报文格式的性质。规定了擦除的设计，无法在会把内存换页到磁盘的平台上强制执行。

分层依赖进一步扩大了缝隙：TLS 隧道背后的 TLS 库、用户态隧道所用的内核接口，以及随机数生成器，都位于协议文本之外。

顺着字节追到构建里

从文档走向制品：先识别版本，再与真正在承载流量的东西对比。一个号称支持某协议的产品，可能加上了规范从未描述的开通、遥测与管理组件。

openvpn --version | head -3
wg --version
dpkg -l | grep -E 'openvpn|wireguard|libssl'
ss -lunp | grep -E '1194|51820'
sha256sum ./wireguard-tools_1.0.20210914_amd64.deb

可复现构建与公开校验和，使得把源码树与分发的二进制文件对应起来成为可能。没有这层对应，公开源码只能证明检查可行，而不能证明正在运行的文件与之相符。

配置也属于同一步。加密套件、允许的对端与路由设置都是部署选择，而配置草率的合规构建仍然只能得到脆弱的隧道。

把运营实践单独看待

账户记录、支付数据与支持提交是运营方的决定，任何协议文本都无法约束。审计报告在声明范围内覆盖指定组件，隐私政策描述意图与实践；二者不能互相替代，也都不是密码学陈述。

准确的结论是累积式的：规范解释设计，构建与配置解释隧道，而运营方有据可查的实践解释隧道永远看不到的一切。说明你验证了其中哪一项，这个说法就仍然成立。