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.
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.
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.
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.
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
- unilateral authentication of the server (mandatory),
- mutual authentication (optional)
- confidentiality and perfect forward secrecy of session keys and
- integrity of handshake messages.
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
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
ns, and the server Finished message, computed using
ns and recomputes the Finished message for Alice using
PSK_1. Alice returns
Finished message to Charlie who recomputes the Finished message for
PSK_2. At this point, Alice and Charlie share session keys
PSK_1 and Charlie and Bob share session keys derived from
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
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.
Download the technical paper.
Download the Real World Crypto slides.
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.