On the Theory and Practice of Modern Secure Messaging

Billions of people now have conversations daily over the Internet. A large portion of this communication takes place via secure messaging protocols that offer "end-to-end encryption'" guarantees and resilience to compromise like the widely-used Double Ratchet protocol of Perrin and Marlinspike. This thesis explores secure messaging from a cryptographic perspective in both the analysis and improvement of existing messaging solutions as well as the design of protocols with new security and efficiency characteristics.The first half of the thesis considers communication between two parties. We first draw our attention to the impending threat of quantum computers on Diffie-Hellman-based key exchange protocols, and in particular on the widely used X3DH key exchange protocol of Perrin and Marlinspike. We propose a new deniable authenticated key exchange protocol, K-Waay, that is based on the relatively conservative plain learning-with-errors (LWE) assumption and is faster than previous proposals. We then consider active attack detection to ensure parties can detect if and when they have been compromised and impersonated by an adversary, even if messages can be delivered out-of-order like in the Double Ratchet protocol. We consider both in-band and out-of-band detection (the latter offering better security but being less convenient for users) and prove formally that immediate active attack detection is sometimes inherently expensive but, despite this, a relaxed yet meaningful notion of active attack detection can be achieved practically.The second half of this thesis then deals with communication between a dynamic group of parties. Firstly, we formalise the group administration problem where a (dynamic) portion of a given group is entrusted with additional privileges: we identify and formalise their core role of enforcing access control. We propose two protocols extending the continuous group key agreement methodology underpinning the recent IETF Messaging Layer Security (MLS) standard, and demonstrate experimentally that administration can be achieved with very little overhead for MLS. Finally, we formalise the practical Sender Keys group messaging protocol used by WhatsApp and Signal (which in fact relies on two-party communication at its core) and prove in a new security model that the core protocol structure is sound. Through our formalisation, we report some drawbacks of Sender Keys, especially in terms of its resilience to state compromise, and propose some tweaks to overcome them using standard cryptographic primitives, each of which either incurs little overhead or in fact improves practical efficiency.