QUIC Privacy and Security Workshop 2020

A Security Model and Verified Implementation for the IETF QUIC Transport Protocol

Antoine Delignat-Lavaud, Cédric Fournet, Bryan Parno, Jonathan Protzenko, Tahina Ramananandro, Jay Bosamiya, Joseph Lallemand, Itsaka Rakotonirina, Yi Zhou

Abstract: We investigate the security of the QUIC transport, as standardized by the IETF in draft version 24. This version features major differences compared to Google’s original protocol and prior IETF drafts. We model packet and header encryption, which uses a custom construction for privacy. We propose a new security definition for authenticated encryption with semi-implicit nonces. We show that QUIC uses an instance of a generic construction parameterized by a standard AEAD-secure scheme and a PRF-secure cipher. We formalize and verify the security of this construction in F?. The proof uncovers interesting limitations of nonce confidentiality, due to the malleability of short headers and the ability to choose the number of least significant bits included in the packet counter. We propose improvements that simplify the proof and increase robustness against strong attacker models. In addition to the verified security model, we also implement the concrete functional specification, and prove that it satisfies important correctness properties (such as successful decryption of encrypted packets) after fixing more errors in the draft. Lastly, we provide a high-performance Low* implementation of packet stream encryption built on top of the verified EverCrypt crypto provider and the EverParse message formatting library, that we prove to be memory safe, correct with respect to our concrete specification (inheriting its functional correctness properties), and secure with respect to our verified model. To evaluate this component, we write a partial implementation of the QUIC transport in Dafny, and prove its memory safety once extracted to C++.

Two-Tier Authenticated Encryption: Nonce Hiding in QUIC

Mihir Bellare, Felix Günther, and Bjoern Tackmann

Abstract: The QUIC protocol introduces QUIC Packet Encryption (QPE) to protect the data during transmission. QPE encrypts the payload with nonce-based authenticated encryption. Part of the nonce, for which QUIC uses a sequence number, is transmitted with the ciphertext but is additionally, together with parts of the header, masked in order to prevent traffic analysis.

Motivated by QUIC’s use of one key for the masking and another key for the payload encryption, we begin by modeling two-tier encryption schemes that encrypt and decrypt different parts of the ciphertext using different keys, and possibly with different security properties. We explicitly model the guarantees required by the scheme used in QUIC, namely that the payload encryption is authenticated, while the masking scheme only ensures that a modification of the ciphertext will predictably induce a corresponding modification of the plaintext. The goal of this modeling is to formalize statements about the expected properties of QUIC, such as nonce-hiding and the ability to achieve forward secrecy by rotating the payload encryption key.

As a first step, we use the recent framework for nonce-hiding authenticated encryption of Bellare, Ng, and Tackmann (CRYPTO 2019) to analyze the encryption of the nonce. We model QPE as a type of nonce-based encryption scheme where encryption takes a pair (N_i, N_e) of nonces, but decryption obtains only N_e. This syntax, which was already present in the CAESAR call and was called AE5 by Namprempre, Rogaway, and Shrimpton, generalizes both the standard nonce-based encryption syntax (NBE1), where decryption obtains the full nonce, and the NBE2 syntax of Bellare et al., where the decryption does not obtain the nonce. We adapt the definitions of Bellare et al., and model and prove that QPE is partially nonce-hiding in the sense that it hides N_e.

Secure Communication Channel Establishment: TLS 1.3 (over TCP Fast Open) vs. QUIC

Shan Chen, Samuel Jero, Matthew Jagielski, Alexandra Boldyreva and Cristina Nita-Rotaru

Abstract: Secure channel establishment protocols such as Transport Layer Security (TLS) are some of the most important cryptographic protocols, enabling the encryption of Internet traffic. Reducing the latency (the number of interactions between parties) in such protocols has become an important design goal to improve user experience. The most important protocols addressing this goal are the just-released TLS 1.3, which is likely to see deployment in the near future, and Quick UDP Internet Connections (QUIC), a secure transport protocol from Google that is available in the Chrome browser. There have been a number of formal security analyses for TLS 1.3 and QUIC, but their security, when layered with their underlying transport protocols, cannot be easily compared. Our work is the first to thoroughly compare the security and availability properties of these protocols. Towards this goal, we develop novel security models that permit “layered” security analysis. In addition to the standard goals of server authentication and data privacy and integrity, we consider the goals of IP spoofing prevention, key exchange packet integrity, secure channel header integrity, and reset authentication, which capture a range of practical threats not usually taken into account by existing security models that focus mainly on the cryptographic cores of the protocols. Equipped with our new models we provide a detailed comparison of TLS 1.3 over TCP Fast Open (TFO), QUIC over UDP, and QUIC[TLS] (a new design for QUIC that uses TLS 1.3 key exchange) over UDP. In particular, we show that TFO’s cookie mechanism does provably achieve the security goal of IP spoofing prevention. Additionally, we find several new availability attacks that manipulate the early key exchange packets without being detected by the communicating parties. By including packet-level attacks in our analysis, our results shed light on how the reliability, flow control, and congestion control of the above layered protocols compare, in adversarial settings. We hope that our results will help protocol designers in their future protocol analyses and that our results will help practitioners better understand the advantages and limitations of novel secure channel establishment protocols.

QuicR: QUIC Resiliency to BW-DoS Attacks

Ori Hiba, Amir Herzberg, and Hemi Leibowitz

Abstract: We present QuicR, an adaptation of the QUIC protocol, which is resilient to congestion(BW-DoS attacks). Specifically, QuicR uses Forward Error Correction (FEC) to ensure reliable communication between applications, even when using lossy, high-latency connections, as is common under clogging. QuicR can be easily deployed by applications, using TCP-like API,and supports different application requirements, includingFIFO / non-FIFO, lossy / non-lossy,elastic / inelastic (QoS)traffic and optional caching of responses to queries.We describe the design and an initial, partial implementation of QuicR. We also present experimental evaluation of this implementation, confirming that it performs well under a different realistic scenarios. We focus on high loss-rate and latency scenarios, typical to BW-DoS attacks, where both TCP and QUIC fail or perform poorly.

Robust Channels: Handling Unreliable Network Messages in QUIC’s Record Layer

Marc Fischlin, Felix Günther, and Christian Janson

Abstract: The common approach in channel protocols is to rely on ciphertexts arriving in-order and close the connection upon any rogue ciphertext, and cryptographic security models for channels generally reflect such design. This is reasonable when running atop lower-level transport protocols like TCP ensuring in-order delivery, as for example is the case with TLS or SSH. However, channels such as QUIC or DTLS which run over a non-reliable transport protocol like UDP, do not—and in fact cannot—close the connection if packages are lost or arrive in a different order. Those protocols instead have to carefully catch such effects arising naturally in unreliable networks by using a sliding-window technique where ciphertexts can be decrypted correctly as long as they are not misplaced too far. To accommodate such handling of unreliable network messages, we introduce a generalized notion of robustness to cryptographic channel modeling. This property can capture unreliable network behavior and guarantees that adversarial tampering cannot hinder ciphertexts that can be decrypted correctly from being accepted. As one particularly interesting target, we capture the packet encryption in QUIC’s record layer as a cryptographic channel protocol and show that it achieves the intended level of robustness based on certain properties of the sliding-window technique and the underlying AEAD scheme.

QUIC Security Summary

Martin Thomson

Summary: A summary of QUIC’s design and security features will be presented. Open issues and areas requiring further analysis will be identified and discussed.

On Wire Images

Brian Trammell

Authenticated QUIC Handshakes

Chris Wood (on behalf of Christian Huitema and Kazuho Oku)

Summary: This talk will explain a proposal that uses a variant of QUIC protocol version 1 that uses TLS Encrypted Client Hello (ECHO) keys to authenticate the Initial packets thereby making the entire handshake tamper-proof.

nQUIC (Noise + QUIC)

Mathias Hall-Andersen, David Wong, Nick Sullivan, and Alishah Chator

Summary: We present nQUIC, a variant of QUIC-TLS that uses the Noise protocol framework for its key exchange and basis of its packet protector with no semantic transport changes. nQUIC is designed for deployment in systems and for applications that assert trust in raw public keys rather than PKI-based certificate chains. It uses a fixed key exchange algorithm, compromising agility for implementation and verification ease. nQUIC provides mandatory server and optional client authentication, resistance to Key Compromise Impersonation attacks, and forward and future secrecy of traffic key derivation, which makes it favorable to QUIC-TLS for long-lived QUIC connections in comparable applications. We developed two interoperable prototype implementations written in Go and Rust. Experimental results show that nQUIC finishes its handshake in a comparable amount of time as QUIC-TLS.

Towards Securing the Internet of Things with QUIC

Lars Eggert

Summary: This paper is the first to evaluate the feasibility of deploying QUIC, a new UDP-based transport protocol currently undergoing IETF standardization, directly on resource-constrained IoT devices. It quantifies the storage, compute, memory and energy requirements of the Quant QUIC stack on two different IoT platforms, and finds that a minimal standards-compliant QUIC client currently requires approximately 58 to 63 KB of flash and can retrieve 5 KB of data in 4.2 to 5.1 s over 0-RTT or 1-RTT connections, using less than 16 KB of heap memory (plus packet buffers), less than 4 KB of stack memory and less than 0.9 J of energy per transaction.