Introduction. Hidden communication systems (HCS) allow users to establish a communication channel over a public network by encoding information into existing or benign-looking traffic. The security goal is to ensure that the presence of this channel is not detectable by a network monitor. QUICstep [1] is an HCS that relies on QUIC [2], a transport protocol with a privacy-centric design that has recently seen widespread adoption, to evade censorship. In particular, defeating stateless censors that drop handshake packets based on the server name indication (SNI) field. Concretely, QUICstep leverages an existing HCS, such as a WireGuard [3] tunnel, to establish a secure channel to a proxy server outside the censor’s influence, for relaying all handshake packets containing SNI fields to the destination. All remaining data packets are then sent over the censored network path using QUIC’s connection migration feature, without being dropped by the censor. QUICstep can significantly improve the performance of the existing HCS by sending the bulk of data over low-latency high-throughput network paths.

Problem Statement. The design of QUICstep did not involve formal verification to ensure that the claimed security property, i.e., evading a stateless censor based on SNI blocking, holds for all possible configurations and in any network. We address this shortcoming by formally modeling all relevant aspects of QUICstep and rigorously proving its security properties. The challenge with this approach is that the security property of an HCS, namely undetectability, is different from security properties that are typically proven in formal modeling, such as secrecy and authenticity. These properties require that a given predicate, e.g., secrecy, holds for any possible protocol execution and arbitrary adversary behavior. However, to prove the undetectability of an HCS, a predicate cannot only consider a single protocol execution, but must instead ensure that the adversary cannot distinguish between executions with and without using the HCS.

Formal Model. We prove this indistinguishability using the symbolic prover Tamarin [4]. Tamarin has a built in Dolev-Yao adversary and supports common cryptographic primitives, such as signatures and encryption. We encode all QUICstep entities and their relevant interactions as a Tamarin model, which can then be executed by Tamarin resulting in so-called “execution traces”. The security properties are then encoded in Tamarin lemmas, which are statements over these execution traces, e.g., universal quantifier lemmas for properties such as secrecy and authenticity of the derived shared TLS session key, and existential quantifier lemmas for properties such as the feasibility and correctness of the QUIC handshake. For our core proof, we use Tamarin’s “Observational Equivalence” mode, which allows the comparison of two execution traces—in our case a regular QUIC connection and a QUICstep connection—and prove that they behave identically from the adversary’s point of view. 

Results. Our model shows that a stateless censor cannot distinguish between HTTPS GET request/response packet pairs generated by regular QUIC connections for non-censored resources and packet pairs generated by QUICstep connections for censored resources. We increase the confidence in the correctness of our model by additionally proving the feasibility, secrecy, and authenticity of our modeled TLS handshake. We also leverage Tamarin’s capability of automatically finding violating execution traces, to experiment with different threat models and, for example, show that QUICstep cannot defend against a stateful censor that observes handshake messages.

Conclusion. We believe that other formal verification efforts on hidden communication systems could benefit from our approach to detect protocol-level design flaws in these systems. As future work, we are exploring the automatic creation of Tamarin models from protocol specification documents, such as IETF RFCs, to automate our analysis for other HCS with minimal effort, as well as specification-based model validation to increase model reliability. Additionally, we plan to analyze HCS with properties similar to QUICstep, such as domain fronting, using our analysis approach. The presentation will be structured as follows: (1) introduction of the problem and limitations of state-of-the-art solutions, (2) our design approach including challenges we encountered and how we overcame them, (3) a brief discussion of our results, and finally (4) an outlook on ongoing and future work.