TLS 1.3 Ready or Not (TRON) Workshop Programme

Session 1:  Analysis of TLS 1.3

The OPTLS Protocol and TLS 1.3

Authors: Hugo Krawczyk and Hoeteck Wee
Speaker: Hugo Krawczyk

We present the OPTLS key-exchange protocol, its design, rationale and cryptographic analysis. The OPTLS design has been motivated by the work in the IETF for specifying TLS 1.3, and has informed the ongoing development of the protocol. OPTLS offers a simple design framework that supports the requirements of TLS 1.3 with a uniform and modular logic that can help the specification, analysis, performance optimization, and future maintenance of the protocol. The current TLS 1.3 draft builds upon the OPTLS framework as a basis for the cryptographic core of the handshake protocol, adapting the OPTLS modes and its HKDF-based key derivation to the TLS 1.3 context.

https://eprint.iacr.org/2015/978

Slides

A Cryptographic Analysis of the TLS 1.3 draft-10 Full and Pre-shared Key Handshake Protocol

Authors: Benjamin Dowling, Marc Fischlin, Felix Günther and Douglas Stebila
Speaker: Felix Günther

We analyze the handshake protocol of TLS 1.3 draft-ietf-tls-tls13-10 (published October 2015). This continues and extends our previous analysis (CCS 2015, Cryptology ePrint Archive 2015) of former TLS 1.3 drafts (draft-ietf-tls-tls13-05 and draft-ietf-tls-tls13-dh-based). Here we show that the full (EC)DHE Diffie-Hellman-based handshake of draft-10 is also secure in the multi-stage key exchange framework of Fischlin and Günther which captures classical Bellare-Rogaway key secrecy for key exchange protocols that derive multiple keys.

We also note that a recent protocol change—the introduction of a NewSessionTicket message for resumption, encrypted under the application traffic key—impairs the protocol modularity and hence our compositional guarantees that ideally would allow an independent analysis of the record protocol. We additionally analyze the pre-shared key modes (with and without ephemeral Diffie-Hellman key), and fit them into the composability framework, addressing composability with the input resumption secret from a previous handshake and of the output session keys.

https://eprint.iacr.org/2016/081

Slides

Session 2:  More Analysis of TLS 1.3

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

Authors: Cas Cremers, Marko Horvat, Sam Scott and Thyla van der Merwe
Speaker: Thyla van der Merwe

After a development process of many months, the TLS 1.3 specification is nearly complete. In order to prevent past mistakes, this crucial security protocol must be thoroughly scrutinised prior to deployment. We model and analyse revision 10 of the TLS 1.3 specification using the Tamarin prover, a tool for the automated analysis of security protocols. We show that revision 10 meets the goals of authenticated key exchange in both the unilateral and mutual authentication cases. We extend our model to incorporate the desired delayed client authentication mechanism and uncover a potential attack in which an adversary is able to successfully impersonate a client during a PSK resumption handshake. This observation was reported to, and confirmed by, the IETF TLS Working Group, and has informed revision 11 of the specification draft. Our work provides the first supporting evidence for the security of several complex protocol mode interactions in TLS 1.3, and highlights the strict necessity of including more information in the protocol’s signature contents.

http://tls13tamarin.github.io/TLS13Tamarin/

Slides

ProScript-TLS: Verifiable Models and Systematic Testing for TLS 1.3

Authors: Karthikeyan Bhargavan, Nadim Kobeissi and Benjamin Beurdouche
Speaker:  Karthik Bhargavan

We describe our ongoing work on implementing a verified reference implementation of TLS 1.0-1.3 in JavaScript. The core protocol code is written in ProScript, a statically typed subset of JavaScript, from we can automatically extract a symbolic cryptographic protocol model in the applied pi calculus and verify it using the protocol analyzer ProVerif. Our implementation interoperates with Mozilla’s NSS implementation of TLS 1.3 and with all other libraries for TLS 1.0-1.2. We will report on our experience in implementing TLS 1.3 and present results from our ProVerif analysis.In particular, we will evaluate the security of data sent during different phases of the TLS 1.3 handshake and we will analyze alternative key schedules for the protocol. Finally, we will show how our JavaScript implementation can be used by other TLS 1.3 implementers to test their code for state-machine bugs, a la SmackTLS.

Slides

(De-)Constructing TLS 1.3

Authors: Markulf Kohlweiss, Ueli Maurer, Cristina Onete, Björn Tackmann and Daniele Venturi
Speaker: Björn Tackmann

SSL/TLS is one of the most widely deployed cryptographic protocols on the Internet. It is used to protect the confidentiality and integrity of transmitted data in various client-server applications. The currently specified version is TLS 1.2, and its security has been analyzed extensively in the cryptographic literature.

In this paper, we analyze the security of a slightly modified version of a recent TLS 1.3 draft. (We do not encrypt the server’s certificate.) Our security analysis is performed in the constructive cryptography framework. This ensures that the resulting security guarantees are composable and can readily be used in subsequent protocol steps, such as password-based user authentication over a TLS-based communication channel in which only the server is authenticated. Most steps of our proof hold in the standard model, with the sole exception that the key derivation function HKDF is used in a way that has a proof only in the random-oracle model. Beyond the technical results on TLS 1.3, this work also exemplifies a novel approach towards proving the security of complex protocols by a modular, step-by-step decomposition, in which smaller sub-steps are proved in isolation and then the security of the protocol follows by the composition theorem.

https://eprint.iacr.org/2014/020.pdf

Slides

Session 3:  Implementation Security

Towards a Provably Secure Implementation of TLS 1.3

Authors: Benjamin Beurdouche, Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cedric Fournet, Samin Ishtiaq, Markulf Kohlweiss, Jonathan Protzenko, Nikhil Swamy, Santiago Zanella-Béguelin and Jean Karim Zinzindohoué
Speaker: Antoine Delignat-Lavaud

We report ongoing work towards a verified reference implementation of TLS 1.3 in the F* programming language, building up on previous efforts verifying prior TLS versions in miTLS using F# and F7. In particular, we report on the problems we have encountered from the perspective of developers of an existing TLS stack trying to implement support for TLS 1.3. More specifically, we present our new application interface and its expected security goals, now accounting for the negotiation of potential 0-RTT data from the client, and potential 0.5-RTT data from the server. We also present the structure of the new record layer, along with the ambiguities of its state machine, and the complexity of its key schedule. Lastly, we investigate how to an implementation of TLS 1.3 can retain compatibility with current versions, while mitigating downgrade attacks. Based on our experience, we propose several simplifications to the protocol that could reduce the implementation burden for TLS 1.3, and highlight underspecified aspects of the protocol.

https://www.mitls.org/

https://github.com/mitls

Not-quite-so-broken TLS 1.3 Mechanised Conformance Checking

Authors: David Kaloper-Meršinjak and Hannes Mehnert
Speaker:  Hannes Mehnert

We present a set of tools to aid TLS 1.3 implementors, all derived from a single TLS implementation/model.  These include an automated offline TLS protocol conformance checker, a test oracle validating recorded sessions, a tool replicating recorded sessions with other implementations, and an interactive online handshake visualisation.

The conformance checker repeatedly runs a user-provided TLS implementation, attempting to establish TLS sessions with it; the checker explores the TLS parameter space to determine feature coverage of the provided implementation. The test oracle takes a recorded session between two endpoints and decides whether the session was conformant with the specification.  The replication utility re-runs one side of a recorded session against another TLS implementation, and observes its behaviour.  The online visualisation accepts connections from clients and presents the TLS session as an interactive sequence diagram.

All of these tools are based on our clean-slate nqsb-TLS implementation/model. It already supports TLS 1.0-1.2, and interoperates with a broad range of other TLS implementations. We are currently extending nqsb-TLS with TLS 1.3 support, and tracking the progress of the TLS 1.3 draft, adapting our implementation/model accordingly.

We invite the community to use our tools while implementing the TLS 1.3 RFC, and provide feedback on deviations in the interpretation thereof. This process enables the community to converge to a single, mechanically checkable TLS 1.3 model, as implemented by nqsb-TLS.

https://www.cl.cam.ac.uk/~hm519/tron.pdf

Slides

Session 4:  Attacks and Defences

On the Security of TLS 1.3 (and QUIC) Against Weaknesses in PKCS#1 v1.5 Encryption

Authors: Tibor Jager, Joerg Schwenk and Juraj Somorovsky
Speaker: Tibor Jager

Encrypted key transport with RSA-PKCS#1 v1.5 is the most commonly deployed key exchange method in all current versions of the Transport Layer Security (TLS) protocol, including the most recent version 1.2. However, it has several well-known issues, most importantly that it does not provide forward secrecy, and that it is prone to side channel attacks that may enable an attacker to learn the session key used for a TLS session. A long history of attacks shows that RSA-PKCS#1 v1.5 is extremely difficult to implement securely. Therefore it seems a wise decision that the current draft of TLS version 1.3 dispenses with this key transport method. But is this sufficient to protect against weaknesses in RSA-PKCS#1 v1.5?

We describe attacks which transfer the potential weakness of prior TLS ver- sions to TLS 1.3, even though it does not even support PKCS#1 v1.5 encryption. The attack enables an attacker to impersonate a server by using a vulnerable TLS-RSA server implementation as a “signing oracle” to compute valid signa- tures for messages chosen by the attacker.

The attack on TLS 1.3 requires a very fast “Bleichenbacher-oracle” to create the TLS CertificateVerify message before the client drops the connection. Even though this limits the practical impact of this attack, it demonstrates that simply removing a legacy algorithm from a standard is not necessarily sufficient to protect against its weaknesses.

https://www.nds.rub.de/media/nds/veroeffentlichungen/2015/08/21/Tls13QuicAttacks.pdf

Slides

Metadata Protection Considerations for TLS Present and Future

Author / Speaker: Bryan Ford

TLS 1.3 takes important steps to improve both performance and security, so far offers little protection against traffic analysis or fingerprinting using unencrypted metadata or other side-channels such as transmission lengths and timings. This paper explores metadata protection mechanisms for TLS, including already-included provisions (e.g., record padding), provisions not yet included but potentially feasible in TLS 1.3 (e.g., optional or encrypted headers), and provisions that are likely too ambitious to achieve in TLS 1.3 but may be worth considering for a future “TLS 2.0” (e.g., fully encrypted and authenticated negotiation/handshaking). In addition, we briefly explore how these metadata protection provisions might apply to the datagram-oriented DTLS, or to a version of TLS supporting out-of-order delivery atop TCP.

http://bford.info/pub/net/tlsmeta-abs

Slides

Panel discussion: What do we know and where are we going?

Panelists:  TBA