The privacy of the TLS 1.3 protocol

TLS (Transport Layer Security) is a widely deployed protocol that plays a vital role in securing Internet traffic. Given the numerous known attacks for TLS 1.2, it was imperative to change and even redesign the protocol in order to address them. In August 2018, a new version of the protocol, TLS 1.3, was standardized by the IETF (Internet Engineering Task Force). TLS 1.3 not only benefits from stronger security guarantees, but aims to protect the identities of the server and client by encrypting messages as soon as possible during the authentication. In this paper, we model the privacy guarantees of TLS 1.3 when parties execute a full handshake or use a session resumption, covering all the handshake modes of TLS. We build our privacy models on top of the one defined by Hermans et al. for RFIDs (Radio Frequency Identification Devices) that mostly targets authentication protocols. The enhanced models share similarities to the Bellare-Rogaway AKE (Authenticated Key Exchange) security model and consider adversaries that can compromise both types of participants in the protocol. In particular, modeling session resumption is non-trivial, given that session resumption tickets are essentially a state transmitted from one session to another and such link reveals information on the parties. On the positive side, we prove that TLS 1.3 protects the privacy of its users at least against passive adversaries, contrary to TLS 1.2, and against more powerful ones