The goals of the TLS:DIV workshop are threefold: first, to explain and justify the latest changes to the TLS 1.3 design (from draft 13 to draft 19); second, to give an overview of some ongoing efforts to prove the cryptographic security of the TLS 1.3 protocol, and third, to showcase recent tools and methods to evaluate and improve the safety and security of TLS implementations, up to the level of cryptographic primitives.
The workshop is organized by the Everest project team and consists of invited talks from leading experts on key exchange security and implementation of cryptography on topics related to the analysis and implementation of TLS.
You can register for the workshop on the IACR website..
| Early Registration until March 31 |
Late registration and on-site |
|
|---|---|---|
| EuroS&P or EUROCRYPT attendees | USD $60 | USD $80 |
| Neither EuroS&P nor EUROCRYPT attendees | USD $80 | USD $100 |
| Time | Topic |
|---|---|
| 08:00-08:50 | Breakfast |
| 08:50-09:00 | Introduction and Opening Remarks |
| 09:00-09:30 |
Status update on the TLS 1.3 Standard (Eric Rescorla, Mozilla). Most of the papers published last year on TLS 1.3 consider draft 13 of the standard. Eric will give an overview of the main changes leading to draft 19. This presentation includes a Q&A session to allow participants to directly ask questions to the editor of the TLS 1.3 standard on any specification-related question. |
| 09:30-10:00 |
Implementing and Proving the TLS 1.3 Record Layer (Cédric Fournet, Microsoft Research). This talk introduces cryptographic security proofs by typing in F* using the Bellare-Rogaway code-based game-playing approach, and presents a security proof of the TLS record layer and its verified implementation. |
| 10:00-10:30 |
Secure Channels (Britta Hale, NTNU) Secure channel establishment is the fundamental goal of TLS; however, the exact goals of a secure channel remain elusive. Authenticated Encryption with Associated Data (AEAD) as well as Authenticated and Confidential Channel Establishment (ACCE) have been considered as end-goals with respect to TLS. This talk delves into the construction and goals of secure channels. |
| 10:30-11:00 | Coffee break |
| 11:00-11:30 |
Project Wycheproof (Thai Duong, Google) In cryptography, subtle mistakes can have catastrophic consequences, and cryptographic libraries fall into such implementation pitfalls much too often and for much too long. Good implementation guidelines, however, are hard to come by: understanding how to implement cryptography securely requires digesting decades' worth of academic literature. We recognize that software engineers fix and prevent bugs with unit testing, and we found that cryptographic loopholes can be resolved by the same means. These observations have prompted us to develop Project Wycheproof, a collection of unit tests that detect known weaknesses or check for expected behaviors of some cryptographic algorithm. Project Wycheproof provides tests for most cryptographic algorithms, including RSA, elliptic curve crypto and authenticated encryption. Our cryptographers have systematically surveyed the literature and implemented most known attacks. We have over 80 test cases which have uncovered more than 40 bugs. |
| 11:30-12:00 |
A Cryptographic Analysis of the TLS 1.3 Handshake Protocol (Felix Günther, TU Darmstadt) This talk covers cryptographic analyses of the draft TLS 1.3 full, resumption, and 0-RTT handshake protocols, presenting security proofs in an extended multi-stage key exchange framework which captures classical Bellare-Rogaway key secrecy for key exchange protocols that, like TLS 1.3, derive multiple keys. |
| 12:00-12:30 |
TLS-Attacker: Future directions in testing and fuzzing (Juraj Somorovsky , RUB) TLS-Attacker is a Java-based framework for flexible analysis of TLS libraries, which was used to find recent padding oracle attacks or boundary violations in major TLS implementations. This talk will give an overview of TLS-Attacker basic functionalities and present future plans regarding the implementation of new features and TLS tests. |
| 12:30-14:00 | Lunch break |
| 14:00-14:30 | Mechanized Computational Proof of the TLS 1.3 Standard Candidate (Bruno Blanchet, Inria Paris) We present a computational CryptoVerif model for TLS 1.3 Draft-18 and mechanically prove its security under standard assumptions on its cryptographic primitives. This model includes most features of TLS 1.3: handshakes with and without pre-shared key, with and without Diffie-Hellman ephemerals, key updates, optional client authentication, 0-RTT and 0.5-RTT data. To perform the proof, we split the protocol into 3 pieces that we independently prove in CryptoVerif: the initial handshake without pre-shared key; the handshake with pre-shared key and optionally Diffie-Hellman exchange; and the record protocol. Then, we manually compose the results together in order to obtain a proof of the full protocol. |
| 14:30-15:00 |
Mitigating cryptographic and application security attacks against TLS1.3 0-RTT data (Colm MacCarthaigh, Amazon) TLS 1.3’s new 0-RTT mode enables a game-changing user experience: no additional latency for encrypted data. But it also opens TLS up to new cryptographic and application-level attacks. This presentation will be a data-driven analysis of some of these attacks in realistic settings, along with suggested mitigations. |
| 15:00-15:30 |
Verified Assembly Language for Fast Cryptography (Chris Hawblitzel, Microsoft Research) We will present a new language called Vale, designed for formally verifying the high-performance assembly language code used in common implementations of cryptographic algorithms. Vale supports multiple architectures, including x86, x64, and ARM, and can be used to verify both functional correctness and information flow properties. We will describe the application of Vale to implementations of SHA-256, Poly1305, and AES-CBC, including verification of high-performance assembly language code ported from OpenSSL. |
| 15:30-16:00 | Coffee break |
| 16:00-16:30 |
Tamarin analysis of TLS 1.3: What did we prove? (Sam Scott, Royal Holloway) TLS 1.3 is a complex object, and warrants multiple analysis approaches. We present an overview of our analysis using the Tamarin prover, aiming to provide an insight into the construction of the model and the properties proven. |
| 16:30-17:00 |
Deployment and implementation of TLS 1.3 at Facebook (Kyle Nekritz, Facebook) Over the past year at Facebook we built and deployed a custom 0-RTT protocol based on QUIC Crypto called Zero Protocol, which currently carries the majority of our app's traffic. We are currently working on transitioning to TLS 1.3, and will talk about our rationale in moving to TLS 1.3, our current 1.3 deployment efforts and obstacles we've run into deploying TLS 1.3 over the internet, as well as our secure design abstractions and usage of 0-RTT data in HTTP2. |
| 17:00-17:30 |
Preparing for post-quantum cryptography in TLS (Douglas Stebila, McMaster University) I will discuss various issues involved in trying to use post-quantum cryptography in TLS 1.2 and 1.3. For key exchange, this includes matching the security properties offered by most post-quantum key exchange primitives with the properties required by security proofs. For signatures, this includes the challenges of certifying and conveying public keys from post-quantum signature schemes. In both cases, I will discuss constructions and compatibility issues for hybrid cryptography, where two (or more) algorithms are used simultaneously---one traditional, one post-quantum---for potential security improvements. |