An adversary's false positive rate against a circumvention tool depends critically on the statistical properties of background traffic; if background traffic is modeled inaccurately (e.g., with toy uniform distributions), formal detection bounds are not meaningful. The paper proposes a hybrid pipeline: train NetDiffusion on real packet-level traces from campus networks or backbone providers, sample synthetic background traffic, extract empirical mean/variance, and integrate those distributions into EasyCrypt formal models to produce statistically grounded detectability proofs.

Security arguments for existing circumvention systems are based on ad-hoc adversary models that are often incomplete or unrepresentative of real-world adversaries, leading to allegedly secure designs that fail against relatively straightforward attacks. Protocols that substitute or parasitize a cover application's encrypted traffic channel fail against application-aware adversaries who observe or induce violations of application-specific behavioral invariants — a weakness that pre-trained classifiers on custom traces fail to surface.

§1, §2 defense

A machine-checked EasyCrypt proof demonstrates that a conjunctive SNI + traffic-profile adversary achieves a true positive rate of 1.0 against meek, with a false positive rate bounded by Pr[Game0(MeekEnc).main()=true] ≤ (1/10000) × (1/1000) ≈ 10⁻⁷, under the assumption that meek traffic follows a normal distribution centered at 512 bytes and background traffic a Poisson-like distribution centered at 1024 bytes. The proof is fully machine-checked in EasyCrypt.

§4.2 detection

The paper proposes modeling HCS undetectability as a simulation-based cryptographic distinguishability problem: if traces produced by the real-world HCS channel are computationally indistinguishable from ideal-world application-channel traces (T_HCS ∼ T_simulator), the HCS achieves provable security against any adversary — passive or active. The simulation paradigm is parametric in adversary capability, meaning a single proof covers the full spectrum from passive SNI monitoring to active DPI.

§1, §2 defense

The host-profiling censor (passive traffic analysis: count connections per server, block those exceeding a threshold τ within a window w) blocks essentially all circumvention user traffic within 30 time steps for all classifier qualities tested (ρ_TP ∈ {0.9, 0.95, 0.99}), while causing far less collateral damage than zig-zag (never exceeding ~30% innocent server blocking). Snowflake resists this attack well: with w=3, τ=3, over 94.48% of users receive a proxy within 2 steps even with worst-classifier rules, and final unblocked server rates are 91.24–99.04%. The host profiling approach is feasible for passive censors who cannot enumerate the distribution channel.

2026-fares-game §5.2, Table 2, Table 3 traffic-shapeml-classifier

Balboa's synchronous leaf-content replacement adds non-negligible timing differences that allow censors to identify its activity with up to ~90% accuracy over different network conditions. The timing anomaly arises because Balboa performs data substitution directly at each data exchange, delaying the server's response while covert data is prepared.

2026-kamali-huma §I (Introduction), §II-A traffic-shapeml-classifier

Huma's deferred-reply / double-request receive (DRR) protocol reduces a traffic-fingerprinting XGBoost classifier's accuracy to at most 54% (near random guessing) across geographically distributed clients (San Francisco, Frankfurt, Bangalore). A Kolmogorov-Smirnov test on absolute page-load timing distributions yields D=0.03, p=0.98 for U.S. clients — substantially tighter than Waterfall of Liberty's D=0.11 at p=0.5 — confirming that Huma flows are statistically indistinguishable from benign HTTPS fetches.

2026-kamali-huma §V-D, Table II traffic-shapeml-classifier

The PPBR (probabilistic profile-based routing) protocol leaks user community membership through observable routing decisions: in a controlled experiment with 800 majority and 200 minority users, a statistical disclosure attack achieved a true positive rate of 100% and false positive rate of 0% when identifying minority users. Even under a conservative PPBR configuration (top 1/3 fraction acceptance), the attack achieved 100% TPR and only 0.4% FPR.

2026-ratliff-mirage §V ml-classifiertraffic-shape

Banking apps from major Russian institutions (Sber, T-Bank, VTB, Alfa-Bank) combine VPN detection with behavioral biometrics — screen pressure, touch coordinates, and gesture timing — enabling cross-account re-identification of users behind proxies. 11 apps received a "RED" (maximum surveillance) rating. T-Bank, Yandex services, and MAX additionally deploy active anti-analysis features that detect research tooling on the device (rooted devices, emulators, Frida, etc.).

2026-rks-russian-apps-vpn-detection §5, §6 ml-classifiertraffic-shape

Amnesty International's 102-page investigation identifies a multi-vendor surveillance stack deployed in Pakistan: Chinese DPI (Geedge/MESA-derived), Canadian social-media monitoring (Netsweeper), and Emirati commercial spyware (Pegasus and FinFisher). The system enables deep packet inspection, SNI-based filtering, and traffic-shape classification at national scale, including targeted interception of encrypted messaging apps and VPN traffic.

2025-amnesty-pakistan-shadows §3, §5 dpisni-blockingip-blockingtraffic-shapeml-classifier