Automated Analysis of TLS 1.3: 0-RTT, Resumption and Delayed Authentication

Cas Cremers, Marko Horvat, Sam Scott, Thyla van der Merwe
University of Oxford, UK & Royal Holloway, University of London, UK

Download the technical paper
A version of this paper, substantially similar in content to this version, has been accepted to appear at IEEE S&P 2016.

Introduction

The TLS protocol is used globally by millions of users on a daily basis, serving as the core building block for Internet security. The various flaws identified in TLS 1.2 and below, be they implementation- or specification-based, have prompted the TLS Working Group to adopt an "analysis-before-deployment" design paradigm in drafting the next version of the protocol. After a development process of many months, the TLS 1.3 specification is nearly complete.

In the spirit of contributing towards this new design philosophy, we model the TLS 1.3 specification using the Tamarin prover, a tool for the automated analysis of security protocols. We show that revision 10 of the specification meets the goals of authenticated key exchange for any combination of unilaterally and mutually authenticated handshakes.

By extending our revision 10 model to incorporate the desired delayed client authentication mechanism, we uncovered a potential attack in which an adversary is able to successfully impersonate a client during a PSK-resumption handshake. Our attack highlighted the strict necessity of including more information in the client signature contents. The IETF TLS Working Group updated revision 11 of the TLS 1.3 specification draft based on our report.

Our work provides the first supporting evidence for the security of several complex protocol mode interactions in TLS 1.3. Our formal model can be extended to future releases, thus being of long-lasting benefit. We give a brief overview of our methodology in the following sections.

TLS 1.3

In comparison to TLS 1.2, TLS 1.3 encrypts more of the handshake, reduces handshake latency and employs only AEAD schemes. The new handshake modes of TLS 1.3 include a 1-RTT initial (EC)DHE mode, a 0-RTT mode, a (Pre-Shared Key) PSK mode and a PSK-DHE mode. For further details see the TLS 1.3 specification draft.

Building a Model

For our analysis, we use the Tamarin prover, a tool for the symbolic analysis of security protocols. Tamarin enables us to precisely specify and analyse the secrecy and authentication properties of the various handshake modes. Furthermore, Tamarin's multiset rewriting semantics are well-suited for modelling the complex transition system implied by the TLS 1.3 specification; the tool allows us to analyse the interaction of an unbounded number of concurrent TLS sessions. The tool and further documentation can be found on its webpage.

The first step of our analysis is to construct an abstraction of the handshake and record protocols which we then encode as Tamarin rules. Rules capture honest-party and adversary actions alike. In the case of legitimate clients and servers, our constructed model rules generally correspond to all processing actions associated with respective flights of messages. Our first client rule, for instance, captures a client generating and sending all necessary parameters as part of the first flight of an (EC)DHE handshake, as well as keeping track of them in the local client state. This rule, C_1, is visible in the client state machine diagram below. The diagram represents the union of all the options that a client has in different executions.

Client state machines for TLS 1.3 revision 10

Partial client state machines for TLS 1.3 revision 10, as modelled in our analysis.

Proving Stated Goals and Security Properties

The second step of the analysis involves encoding the desired security properties as Tamarin lemmas. The goal of the TLS handshake protocol is to allow for unilateral or, optionally, mutual entity authentication of communicating parties, as well as to establish a shared secret that is unavailable to eavesdroppers and adversaries who can place themselves in the middle of the connection. The TLS record protocol is intended to provide confidentiality and integrity of application data. Hence, we encode the following properties as lemmas

and aim to show that each property holds.

While Tamarin can automatically construct proofs for simple protocols, its proof-finding heuristics are not yet strong enough to automatically generate full proofs for TLS 1.3. In practice this meant that we augmented Tamarin's search with substantial manual effort: inspecting partial proofs and deducing appropriate hints (in the form of lemmas) to guide Tamarin's proof search.

Using this approach, we establish that revision 10 of the TLS 1.3 specification meets the goals of authenticated key exchange in all possible combinations of client, server, and adversary behaviours.

Attacking Client Authentication

In extending our revision 10 model to include the delayed client authentication mechanism as proposed by the TLS Working Group, we found an attack which violates client authentication, as an adversary can can impersonate a client when communicating with a server. The attack is similar to the Triple Handshake attack and works as follows:

Step 1: Alice (the victim client) starts a connection with Charlie (the man-in-the-middle), and Charlie starts a connection with Bob (the targeted server). In both connections a PSK is established. Alice shares PSK_1 with Charlie and Charlie shares PSK_2 with Bob.

Step 2: Alice resumes a connection with Charlie using PSK_1. Alice generates a random nonce nc and this is sent to Charlie. Charlie reuses this nonce to initiate a PSK-resumption handshake with Bob. Bob responds with a random nonce ns, and the server Finished message, computed using PSK_2. Charlie reuses ns and recomputes the Finished message for Alice using PSK_1. Alice returns her Finished message to Charlie who recomputes the Finished message for Bob using PSK_2. At this point, Alice and Charlie share session keys derived from PSK_1 and Charlie and Bob share session keys derived from PSK_2.

Step 3: Following resumption, Charlie attempts to make a request of Bob that requires client authentication. Charlie is subsequently prompted for his certificate and verification. Charlie re-encrypts this request for Alice. To compute the verification signature, Alice uses the session_hash value, which is defined as the hash of all handshake messages excluding the Finished messages. This session_hash value will match the one of Charlie and Bob, and hence Charlie can re-encrypt Alice's signature for Bob, who accepts Alice's certificate and verification as valid authentication for Charlie.

The attack is possible due to the lack of a strong binding between the client signature and the session for which that signature is intended. We note that revision 11 of the TLS 1.3 specification defines the client signature based on a Handshake Context value that includes the Finished message. This appears to address the attack as the adversary would now need to force the Finished messages to match across the two sessions. Although the inclusion of the Finished message in the Handshake Context message was suggested in Pull Request #316, the TLS Working Group was unaware of the strict requirement to mitigate this attack.

Downloads

Download the technical paper.
Download the Real World Crypto slides.

Support

Part of this work was completed whilst Sam Scott and Thyla van der Merwe were interns at Mozilla. We would like to thank Eric Rescorla, Martin Thomson and the TLS Working Group for their invaluable inputs to this work by way of numerous clarifying conversations.