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.

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

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

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

Censorship classifiers and traffic analysis attacks consistently exploit the initial seconds of a proxy connection, where packet-size, inter-arrival-time, and burst features are maximally discriminative. Cited work demonstrates that website fingerprinting classifiers trained solely on the first few seconds of Tor traffic achieve high accuracy, and real-world GFW detection of fully-encrypted protocols also targets early-connection bytes.

2025-pereira-extended §1 traffic-shapewebsite-fingerprintml-classifierdpifully-encrypted-detect

State-of-the-art ML classifiers (Deep Fingerprinting, Decision Tree, Random Forest, nPrintML) trained on known UPGen protocols and benign traffic always incur high out-of-distribution false-positive rates when attempting to block unknown UPGen protocols — in the vast majority of experiments the OOD FPR is 100%. The one exception (SSH OOD, Deep Fingerprinting) achieved a UPGen TPR of only 20%. By contrast, identical classifiers successfully generalize to block unknown Obfs4 flows with near-zero collateral damage in 3 of 4 cases.

2025-wails-censorship §4.3.3, Table 3, Table 4 dpiml-classifiertraffic-shape