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.

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

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.

§3 evaluation

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 paper identifies a fundamental architectural vulnerability in single-IP circumvention designs: a relay must generate new observable flows (via DNS or TLS SNI) to reach end services after receiving client connections, creating a detectable server-and-client behavioral contrast. A relay accessing user-facing domains (news, social media) scores high on a Relay Suspicion Score (w=0.9) versus infrastructure domains (w=0.1). The paper argues this host-level signal is censorship-invariant and cannot be concealed by link obfuscation.

2026-almutairi-server §2.4, §4 traffic-shapedpisni-blocking

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

Internal Geedge documents confirm active contracts to deploy GFW-derived censorship and surveillance infrastructure in Myanmar, Pakistan, Ethiopia, Kazakhstan, and at least one additional unidentified country under the Belt and Road framework, in addition to domestic deployments in Xinjiang, Jiangsu, and Fujian. The exported product (the Tiangou Secure Gateway / TSG line) is not a stripped-down export variant — leaked TSG documentation shows DPI, active-probing, ML classifiers, and granular per-region traffic control rules that mirror the domestic GFW capability set.

2025-geedge-mesa-leak §5, §6 dpiactive-probingml-classifiersni-blockingdns-poisoningfully-encrypted-detecttraffic-shape

InterSecLab's 76-page analysis of the Geedge/MESA leak (based on nine months of indexing and translating >100,000 documents) characterizes the Tiangou Secure Gateway (TSG) product line as a commercially deployable detection stack that combines deep packet inspection, real-time mobile subscriber monitoring, active probing, ML-based traffic classifiers, and granular per-region rule sets. TSG is not a research prototype — leaked documentation includes deployment timelines and client government interactions for Kazakhstan, Ethiopia, Pakistan, Myanmar, and one unnamed country, with censorship rules explicitly tailored to each region.

2025-interseclab-internet-coup §3–§5 (InterSecLab report) dpiactive-probingml-classifiersni-blockingip-blockingtraffic-shapefully-encrypted-detect

Justice for Myanmar documents that Geedge Networks supplied Myanmar's military junta with GFW-derived surveillance and censorship infrastructure under Belt and Road frameworks following the February 2021 coup. The deployed system (Tiangou Secure Gateway / TSG) incorporates the same DPI, active-probing, and ML-classifier capabilities as the domestic Chinese GFW, giving Myanmar one of the most technically capable censorship systems in Southeast Asia.

2025-jfm-silk-road-surveillance §3, §5 dpisni-blockingip-blockingtraffic-shapeml-classifieractive-probing

A three-stage detection pipeline exploiting the "dual-role" behavioral fingerprint of single-IP circumvention relays achieved 23.2% recall (96/414 ground-truth relays) with a 0.18% false-positive rate against 97,651 benign TLS servers, for an overall accuracy of 99.5%. The ground-truth set covered OpenVPN, WireGuard, and SOCKS relays identified in a 17 TB single-day backbone trace (WIDE Project, April 9, 2025).

2026-almutairi-server §3.4, Table 1 traffic-shapedpiflow-correlation