Why OHTTP needed a formal proof
Oblivious HTTP (OHTTP) is conceptually straightforward: end-to-end encrypted requests and responses travel between client and server through an intermediary relay, so the relay sees only ciphertext plus the identities of the two endpoints. But "conceptually straightforward" is not the same as "provably correct." Before committing a new privacy protocol to standardization and production, it pays to verify that the cryptography actually delivers the intended guarantees.
To that end, Cloudflare ran a formal, machine-checked security analysis of OHTTP using the Tamarin theorem prover. The models and proofs are publicly available. This article explains what was modeled, which attacker was assumed, and what properties were proven.
What OHTTP actually does
OHTTP is a message-oriented proxy protocol. It forwards individual application messages — HTTP requests and responses — rather than proxying a TCP connection the way HTTP CONNECT does. That distinction matters. A connection-oriented proxy is general purpose: it tunnels any TCP-based application. A message-oriented proxy handles transactional exchanges: a client sends one request object, the server returns one response object. DNS queries and responses, or app-level API calls, fit this pattern.
The two properties OHTTP aims to provide are:
- Requests are not linked to client identifying information such as IP address or TLS fingerprint — the basic job of any proxy.
- Requests from the same client are not linkable to each other.
The second property matters for stateless applications. A connection-oriented protocol could also provide both properties — by opening a fresh, end-to-end TLS connection for each message — but that is prohibitively expensive for all parties. OHTTP's design achieves the same privacy goals with a single public-key encryption operation per message.
The transaction flow
A single OHTTP transaction involves four steps:
- The client encapsulates an HTTP request using the gateway's public key and sends it to the relay over a client–relay HTTPS connection.
- The relay forwards the encapsulated request to the gateway over its own HTTPS connection.
- The gateway decapsulates, recovers the HTTP request, and forwards it to the target server.
- The gateway encapsulates the response using a symmetric key shared with the client, returns it to the relay, and the relay forwards it back to the client.
The HTTP forwarding mechanics are unremarkable — POST requests over HTTPS. The cryptographic core is more interesting. The client first encodes its HTTP request as Binary HTTP per RFC9292, then feeds that binary value into HPKE (hybrid public key encryption). The gateway reverses both operations on receipt. Responses follow the same pattern: the gateway encodes the response as Binary HTTP, encrypts it with a key known only to client and gateway, and forwards the result back through the relay.
At no point does the relay see application data, and at no point does the gateway see the client's IP address — unless the two collude.
The attacker model
The analysis considered a simplified world with two clients, C1 and C2, one relay, and one gateway. The attacker observes all network traffic and can adaptively compromise either the relay or the gateway — but not the clients — and the relay and gateway are assumed not to collude. Once a party is compromised, the attacker has access to that party's session state and private keys. The attacker is additionally prohibited from passing client-identifying information such as IP addresses to the gateway (which would trivially defeat the scheme).
Both clients send requests Q1 and Q2 through the relay to the gateway, receiving answers A1 and A2. The attacker's goal is to link C1 to (Q1, A1) and C2 to (Q2, A2). The desired guarantees, stated informally, are:
- Requests and responses are known only to clients and gateways holding the corresponding HPKE keying material.
- The gateway cannot distinguish two identical requests from the same client from two identical requests from different clients, absent unique per-client keys.
Formal analysis proves properties of an idealized algebraic model of the protocol. That is distinct from formal verification, which proves a concrete implementation matches a design. Both are useful; this exercise was the former.
How Tamarin works
Tamarin models protocols using multiset rewriting. A protocol is a set of rules; each rule represents a discrete step and fires when its prerequisites are met. Tamarin stores available facts in a multiset — an unordered collection that, unlike a set, allows duplicates. When a rule fires, it consumes some facts and produces new ones, which may unlock further rules.
For example, a rule for the gateway generating its long-term HPKE encapsulation key has no prerequisites and produces the key as an output fact. A rule for the client generating a request requires, among other things, that such a key fact exists.
Each rule can also record action facts — side effects that mark events in time, such as "a message with contents m was sent at time t." When a protocol is run to completion following all possible rule orderings, the action facts form a directed acyclic graph (DAG) called the action graph. The graph captures every combination of messages and actions the protocol allows.
Security properties are expressed as queries over this graph, e.g., "in all runs, if the client finishes and can decrypt the response, the response was generated by an entity holding the shared secret." Rules can also model attacker capabilities — reading messages, compromising keys, and so on. The attacker in this model is an extended Dolev-Yao adversary: it controls the network (read, modify, drop, replay) and can additionally compromise protocol entities to learn their state and keys.
The proven properties
Five properties were proven against this attacker model. Each is a formal translation of an informal security goal.
Gateway authentication
Unless the attacker has compromised the gateway's long-term keys, if the client completes the protocol and decrypts the response, then the responder was the intended gateway, the gateway derived the same keys, the gateway saw the request the client sent, and the response received is the one the gateway sent. This is a bundle of properties, but they all fall under authentication: the participants agree on the data exchanged.
Request and response secrecy
The request and response are secret unless the attacker has compromised the gateway's long-term keys. This covers the malicious-gateway case, which amounts to the attacker knowing the gateway's keys.
Relay connection security
The contents of the client–relay connection are secret unless the attacker has compromised the relay. If the client itself is compromised, there is nothing to protect — the attacker knows the query before it is sent and can obtain the response by making an honest query.
AEAD nonce reuse resistance
If the gateway sends a message to the client and the attacker finds a second message encrypted with the same key and nonce, then either the gateway was already compromised or the attacker already knew the query. This rules out failure modes from nonce reuse in the response encryption, a class of bug previously found in ODoH.
Client unlinkability
If the attacker knows the query and the contents of the connection sent to the relay — i.e., the encrypted query — then it must have compromised both the gateway and the relay. That is the crux: linking ciphertext to plaintext requires both parties to collude with the attacker.
The proof does not claim full indistinguishability between clients. There are two ways to link queries: direct inference and statistical analysis. The anonymity trilemma rules out defending against statistical analysis, so that threat is declared out of scope. Direct inference is prevented by ensuring the attacker does not compromise both relay and gateway simultaneously. The one remaining protection is that a gateway cannot tell if two messages came from the same client, because the protocol carries no state between connections — a returning client is indistinguishable from a new one.
The full models, including the rule definitions for key generation, TLS session establishment, request encapsulation, and compromise, are available in the publicly released analysis repository along with the ODoH models that preceded it. The Tamarin prover itself is freely available, so the proofs can be independently rechecked.
