1,721,172 research outputs found
Key Derivation Functions Without a Grain of Salt
No full textKey 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
Identification of cryptographic algorithms in binary programs
No full textCette thèse traite de la conception de méthodes automatisées ou semi-automatisées pour détecter et identifier des algorithmes cryptographiques dans des programmes compilés en langage machine. La première méthode proposée a pour but l'identification de primitives symétriques. L'implémentation en langage machine d'une primitive symétrique, assimilée à une suite d'instructions, est représentée par un graphe. Sous cette forme, le code est modifié à l'aide de règles de réécriture tout en préservant une certaine notion de sémantique lors d'une phase dite de normalisation. L'objectif est de faire émerger des expressions communes à différentes implémentations d'une même primitive. Ces expressions servent alors de base à la création de signatures efficaces. La recherche de ces signatures s'effectue à l'aide d'un algorithme énumérant les isomorphismes de sous-graphe. La seconde méthode, conçue en complément de la première, produit une représentation synthétique facilitant l'identification des modes opératoires. Cette représentation se définit comme le plus petit sous-graphe préservant les distances entre des sous-ensembles de nœuds précédemment identifiés comme étant les paramètres d'entrée et de sortie des primitives impliquées.This thesis is about the design of automatic or semi-automatic methods to detect and identify cryptographic algorithms inside programs compiled into machine code. Two methods are presented. The objective of the first method is to identify cryptographic primitives. A machine code implementation of a cryptographic primitive, regarded as a sequence of instructions, is represented by a graph structure. During a normalization phase, a set of rewrite rules is used to modify this graph representation while preserving a specific notion of semantics. The goal is to converge towards expressions which are shared across several implementations of the same primitive. We use these expressions as a basis to create efficient signatures. A subgraph isomorphism enumeration algorithm is used to search for signatures. The second method is built on top of the first one. It produces a synthetic representation designed to help in the identification of modes of operation. This synthetic representation is defined as the smallest subgraph which preserve distances between sets of vertices previously identified as the input and output parameters of the primitives involved within the mode of operation
Computing the endomorphism ring of a supersingular elliptic curve from a full rank suborder
No full textIn this paper, we study the problem of computing the endomorphism ring of a supersingular elliptic curve given the knowledge of a full rank suborder. We provide a polynomial time quantum algorithm to solve this problem in full generality. This result enhances our understanding of the endomorphism ring problem, which is at the core of isogeny-based cryptography. As part of our approach, we also present a polynomial time quantum algorithm to solve the problem of computing the endomorphism ring of the codomain curve of an isogeny from a curve with known endomorphism ring. This extends the work of [CII+23a] by lifting their restrictions on the number of factors of the isogeny degree. As an application, we present quantum reductions between key hard problems in isogeny-based cryptography. We show that some of our quantum reductions are tighter than the classical ones, while all reductions are of polynomial time complexity. In particular, we improve the query complexity of the reduction of the EndRing problem to the OneEnd problem from poly(logp) (classically) to O(1) (quantumly), strengthening the hardness assumption of the OneEnd problem in the post-quantum setting. This reduction underlies the 2-special soundness proof of SQIsign identification protocols
Sécurité prouvée pour les protocoles de la vie réelle
No full textLa sécurité prouvée est un outil cryptographique particulièrement utile pour évaluer la sécurité d'un protocole. Pour construire une preuve, il faut d'abord définir les propriétés de sécurité à atteindre, c'est-à-dire le modèle de sécurité, ainsi que le type d'adversaire auquel nous sommes confrontés. Ces deux éléments représentent le contexte de la preuve, qui sera calculée après avoir « formaté » le protocole dans le modèle. Dans cette thèse, nous introduisons (ou adaptons) des modèles dans lesquels nous donnons des preuves de sécurité pour trois types de protocoles ayant des applications pratiques : un protocole de messagerie sécurisé, une signature assainissable, et un pare-feu inversé. Pour le premier, nous proposons quelques corrections aux faiblesses du protocole Signal et de son analyse de sécurité précédente. Ensuite, pour le second, nous étendons la signature assainissable pour inclure une nouvelle fonctionnalité, et donc nous étendons les propriétés de sécurité pré-existantes pour la prendre en compte. Enfin, pour la troisième, nous proposons un modèle plus réaliste et plus inclusif que ce qui avait été fait auparavant. Dans les trois cas, nous construisons un protocole que nous prouvons sécurisé dans le modèle défini.Provable security is a very useful cryptographic tool that helps in the evaluation of the security of a protocol. In order to construct a proof, one must first define the security properties that are to be achieved, i.e., the security model, as well as what kind of adversary we are facing. These two components represent the context of the proof, which we can compute after fitting the protocol to the model. In this thesis, we introduce (or adapt) models in which we give security proofs for three kinds of protocols with real-life applications: a secure messaging protocol, a sanitizable signature, and a reverse firewall. For the first, we propose some corrections to the weaknesses of the Signal protocol and its previous security analysis. Then, for the second, we extend sanitizable signature to include a new feature, and thus extend the previous security properties to take this feature into account. Finally, for the third, we propose a more realistic and inclusive model than what had been done before. In all three, we build a protocol that we show is secure in the model we defined
Cryptographie dans la nature : la sécurité des implémentations cryptographiques
No full textLes attaques par canaux auxiliaire sont redoutables face aux implémentations cryptographiques. Malgré les attaques passées, et la prolifération d'outils de vérification, ces attaques affectent encore de nombreuses implémentations. Dans ce manuscrit, nous abordons deux aspects de cette problématique, centrés autour de l'attaque et de la défense. Nous avons dévoilé plusieurs attaques par canaux auxiliaires microarchitecturaux sur des implémentations de protocoles PAKE. En particulier, nous avons exposé des attaques sur Dragonfly, utilisé dans la nouvelle norme Wi-Fi WPA3, et SRP, déployé dans de nombreux logiciel tels que ProtonMail ou Apple HomeKit. Nous avons également exploré le manque d'utilisation par les développeurs d'outil permettant de détecter de telles attaques. Nous avons questionné des personnes impliqués dans différents projets cryptographiques afin d'identifier l'origine de ce manque. De leur réponses, nous avons émis des recommandations. Enfin, dans l'optique de mettre fin à la spirale d'attaques-correction sur les implémentations de Dragonfly, nous avons fournis une implémentation formellement vérifiée de la couche cryptographique du protocole, dont l'exécution est indépendante des secrets.Side-channel attacks are daunting for cryptographic implementations. Despite past attacks, and the proliferation of verification tools, these attacks still affect many implementations. In this manuscript, we address two aspects of this problem, centered around attack and defense. We unveil several microarchitectural side-channel attacks on implementations of PAKE protocols. In particular, we exposed attacks on Dragonfly, used in the new Wi-Fi standard WPA3, and SRP, deployed in many software such as ProtonMail or Apple HomeKit. We also explored the lack of use by developers of tools to detect such attacks. We questioned developers from various cryptographic projects to identify the origin of this lack. From their answers, we issued recommendations. Finally, in order to stop the spiral of attack-patch on Dragonfly implementations, we provide a formally verified implementation of the cryptographic layer of the protocol, whose execution is secret-independent
Analysis of the Telegram Key Exchange
Full text linkWe describe, formally model, and prove the security of Telegram’s key exchange protocols for client-server communications. To achieve this, we develop a suitable multi-stage key exchange security model along with pseudocode descriptions of the Telegram protocols that are based on analysis of Telegram’s specifications and client source code. We carefully document how our descriptions differ from reality and justify our modelling choices. Our security proofs reduce the security of the protocols to that of their cryptographic building blocks, but the subsequent analysis of those building blocks requires the introduction of a number of novel security assumptions, reflecting many design decisions made by Telegram that are suboptimal from the perspective of formal analysis. Along the way, we provide a proof of IND-CCA security for the variant of RSA-OEAP+ used in Telegram and identify a hypothetical attack exploiting current Telegram server behaviour (which is not captured in our protocol descriptions). Finally, we reflect on the broader lessons about protocol design that can be taken from our work
POKÉ:A Compact and Efficient PKE from Higher-dimensional Isogenies
Full text linkWe introduce a new PKE protocol, POKÉ, based on isogenies of unknown degree. The protocol relies on two new techniques: the first constructs an SIDH square while also working with higher-dimensional representations, whereas the second allows us to obtain a shared secret even when all curves in the commutative diagram are known.The resulting protocol is compact and extremely efficient. We provide a proof-of-concept implementation in SageMath of POKÉ that shows encryption and decryption taking about a hundred milliseconds at security level I: POKÉ is thus the most efficient encryption protocol from isogenies, and it outperforms existing protocols by more than an order of magnitude
Hollow LWE::A New Spin, Unbounded Updatable Encryption from LWE and PCE
Full text linkUpdatable public-key encryption (UPKE) allows anyone to update a public key while simultaneously producing an update token, given which the secret key holder could consistently update the secret key. Furthermore, ciphertexts encrypted under the old public key remain secure even if the updated secret key is leaked – a property much desired in secure messaging. All existing lattice-based constructions of UPKE update keys by a noisy linear shift. As the noise accumulates, these schemes either require super-polynomial-size moduli or an a priori bounded number of updates to maintain decryption correctness.Inspired by recent works on cryptography based on the lattice isomorphism problem, we propose an alternative way to update keys in lattice-based UPKE. Instead of shifting, we rotate them. As rotations do not induce norm growth, our construction supports an unbounded number of updates with a polynomial-size modulus. The security of our scheme is based on the LWE assumption over hollow matrices – matrices which generate linear codes with non-trivial hull – and the hardness of permutation code equivalence. Along the way, we also show that LWE over hollow matrices is as hard as LWE over uniform matrices, and that a leftover hash lemma holds for hollow matrices
Juggernaut: Efficient Crypto-Agnostic Byzantine Agreement
No full textIt is well known that a trusted setup allows one to solve the Byzantine agreement problem in the presence of t < n/2 corruptions, bypassing the setup-free t < n/3 barrier. Alas, the overwhelming majority of protocols in the literature have the caveat that their security crucially hinges on the security of the cryptography and setup, to the point where if the cryptography is broken, even a single corrupted party can violate the security of the protocol. Thus these protocols provide higher corruption resilience (n/2 instead of n/3) for the price of increased assumptions. Is this trade-off necessary? We further the study of crypto-agnostic Byzantine agreement among n parties that answers this question in the negative. Specifically, let ts and ti denote two parameters such that (1) 2ti+ts < n, and (2) ti ≤ ts < n/2. Crypto-agnostic Byzantine agreement ensures agreement among honest parties if (1) the adversary is computationally bounded and corrupts up to ts parties, or (2) the adversary is computationally unbounded and corrupts up to ti parties, and is moreover given all secrets of all parties established during the setup. We propose a compiler that transforms any pair of resilience-optimal Byzantine agreement protocols in the authenticated and information-theoretic setting into one that is crypto-agnostic. Our compiler has several attractive qualities, including using only O(λn2) bits over the two underlying Byzantine agreement protocols, and preserving round and communication complexity in the authenticated setting. In particular, our results improve the state-of-the-art in bit complexity by at least two factors of n and provide either early stopping (deterministic) or expected constant round complexity (randomized). We therefore provide fallback security for authenticated Byzantine agreement for free for ti ≤ n/4.EPF
Authenticated key exchange protocols in three parties
No full textDans cette thèse, nous nous sommes intéressés à la sécurité des protocoles d’authentification et de dérivations de clefs dans le cas où une troisième entité intermédiaire, partiellement de confiance, est requise pour différentes raisons pratiques. Dans un premier temps, nous nous sommes focalisés sur le protocole AKA, dont les différentes versions sont utilisées pour établir un canal sécurisé sur la voix radio au sein des réseaux mobiles 3G et 4G. Nous avons d’abord fait état des faiblesses de sécurité et celles concernant le respect de la vie privée des clients mobiles durant l’établissement d’un tel canal sécurisé. Différentes solutions pratiques ont été proposé afin d’assurer les propriétés de sécurité et de vie privée requises par le 3GPP au sein des réseaux 3G, 4G. Dans un second temps, nous avons analysé le protocole Keyless SSL utilisé au sein des CDNs afin d’établir le canal sécurisé requis pour les communications HTTPS. Nous avons proposé un modèle de sécurité calculatoire recoupant l’ensemble des besoins de sécurité et ainsi pointé les différentes faiblesses de sécurité de la proposition Keyless SSL. Par conséquent, une variante basée sur TLS 1.2 a été proposé.In this thesis, we study the security of authentication and key exchange protocols when they are proxied through a semi-trusted third party is required. We begin by focusing on the security of the UMTS/LTE AKA protocol, when the different versions of this protocol are used to establish a secure channel across a radio access link in 3G and 4G mobile networks. We first describe some security and privacy weaknesses during the execution of the EPS- and UMTS-AKA protocols. Then, several practical solutions are proposed, guaranteeing better security and privacy for this protocol in both 3G and 4G scenarios. Secondly, we focus on computer networks, more precisely on the use of the Keyless SSL in proxying over HTTPS. A security model including the different various, specific security requirements from the web delivery context has been established. We also identify and discuss various weaknesses in the structure of Keyless SSL. Finally, we propose an improvement of Keyless SSL over TLS 1.2, and describe how Keyless SSL could work securely for the new TLS 1.3 protocol version
- …
