Recent years have seen many advances in designing secure messaging protocols, aiming at provably strong security properties in theory or high efficiency for real-world practical deployment. However, important trade-off areas of the design space inbetween these elements have not yet been explored.In this work we design the first provably secure protocol that at the same time achieves (i) strong resilience against fine-grained compromise, (ii) temporal privacy, and (iii) immediate decryption with constant-size overhead, notably, in the post-quantum (PQ) setting. Besides these main design goals, we introduce a novel definition of offline deniability suitable for our setting, and prove that our protocol meets it, notably when combined with a PQ offline deniable initial key exchange.
Recent years have seen many advances in designing secure messaging protocols, aiming at provably strong security properties in theory or high efficiency for real-world practical deployment. However, important trade-off areas of the design space inbetween these elements have not yet been explored.In this work we design the first provably secure protocol that at the same time achieves (i) strong resilience against fine-grained compromise, (ii) temporal privacy, and (iii) immediate decryption with constant-size overhead, notably, in the post-quantum (PQ) setting. Besides these main design goals, we introduce a novel definition of offline deniability suitable for our setting, and prove that our protocol meets it, notably when combined with a PQ offline deniable initial key exchange.
In the past few years secure messaging has become mainstream, with over a billion active users of end-to-end encryption protocols such as Signal. The Signal Protocol provides a strong property called post-compromise security to its users. However, it turns out that many of its implementations provide, without notification, a weaker property for group messaging: an adversary who compromises a single group member can read and inject messages indefinitely. We show for the first time that post-compromise security can be achieved in realistic, asynchronous group messaging systems. We present a design called Asynchronous Ratcheting Trees (ART), which uses tree-based Diffie-Hellman key exchange to allow a group of users to derive a shared symmetric key even if no two are ever online at the same time. ART scales to groups containing thousands of members, while still providing provable security guarantees. It has seen significant interest from industry, and forms the basis for two draft IETF RFCs and a chartered working group. Our results show that strong security guarantees for group messaging are practically achievable in a modern setting.
In this work we study communication with a party whose secrets have already been compromised. At first sight, it may seem impossible to provide any type of security in this scenario. However, under some conditions, practically relevant guarantees can still be achieved. We call such guarantees "post-compromise security". We provide the first informal and formal definitions for post-compromise security, and show that it can be achieved in several scenarios. At a technical level, we instantiate our informal definitions in the setting of authenticated key exchange (AKE) protocols, and develop two new strong security models for two different threat models. We show that both of these security models can be satisfied, by proposing two concrete protocol constructions and proving they are secure in the models. Our work leads to crucial insights on how post-compromise security can (and cannot) be achieved, paving the way for applications in other domains.
Authenticated key exchange protocols are ubiquitous in modern-day life. They are used to secure numerous types of data exchange, ranging from online banking to instant messaging conversations. In this thesis, we extend the state of the art for authenticated key exchange security, following the three themes of realistic, strong and provable. First, we tackle the theme of provable security. We develop generic techniques, applicable to a wide range of security models, to assist in proofs of security of cryptographic schemes. Specifically, a "game hopping" proof is a powerful technique to prove strong statements about the security of a protocol. However, the proof technique often involves esoteric and repetitive steps. We demystify the methodology and prove generic theorems to reduce the length and complexity of a wide class of game hopping proofs. Next, we use this new framework to analyse strong and previously unstudied formal security guarantees of authenticated key exchange protocols. These protocols are able to achieve strong security guarantees because they share and update state across sessions. Using our framework, we are able to push the state of the art by defying the folklore of what was previously thought provable of authenticated key exchange protocols. Specifically, it was previously thought that no protocol can achieve a security guarantee about communication with a peer if the peer was already fully compromised. We show that this is not true by formally defining a new concept, which we name post-compromise security. We capture an intuitive "self-healing" property of protocols. We then construct and formally prove protocols can achieve this strong security notion. Finally, we leverage all of this work to analyse realistic protocols. Signal, which is used to encrypt messages in WhatsApp, Facebook Messenger and Google Allo amongst others, is one such protocol we consider. Despite being used by billions of people, Signal was completely unstudied in the academic literature prior to this work. Two reasons for this were that Signal had no documentation at the time and it did not fit into existing models: it shares state across sessions and has over ten different types of key, most of which continually update. Despite its complexity, we are able to use the other work in this thesis to give the first ever analysis and proof of security of Signal. Overall, this thesis aims to bridge the gap between theory and practice in the current state of the art of authenticated key exchange protocols.
Widely used communication and messaging protocols, e.g., TLS 1.3 and Signal, are insecure against an adversary with a quantum computer. We expect that post-quantum security will become mandatory for a new generation of cryptographic protocols in the nearest 10-15 years. The analysis of existing post-quantum secure cryptographic tools for key exchange, encryption and message authentication based on hard problems in codes, lattices, ring learning with errors and elliptic curve isogenies revealed their advantages and drawbacks. In particular, we conclude, that the main threat to communication and messaging protocols is only pre-quantum security of currently used Diffie-Hellman key exchange protocols. We summarize efficiency and safety results for each class of post-quantum cryptographic schemes and present an experimental implementation of isogeny-based Diffie-Hellman-like key exchange protocol as an illustration of their applicability.
This thesis aims to facilitate the deployment of advanced cryptographic primitives in the real world. It does so by designing and implementing post-quantum algorithms on electronic travel documents, and multi-party computation (MPC) on smart meters. We also introduce a novel pairing-based key-and-message-homomorphic (KMHE) scheme for more efficient outsourced MPC. First, we present PQ-EAC, a post-quantum secure replacement for the Extended Access Control protocol used in electronic machine-readable travel documents (eMRTDs). By substituting Diffie-Hellman key exchange with post-quantum key encapsulation mechanisms, we design eight protocol variants offering different trade-offs between security and efficiency. Our implementation on an ARM SC300 chip demonstrates runtimes of under two seconds at typical data rates, confirming the practical feasibility of migrating eMRTDs to post-quantum security. Second, we develop the first fully privacy-preserving power flow analysis (PFA) based on MPC. By adopting a Cartesian formulation of Newton's method and exploiting sparsity, we create an efficient MPC implementation that enables smart grid operations without compromising prosumer privacy. Our benchmarks show that for small grids with low network latency, online computation completes in under 30 seconds, demonstrating that MPC-based PFA is practical for preventive smart grid applications.Third, we present a new KMHE scheme based on bilinear pairings that enables practical rerandomizable garbling schemes (RGS). Our construction reduces garbled gate size by 98.99% (from 133.43 MB to 1.35 MB) and garbling time by 99.998% (from 33 minutes to 0.04 seconds) compared to previous BHHO-based approaches. This four-order-of-magnitude improvement makes the SCALES protocol practically feasible for the first time, enabling constant-round outsourced computation with security against adaptive adversaries.Together, these contributions demonstrate that advanced cryptographic techniques can be made practical through careful protocol design, algorithmic optimization, and implementation strategies tailored to specific application constraints.
Due to development in quantum computing, we need to create and implement new cryptographic protocols, which are resistant to attacks using a quantum computer, in all practical cases. Last years humans became using messengers to transfer far more important information than earlier, so it is necessary to create new post-quantum secure messaging protocols for peer-to-peer and group communications. In this article, we describe needed security properties, existing ways for the creation of group chats, and our suggestions. We described ways and needed primitives for the creation of a group key establishment scheme based on isogenies of elliptic curves. We describe such protocol as an extended Double Ratchet protocol.