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.

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

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

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

The system targets a threat model where the censor performs passive DPI to fingerprint and block the client-to-TURN-proxy channel, and also conducts active enumeration attacks to discover and block proxy endpoints. The paper explicitly notes that traffic splitting may introduce distinct fingerprints of its own that require empirical evaluation — acknowledging that multi-path approaches are not fingerprint-free.

2025-vilalonga-extended §3.1 Threat Model dpiactive-probingtraffic-shape

Relying on third-party email providers to verify users was demonstrated by Ling et al. to leave Tor's BridgeDB vulnerable to censors capable of creating multiple accounts, enabling bridge enumeration via sock-puppet attacks at scale. Active and passive detection techniques — including traffic flow analysis, DPI, website fingerprinting, and active probing — have been demonstrated in prior work to reveal Tor bridges, making Tor inaccessible for the majority of users in some regions.

2023-tulloch-lox §2.2.1 active-probingdpitraffic-shapewebsite-fingerprintip-blocking

A two-phase passive-filter-plus-active-probing framework deployed at a 1-million-user ISP identified 85.90% of vanilla OpenVPN flows (1,718/2,000) and 72.67% of obfuscated flows (1,468/2,020), with an upper-bound false positive rate of 0.0039% across over 10 million flows — three orders of magnitude lower than prior ML-based approaches (1.4–5.5%). The system processed 15 TB and 2 billion flows per day on a single commodity server.

2022-xue-openvpn §9, Table 3 dpiactive-probingtraffic-shape