〇、这份证明要回答什么
只回答两个问题：
- 我们是怎么把你的 NAT 类型测出来的（证明过程）；
- 为什么同样给出四类结论，别的站点会把 NAT4 判成 NAT3、把 NAT3 判成 NAT4，而我们不会。
为了能「证」而不是「说」，先把「测」变成数学对象。下文每一步都可以对照代码复核，也可以被反例推翻——但推翻不了。
一、先定义：一个 NAT 到底由什么决定
把你电脑上的一个端口记作 s（内网端点），把互联网上某个服务器的地址记作 d（目的端点）。你的 NAT 对外只做两件事：
再加一个历史量 H：s 曾经主动发过包的那些目的地址。过滤规则只依赖 H。这两件事彼此独立——记住这句话，后面所有误判都源于把两者搞混。
四类 NAT 就是用这两个量写出来的：
| 类型 | 映射 M 的行为 | 过滤 F 的行为 | 现实含义 |
|---|---|---|---|
| NAT1 全锥形 | 与目的地址无关（EIM） | 恒放行，任何来源都能打进来 | 打洞最顺，PCDN 收益最高 |
| NAT2 受限锥形 | 与目的地址无关（EIM） | 只放行你主动连过的那个 IP，端口不限 | 对方 IP 固定时可打通 |
| NAT3 端口受限 | 与目的地址无关（EIM） | 只放行你主动连过的那个 IP 加 那个端口 | 端口一变就不通，打洞要靠预测 |
| NAT4 对称型 | 与目的地址有关（非 EIM），换目的地就换端口 | 通常伴随严格过滤（但不必然） | 端口不可预测，几乎无法打洞 |
记 EIM 为「映射与目的地址无关」，则四类可写成：NAT1 = EIM ∧ F 恒放行；NAT2 = EIM ∧ F 按 IP；NAT3 = EIM ∧ F 按 IP+端口；NAT4 = ¬EIM。
这四类互不重叠、也不留空隙（在「过滤只有这三种形态」的前提下），所以你真实的类型有且只有一个。
二、四个探针各自测到了什么
关键设计：我们用两条互相独立的浏览器连接，各占一个本地端口，也就是两个不同的 s。这一点是全篇的地基。
- 过滤探测连接（记 sf）：只告诉浏览器「主服务器 dp 在这」，浏览器只会向 dp 发包。
- 映射比对连接（记 sm）：同时告诉浏览器两个公网 IP，浏览器会用同一个本地端口向两者都发包。
| 探针 | 做法 | 观测量 | 能证明什么 |
|---|---|---|---|
| 测试 I | 向 dp 发 STUN 请求，读回自己的公网端口 | ω1 = M(sm, dp) | 存在映射，且拿到基准值 |
| 测试 II | 从另一个公网 IP 主动向 sf 的公网端口打一个请求 | ω2 ∈ {0,1} | 换 IP 能否打通（过滤是否端点无关） |
| 测试 IV | 从同一 IP 的另一个端口主动打你 | ω4 ∈ {0,1} | 换端口能否打通（区分 NAT2 / NAT3） |
| 测试 III | 让映射比对连接再向第二个 IP 发一次，看公网端口变没变 | ω3 = M(sm, da) | 映射是否随目的地址漂移（唯一能定 NAT4 的证据） |
为什么「我们主动打你」和「标准里说的让服务器换地址回包」是一回事：NAT 的放行判断只看（你的公网端口，对方源地址）这两个量，它不解析 STUN 报文，也不区分这一包是「应答」还是「新请求」。所以两种做法在 NAT 眼里完全等价。
为什么必须用两条连接：如果映射比对和换 IP 探测共用一个端口，那么一旦浏览器先向第二个 IP 发过包，你的 NAT 就已经给那个 IP 开了门，后面的「换 IP 主动探测」必然打通——NAT2、NAT3 会被一律误判成 NAT1。所以我们的过滤探测连接，从设计上就绝不告诉浏览器第二个 IP 的存在。测试的顺序也据此固定：先做 II / IV，最后才做 III，免得 III 提前替后面两个探针开门。
三、判定规则（一张表说清）
| 观测到的组合 | 判定 | 依据 |
|---|---|---|
| 映射可比，且两个目的地上端口不同（漂移） | NAT4 对称型 | ¬EIM 直接成立，压过其它一切观测 |
| 端口相同，换 IP 能打通 | NAT1 全锥形 | EIM + 过滤端点无关 |
| 端口相同，换 IP 不通、换端口通 | NAT2 受限锥形 | EIM + 过滤按 IP |
| 端口相同，两个方向都不通 | NAT3 端口受限 | EIM + 过滤按 IP+端口 |
| 映射没法比对 | 无法判定 | 信息不足，不给类型 |
最后一行是我们和大多数站点最大的区别，第五节会专门讲。注意第一行的优先级：即便测试 II 收到了回包，只要映射被证实在漂移，结论仍然是对称型——两种观测互相矛盾时，以映射漂移为准。
四、证明：三条定理
判成 NAT4，就一定是 NAT4。
等价说法：NAT1 / NAT2 / NAT3 永远不会被测成 NAT4。
要判 NAT4，必须「观测到两个目的地址上的公网端口不同」。这个观测只有在满足全部三个条件时才成立：
- 两个观测都来自映射比对连接 sm（同源）；
- 两个目的地确实不同（我们强制两个服务器 IP 不同）；
- sm 在这两个目的地上各自只出现过一个端口。
前两条保证两次观测是同一个 s 在两个不同 d 上的映射，第三条排除「你有多个网卡、多个本地端口」造成的身份混淆。于是我们有 M(sm, dp) ≠ M(sm, da) 这个事实。
如果 NAT 是锥形的（EIM），按定义它对任何目的地映射都相同，就会得到 M(sm, dp) = M(sm, da)，与上述事实矛盾。所以它不是锥形，只能是对称。
证毕
这条结论不依赖丢包率，不依赖超时设置，也不依赖浏览器行为。只要「漂移」是被看见的，方向就是确定的。
判成 NAT2 或 NAT3，就说明那两个目的地上确实没有漂移。
等价说法：NAT4 永远不会被测成 NAT3。
我们的判定规则里，走到 NAT2 / NAT3 之前有一道硬门槛：必须先拿到「端口相同」这个已验证的观测；如果端口没法比对，规则直接跳到「无法判定」，不会继续往下走。
于是「判成 NAT3」这件事本身携带了「已观测到 M(sm, dp) = M(sm, da)」这一事实。既然这两个目的地上端口没有变化，「映射随目的地址变」这个对称 NAT 的特征就不成立，对称 NAT 不能落在这个分支里。
证毕
我们的错只会偏保守，不会偏乐观。
等价说法：不会把打不了洞的网络说成能打洞。
全篇唯一带概率的观测是「没收到回包」。而「没收到回包」有两种可能：被过滤了，或者包丢了。所以它只能单向使用：
- 收到回包 ⟹ 一定放行（确定）；
- 没收到回包 ⟹ 可能放行、也可能不放行（不确定）。
也就是说，观测到的放行情况永远「不高于」真实情况。而三种锥形类型恰好由两个方向的放行情况唯一确定：（通，通）= 全锥形，（不通，通）= 受限锥形，（不通，不通）= 端口受限。观测只会把「通」看成「不通」，于是判定只会往更严格的方向偏，或者因为信息不足而退回「无法判定」。绝不会反过来。
证毕
五、别的站点为什么会把 NAT4 测成 NAT3（以及反过来）
下面六种是现实中常见的实现路线。每一种都能在公开的网页版 NAT 测试里见到，也都是可被数学反驳的。
| 做法 | 会得出什么 | 为什么错 |
|---|---|---|
| ① 只有一台服务器 只发一两次请求 |
端口稳定就说锥形，端口变了就说对称；NAT1/2/3 完全分不开 | 端口变化也可能只是你自己换了本地端口（浏览器新建连接），那与 NAT 行为无关。把「换了连接」当成「换了映射」，锥形就被判成 NAT4。而且它根本没测过滤。 |
| ② 照抄 RFC 3489 的原始流程图 |
先做「换 IP + 换端口」，一有回包就判全锥形 | 存在一类 NAT：映射确实随目的地址变，但过滤很宽松。按 RFC 顺序它会被判成全锥形。这是标准自身的漏洞，不是实现者粗心。我们把这个顺序改了过来：先看漂移，再看过滤。 |
| ③ 有换 IP / 换端口 但没有映射比对 |
把 NAT4 报成 NAT3 | 只有一台服务器或只有同一 IP 的两个端口，就没法比较「同一个端口在两个目的地上的映射」。而对称 NAT 的过滤几乎总是端口受限的，于是它在观测上与 NAT3 一模一样。这不是测得粗，是信息不足：NAT3 与 NAT4 在这组观测下数学上不可区分。正确做法只有一个——不给类型。 |
| ④ 做了映射比对 但两条连接混着比 |
任何锥形 NAT 都被判成 NAT4 | 两条连接就是两个本地端口，公网端口本来就不同。拿 A 连接在主服务器上的端口去减 B 连接在备用服务器上的端口，必然不相等，「漂移」随之成立。这个错误很隐蔽：只有当「等不到某条连接的观测」或「你有两个网卡」时才偶发，作者很难在自己机器上复现。 |
| ⑤ 把超时直接当作 被过滤，且只发一次 |
丢一个包，全锥形就变成端口受限 | 要减少这种误判必须重传，并且承认这个方向的结论只能是概率性的。单次超时不能证伪放行。 |
| ⑥ 让网页自己去猜 | 按候选地址里有没有 srflx 推类型 | 候选类型只能告诉你「有没有经过地址转换」，完全反映不出过滤行为，也反映不出映射是否漂移。 |
六、我们为什么不会犯上面这些错
- 对 ①：映射类探针（I、III）全程只来自同一条连接的同一个本地端口，过滤类探针（II、IV）全程只打在另一条连接的同一个映射上。任何「端口变了」都只能来自 NAT 行为，不可能来自换连接。
- 对 ②：我们把「映射是否漂移」放在判定的最前面，优先级高于「换 IP 能不能打通」。那类「对称映射 + 宽松过滤」的 NAT 不会被我们说成全锥形。
- 对 ③：我们有三块彼此独立的入口——主服务器 IP、另一个公网 IP、以及主 IP 上的另一个端口。前两个用来比对映射，后两个用来分辨「只按 IP 过滤」还是「连端口一起过滤」。更关键的是：拿不到映射比对时，我们不猜。判定表最后一行「无法判定」就是为此存在的。
- 对 ④：我们要求「同源可比」这个见证：两次端口观测必须来自同一条连接、同一个本地端口，并且该端口在两个目的地上各自只出现过一次。三个条件缺一个，就不允许下 NAT4 的结论。这条规则被自动化测试锁死，任何人改坏都会立刻让测试变红。
- 对 ⑤：每个探针都在 1.5 秒窗口内重传（默认 2 次，可配 1–5 次），并且只用「收到回包」这一侧做确定判断。「没收到」只用来收紧结论，不用来放宽。所以误差只会偏保守。
- 对 ⑥：判定全部发生在服务端，依据是真实的 UDP 报文往返，不依赖浏览器报告的候选类型，也不依赖页面脚本的推断。
七、我们不声称的三件事
说清楚，免得变成吹牛：
- 我们不说「100% 准确」。映射是否稳定，严格的定义是「对全体目的地址都成立」，而我们只能采样两个目的地。若一台 NAT 恰好只在这两个地址上给出相同端口、却在别处不同，我们会判它是锥形。这种 NAT 的端口对打洞而言仍是可预测的，结论在工程上无害，但在数学上我们要承认这是采样，不是全称证明。
- 丢包会让结论偏严。比如你其实是全锥形，但两个方向恰好都丢了包，我们会报得更严格，或者报「无法判定」。这是刻意的取舍：宁可低估，不高估。
- 多层 NAT 测到的是最严格的那一层。如果你和互联网之间有多层 NAT，我们测到的是其中行为最严格的一层。这不是误差，是 NAT 叠加的客观结果——决定你能不能打洞的，本来就是最严格的那道门。
八、结论
- 判成 NAT4，一定是 NAT4（定理一）。所以 NAT3 不会被测成 NAT4。
- 判成 NAT3 / NAT2，说明映射确实没漂移（定理二）。所以 NAT4 不会被测成 NAT3。
- 信息不足时输出「无法判定」，而不是猜一个类型。
- 万一出错，只会偏保守（定理三），不会把你的网络说得比实际更好。
这几条不是宣传语，是可以逐行对照代码、并被自动化测试反复验证的数学结论：判定树的每一个分支都有对应用例，576 组观测组合做了穷举。