search

net4people / bbs

Forum for discussing Internet censorship circumvention
3.19k stars 75 forks source link

A Symbolic Analysis of Privacy for TLS 1.3 with Encrypted Client Hello (CCS 2022) #326

Open wkrp opened 4 months ago

wkrp commented 4 months ago

A Symbolic Analysis of Privacy for TLS 1.3 with Encrypted Client Hello Karthikeyan Bhargavan, Vincent Cheval, Christopher A. Wood https://research.cloudflare.com/publications/Bhargavan2022/ https://gitlab.inria.fr/chevalvi/echo_tls PDF

This is a formal privacy model and verification of Encrypted Client Hello (ECH) in TLS 1.3 using ProVerif, a symbolic protocol analyzer. While there has been much work on the formal verification of the security of TLS 1.3, there has been comparatively little on its privacy—and ECH modifies the TLS handshake in non-trivial ways, such that it is not obvious that even security proofs continue to hold. This paper builds on an existing model of TLS 1.3, extending it with ECH as well as enriching it with new protocol options and branches. The new verification shows that TLS with ECH keeps the security properties (authentication, confidentiality, integrity) of TLS without ECH, and also satisfies additional privacy properties. The proofs are, the authors say, at the cutting edge of what automated verification tools can do.

TLS 1.3 made privacy advancements over TLS 1.2: in particular, server certificates (and client certificates, when used) that are exchanged during the handshake are now encrypted, removing one source of identity leakage. But TLS 1.3 still had the well-known identity leak in the Client Hello message's Server Name Indication (SNI) extension. ProVerif quickly finds that TLS 1.3 without ECH does not protect server identity, because of the visible SNI. Hiding the SNI from passive and active network adversaries is not so easy to achieve, however. Section 4 shows a failed early attempt: draft-00 of what was then called ESNI was vulnerable to a "cut-and-paste" attack, in which an active attacker could replay an encrypted SNI to learn what server identity a client requested. The authors' modeling discovered other attacks against earlier draft versions, which have helped guide the change from ESNI to ECH, from encrypting just the SNI to encrypting the entire Client Hello.

Security and privacy properties are enumerated in Section 3. The new privacy properties are CIP (client identity privacy), UNL (client unlinkability), SIP (server identity privacy), and C-EXT and S-EXT (client and server extension privacy). The model only covers the TLS protocol itself, omitting outside factors that nevertheless are important for privacy. For example, IP addresses as an identity side channel: ECH can, at best, provide anonymity within the set of SNIs supported at a given IP address. Server administrators need to take care that different sites support the same cryptographic capabilities, and are otherwise identical in their externally visible handshake features. Things like traffic analysis and website fingerprinting of the traffic stream, after the handshake, are likewise outside the scope of this work.

wkrp commented 4 months ago

An interesting aspect of ECH, that perhaps is not yet widely appreciated, is that clients are supposed to send an ECH extension even when they are not using ECH. The presence of an ECH extension in a Client Hello does not automatically mean the SNI is encrypted. Section 4:

The protocol design also tries to hide whether a particular connection uses the ECH extension or not (a principle sometimes called "do not stick out"). Hence, a client that does not have the client-facing server's public key, will still send an ECH extension containing a random string whose contents are indistinguishable from an encrypted ClientHelloInner. This is referred to as a fake ClientHello or grease. We model grease in our work, but do not try to prove any extra privacy property for this feature.

There's a thoughtful discussion of the "do not stick out" criterion in ECH draft:

https://www.ietf.org/archive/id/draft-ietf-tls-esni-17.html#section-10.9.4

As a means of reducing the impact of network ossification, [RFC8744] recommends SNI-protection mechanisms be designed in such a way that network operators do not differentiate connections using the mechanism from connections not using the mechanism. To that end, ECH is designed to resemble a standard TLS handshake as much as possible. The most obvious difference is the extension itself: as long as middleboxes ignore it, as required by [RFC8446], the rest of the handshake is designed to look very much as usual.

The GREASE ECH protocol described in Section 6.2 provides a low-risk way to evaluate the deployability of ECH. It is designed to mimic the real ECH protocol (Section 6.1) without changing the security properties of the handshake. The underlying theory is that if GREASE ECH is deployable without triggering middlebox misbehavior, and real ECH looks enough like GREASE ECH, then ECH should be deployable as well. Thus, our strategy for mitigating network ossification is to deploy GREASE ECH widely enough to disincentivize differential treatment of the real ECH protocol by the network.

Ensuring that networks do not differentiate between real ECH and GREASE ECH may not be feasible for all implementations. While most middleboxes will not treat them differently, some operators may wish to block real ECH usage but allow GREASE ECH. This specification aims to provide a baseline security level that most deployments can achieve easily, while providing implementations enough flexibility to achieve stronger security where possible. Minimally, real ECH is designed to be indifferentiable from GREASE ECH for passive adversaries with following capabilities:

  1. The attacker does not know the ECHConfigList used by the server.
  2. The attacker keeps per-connection state only. In particular, it does not track endpoints across connections.
  3. ECH and GREASE ECH are designed so that the following features do not vary: the code points of extensions negotiated in the clear; the length of messages; and the values of plaintext alert messages.

This leaves a variety of practical differentiators out-of-scope. including, though not limited to, the following:

  1. the value of the configuration identifier;
  2. the value of the outer SNI;
  3. the TLS version negotiated, which may depend on ECH acceptance;
  4. client authentication, which may depend on ECH acceptance; and
  5. HRR issuance, which may depend on ECH acceptance.

These can be addressed with more sophisticated implementations, but some mitigations require coordination between the client and server. These mitigations are out-of-scope for this specification.