Position Paper: A Case for Machine-Checked Verification of Circumvention Systems

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 ml-classifiertraffic-shapedpi generic

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 sni-blockingtraffic-shape generic

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 traffic-shapeml-classifier

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 dpitraffic-shapeactive-probing