International Association
for Cryptologic Research

Signal recently deployed a new handshake protocol named PQXDH to protect against "harvest-now-decrypt-later" attacks of a future quantum computer. To this end, PQXDH adds a post-quantum KEM to the Diffie-Hellman combinations of the prior X3DH handshake. In this work, we give a reductionist security analysis of Signal's PQXDH handshake in a game-based security model that captures the targeted "maximum-exposure" security against both classical and quantum adversaries, allowing fine-grained compromise of user's long-term, semi-static, and ephemeral key material. We augment prior such models to capture not only the added KEM component but also the signing of public keys, which prior analyses did not capture but which adds an additional flavor of post-quantum security in PQXDH. We then establish fully parameterized, concrete security bounds for the classical and post-quantum session key security of PQXDH, and discuss how design choices in PQXDH make a KEM binding property necessary and how a lack of domain separation reduces the achievable security. Our discussion of KEM binding and domain separation complements the concurrent tool-based analysis of PQXDH by Bhargavan, Jacomme, Kiefer, and Schmidt (USENIX Security 2024), which pointed out a potential re-encapsulation attack if the KEM shared secret does not bind the public key. In contrast to the tool-based analysis, we analyze all protocol modes of PQXDH and its "maximum-exposure" security. We further show that both Kyber (used in PQXDH) and the NIST standard ML-KEM (expected to replace Kyber) satisfy a novel binding notion we introduce and rely on for our PQXDH analysis, which may be of independent interest.

Key derivation functions (KDFs) are integral to many cryptographic protocols. Their functionality is to turn raw key material, such as a Diffie-Hellman secret, into a strong cryptographic key that is indistinguishable from random. This guarantee was formalized by Krawczyk together with the seminal introduction of HKDF (CRYPTO 2010), in a model where the KDF only takes a single key material input. Modern protocol designs, however, regularly need to combine multiple secrets, possibly even from different sources, with the guarantee that the derived key is secure as long as at least one of the inputs is good. This is particularly relevant in settings like hybrid key exchange for quantum-safe migration. Krawczyk's KDF formalism does not capture this goal, and there has been surprisingly little work on the security considerations for KDFs since then. In this work, we thus revisit the syntax and security model for KDFs to treat multiple, possibly correlated inputs. Our syntax is assertive: We do away with salts, which are needed in theory to extract from arbitrary sources in the standard model, but in practice, they are almost never used (or even available) and sometimes even misused, as we argue. We use our new model to analyze real-world multi-input KDFs---in Signal's X3DH protocol, ETSI's TS 103-744 standard, and MLS' combiner for pre-shared keys---as well as new constructions we introduce for specialized settings---e.g., a purely blockcipher-based one. We further discuss the importance of collision resistance for KDFs and finally apply our multi-input KDF model to show how hybrid KEM key exchange can be analyzed from a KDF perspective.

The common approach in secure communication channel protocols is to rely on ciphertexts arriving in-order and to close the connection upon any rogue ciphertext. 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, protocols like QUIC or DTLS which run over a non-reliable transport such as UDP, do not—and in fact cannot—close the connection if packets are lost or arrive in a different order. Those protocols instead have to carefully catch effects arising naturally in unreliable networks, usually by using a sliding-window technique where ciphertexts can be decrypted correctly as long as they are not misplaced too far. In order to be able to capture QUIC and the newest DTLS version 1.3, we introduce a generalized notion of robustness of cryptographic channels. This property can capture unreliable network behavior and guarantees that adversarial tampering cannot hinder ciphertexts that can be decrypted correctly from being accepted. We show that robustness is orthogonal to the common notion of integrity for channels, but together with integrity and chosen-plaintext security it provides a robust analog of chosen-ciphertext security of channels. In contrast to prior work, robustness allows us to study packet encryption in the record layer protocols of QUIC and of DTLS 1.3 and the novel sliding-window techniques both protocols employ. We show that both protocols achieve robust chosen-ciphertext security based on certain properties of their sliding-window techniques and the underlying AEAD schemes. Notably, the robustness needed in handling unreliable network messages requires both record layer protocols to tolerate repeated adversarial forgery attempts. This means we can only establish non-tight security bounds (in terms of AEAD integrity), a security degradation that was missed in earlier protocol drafts. Our bounds led the responsible IETF working groups to introduce concrete forgery limits for both protocols and the IRTF CFRG to consider AEAD usage limits more broadly.

Users increasingly store their data in the cloud, thereby benefiting from easy access, sharing, and redundancy. To additionally guarantee security of the outsourced data even against a server compromise, some service providers have started to offer end-to-end encrypted (E2EE) cloud storage. With this cryptographic protection, only legitimate owners can read or modify the data. However, recent attacks on the largest E2EE providers have highlighted the lack of solid foundations for this emerging type of service. In this paper, we address this shortcoming by initiating the formal study of E2EE cloud storage. We give a formal syntax to capture the core functionality of a cloud storage system, capturing the real-world complexity of such a system’s constituent interactive protocols. We then define game-based security notions for confidentiality and integrity of a cloud storage system against a fully malicious server. We treat both selective and fully adaptive client compromises. Our notions are informed by recent attacks on E2EE cloud storage providers. In particular we show that our syntax is rich enough to capture the core functionality of MEGA and that recent attacks on it arise as violations of our security notions. Finally, we present an E2EE cloud storage system that provides all core functionalities and that is both efficient and provably secure with respect to our selective security notions. Along the way, we discuss challenges on the path towards bringing the security of cloud storage up to par with other end-to-end primitives, such as secure messaging and TLS.

Common verification steps in cryptographic protocols, such as signature or message authentication code checks or the validation of elliptic curve points, are crucial for the overall security of the protocol. Yet implementation errors omitting these steps easily remain unnoticed, as often the protocol will function perfectly anyways. One of the most prominent examples is Apple's goto fail bug where the erroneous certificate verification skipped over several of the required steps, marking invalid certificates as correctly verified. This vulnerability went undetected for at least 17 months. In this talk, we ask whether cryptographic implementations have to be so brittle. What if we could make crypto bugs surface through noticeable errors in a program's functionality? We introduce a mechanism which supports such detection of implementation errors on a cryptographic level. Instead of merely returning a binary acceptance decision, we let verification procedures return more fine-grained information in form of what we call a confirmation code. We then show how to escalate verification errors affecting these confirmation codes to functional errors on the overall protocol level. Concretely, we show that when confirmation codes satisfy a carefully defined unpredictability property, we can provably integrate them into secure connection establishment via key exchange and tie security to basic functionality: if verification steps in the key exchange are faulty, the connection establishment will fail, making an implementation error like goto fail detectable through a simple connection test. We present intuitive (and provably secure) confirmation codes for RSA-PSS signatures, HMAC, and the validation of elliptic curve points and discuss what is needed for their practical deployment.

Censorship circumvention tools enable clients to access endpoints in a network despite the presence of a censor. Censors use a variety of techniques to identify content they wish to block, including patterns that are characteristic of proxy or circumvention protocols. In response to this class of blocking behavior, circumvention practitioners have developed a family of "fully encrypted" protocols (FEPs), intended to have traffic that appears indistinguishable from random. For such protocols to be effective it is crucial that one can establish shared keys and protocol agreement without revealing to observers that an obfuscated protocol is in use. Despite their social significance to millions of users, there is no formal description of security for this handshake phase. This talk recounts the development of the obfs4 handshake, a highly-adopted FEP used to enable access to the Tor network in censored regions, which has incurred an iterative design process in response to censor behavior. We then present concrete results from our work formalizing obfuscated key exchange, capturing the goals of these protocols concretely and analyzing the obfs4 design. We demonstrate how to extend the obfs4 design to defend against stronger censorship attacks and to make it quantum-safe. With our analysis in mind, we point to challenges that remain in modeling and improving upon obfuscated protocols for future work.

In Internet security protocols including TLS 1.3, KEMTLS, MLS and Noise, HMAC is being assumed to be a dual-PRF, meaning a PRF not only when keyed conventionally (through its first input), but also when "swapped" and keyed (unconventionally) through its second (message) input. We give the first in-depth analysis of the dual-PRF assumption on HMAC. For the swap case, we note that security does not hold in general, but completely characterize when it does; we show that HMAC is swap-PRF secure if and only if keys are restricted to sets satisfying a condition called feasibility, that we give, and that holds in applications. The sufficiency is shown by proof and the necessity by attacks. For the conventional PRF case, we fill a gap in the literature by proving PRF security of HMAC for keys of arbitrary length. Our proofs are in the standard model, make assumptions only on the compression function underlying the hash function, and give good bounds in the multi-user setting. The positive results are strengthened through achieving a new notion of variable key-length PRF security that guarantees security even if different users use keys of different lengths, as happens in practice.

EDHOC is a lightweight authenticated key exchange protocol for IoT communication, currently being standardized by the IETF. Its design is a trimmed-down version of similar protocols like TLS 1.3, building on the SIGn-then-MAc (SIGMA) rationale. In its trimming, however, EDHOC notably deviates from the SIGMA design by sending only short, non-unique credential identifiers, and letting recipients perform trial verification to determine the correct communication partner. Done naively, this can lead to identity misbinding attacks when an attacker can control some of the user keys, invalidating the original SIGMA security analysis and contesting the security of EDHOC. In this talk we present a computational analysis capturing the potential attack vectors introduced by non-unique credential identifiers. We show that EDHOC, in its latest draft version 17, indeed achieves the intended key exchange security with user authentication even in a strong model where the adversary can register malicious keys with colliding identifiers, given that the employed signature scheme provides so-called exclusive ownership. Through our security result, we confirm cryptographic improvements integrated by the IETF working group in recent draft versions of EDHOC based on recommendations from our and others' analysis. We will comment on these fruitful interactions with the IETF LAKE working group in the talk, as an encouraging example of how proactive security analyses accompanying standardization efforts benefit real-world cryptography.

The key exchange protocol that establishes initial shared secrets in the handshake of the Signal end-to-end encrypted messaging protocol has several important characteristics: (1) it runs asynchronously (without both parties needing to be simultaneously online), (2) it provides implicit mutual authentication while retaining deniability (transcripts cannot be used to prove either party participated in the protocol), and (3) it retains security even if some keys are compromised (forward secrecy and beyond). All of these properties emerge from clever use of the highly flexible Diffie--Hellman protocol. While quantum-resistant key encapsulation mechanisms (KEMs) can replace Diffie--Hellman key exchange in some settings, there is no KEM-based replacement for the Signal handshake that achieves all three aforementioned properties, in part due to the inherent asymmetry of KEM operations. In this paper, we show how to construct asynchronous deniable key exchange by combining KEMs and designated verifier signature (DVS) schemes. There are several candidates for post-quantum DVS schemes, either direct constructions or via ring signatures. This yields a template for an efficient post-quantum realization of the Signal handshake with the same asynchronicity and security properties as the original Signal protocol.

The pre-shared key (PSK) handshake modes of TLS 1.3 allow for the performant, low-latency resumption of previous connections and are widely used on the Web and by resource-constrained devices, e.g., in the Internet of Things. Taking advantage of these performance benefits with optimal and theoretically-sound parameters requires tight security proofs. We give the first tight security proofs for the TLS 1.3 PSK handshake modes. Our main technical contribution is to address a gap in prior tight security proofs of TLS 1.3 which modeled either the entire key schedule or components thereof as independent random oracles to enable tight proof techniques. These approaches ignore existing interdependencies in TLS 1.3's key schedule, arising from the fact that the same cryptographic hash function is used in several components of the key schedule and the handshake more generally. We overcome this gap by proposing a new abstraction for the key schedule and carefully arguing its soundness via the indifferentiability framework. Interestingly, we observe that for one specific configuration, PSK-only mode with hash function SHA-384, it seems difficult to argue indifferentiability due to a lack of domain separation between the various hash function usages. We view this as an interesting insight for the design of protocols, such as future TLS versions. For all other configurations however, our proofs significantly tighten the security of the TLS 1.3 PSK modes, confirming standardized parameters (for which prior bounds provided subpar or even void guarantees) and enabling a theoretically-sound deployment.

Established security bounds for the TLS 1.3 full (1-RTT) and pre-shared key (PSK) handshake protocols grow quadratically with the total number of handshakes across all users. Due to the pervasive use of TLS, these bounds are so loose that they give no guarantees for the standardized parameters used in practice. We give new proofs and concrete bounds that justify the use of these parameters both in principle and in practice. We also discuss the pitfalls that arise when trying to capture the TLS 1.3 key schedule within the random oracle model.

We introduce puncturable key wrapping (PKW), a new cryptographic primitive that supports fine-grained forward security properties in symmetric key hierarchies. We develop syntax and security definitions, along with provably secure constructions for PKW from simpler components (AEAD schemes and puncturable PRFs). We show how PKW can be applied in two distinct scenarios. First, we show how to use PKW to achieve forward security for TLS 1.3 0-RTT session resumption, even when the server's long-term key for generating session tickets gets compromised. This extends and corrects a recent work of Aviram, Gellert, and Jager (Journal of Cryptology, 2021). Second, we show how to use PKW to build a protected file storage system with file shredding, wherein a client can outsource encrypted files to a potentially malicious or corrupted cloud server whilst achieving strong forward-security guarantees, relying only on local key updates.

Messaging schemes such as the Signal protocol rely on out-of-band channels to guarantee the authenticity of long-running communication. However those out-of-band checks may rarely be performed in practice. In this talk, we propose a method for performing continuous authentication during the communication, without needing an out-of-band channel. Leveraging the users' long-term secrets, our Authentication Steps extension guarantees authenticity as long as long-term secrets are not compromised, strengthening Signal's post-compromise security, and further allows to detect a potential compromise of long-term secrets after the fact via an out-of-band channel. Our protocol comes with a formal definition for continuous authentication and security proof, as well as a prototype implementation which seamlessly integrates on top of the official Signal Java library, together with bandwidth and storage overhead benchmarks.

The Signal protocol for end-to-end encrypted messaging provides a range of desirable security properties: asynchronicity, offline deniability, mutual implicit authentication, forward secrecy, and post-compromise security. Transitioning Signal to a post-quantum secure version with the same guarantees proves tricky, however. This is due to the fact that post-quantum key encapsulation mechanisms cannot be used as a drop-in replacement for the clever use of the Diffie--Hellman protocol in Signal's initial key exchange X3DH. In this talk, we elaborate on this obstacle, which may arise in further high-level protocols with subtle security guarantees, and show how to achieve asynchronous deniable key exchange from key encapsulation mechanisms and designated verifier signatures. In particular, we present a provably-secure construction for the post-quantum Signal initial key agreement which achieves the same security guarantees as the currently used X3DH.

We analyze the handshake protocol of the Transport Layer Security (TLS) protocol, version 1.3. We address both the full TLS 1.3 handshake (the one round-trip time mode, with signatures for authentication and (elliptic curve) Diffie–Hellman ephemeral ((EC)DHE) key exchange), and the abbreviated resumption/“PSK” mode which uses a pre-shared key for authentication (with optional (EC)DHE key exchange and zero round-trip time key establishment). Our analysis in the reductionist security framework uses a multi-stage key exchange security model, where each of the many session keys derived in a single TLS 1.3 handshake is tagged with various properties (such as unauthenticated versus unilaterally authenticated versus mutually authenticated, whether it is intended to provide forward security, how it is used in the protocol, and whether the key is protected against replay attacks). We show that these TLS 1.3 handshake protocol modes establish session keys with their desired security properties under standard cryptographic assumptions.

Secure channel protocols like QUIC and DTLS 1.3 run over unreliable-transport networks like UDP. They have to carefully catch effects arising naturally in those networks while protecting against malicious interference. In this talk, we introduce the notion of robustness for cryptographic channels, generically capturing this behavior. Our robustness notion guarantees that adversarial tampering cannot hinder ciphertexts that can be decrypted correctly from being accepted. We establish that QUIC and DTLS 1.3 achieve the desired level of robustness. Notably though, their robust behavior translates to a practically relevant security degradation (when compared to, e.g., TLS 1.3) which we will highlight in this talk. The security bounds we establish have led the responsible IETF working groups to mandate concrete forgery limits in recent updates to both protocol drafts.

Much of public key cryptography is designed in the Random Oracle Model, which assumes parties have access to one or more independent random functions. Implementing these random functions securely, usually via a cryptographic hash function, critically requires a technique called domain separation. This talk is about how spectacularly wrong things can go when domain separation is not done right, and simple ways to do it right. We begin with a case study on random oracle implementation in the NIST PQC KEM standardization effort, giving attacks arising from poor domain separation on some submissions, and classifying the remaining submissions from dubious to good. We then give a library of proof-validated domain separations that are secure, easy to implement, and usable in any type of cryptographic protocol, not just PQC KEMs.

It is convenient and common for schemes in the random oracle model to assume access to multiple random oracles (ROs), leaving to implementations the task --we call it oracle cloning-- of constructing them from a single RO. The first part of the paper is a case study of oracle cloning in KEM submissions to the NIST Post-Quantum Cryptography standardization process. We give key-recovery attacks on some submissions arising from mistakes in oracle cloning, and find other submissions using oracle cloning methods whose validity is unclear. Motivated by this, the second part of the paper gives a theoretical treatment of oracle cloning. We give a definition of what is an "oracle cloning method" and what it means for such a method to "work," in a framework we call read-only indifferentiability, a simple variant of classical indifferentiability that yields security not only for usage in single-stage games but also in multi-stage ones. We formalize domain separation, and specify and study many oracle cloning methods, including common domain-separating ones, giving some general results to justify (prove read-only indifferentiability of) certain classes of methods. We are not only able to validate the oracle cloning methods used in many of the unbroken NIST PQC KEMs, but also able to specify and validate oracle cloning methods that may be useful beyond that.