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
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.