What formal guarantees should a secure messaging application provide? Do the most widely-used protocols provide them? Can we do better? In this thesis we answer these questions and with them give a formal study of modern secure messaging protocols, which encrypt the personal messages of billions of users. We give definitions and analyses of two protocols: one existing (Signal) and one new (ART). For Signal, we begin by extending and generalising classic computational models, in order to apply them to its complex ratcheting key derivations. With a threat model in mind we also define a security property, capturing strong secrecy and authentication guarantees including a new one which we call "post-compromise security". We instantiate Signal as a protocol in our model, stating its security theorem and sketching a computational reduction. Signal only supports encrypting messages between two devices, and so most implementers have built custom protocols on top of it to support group conversations. These protocols usually provide weaker security guarantees, and in particular usually do not have post-compromise security. We propose a new protocol called ART, whose goal is to bring Signal's strong security properties to conversations with multiple users and devices. We give a design rationale and a precise definition of ART, and again generalise existing computational models in order to formally specify its security properties and sketch a security reduction. ART has enjoyed widespread interest from industry, and we aim to turn it into an open standard for secure messaging. To that end, we have brought it to the IETF and formed a working group called Messaging Layer Security, with representatives from academia as well as Facebook, Google, Twitter, Wire, Cisco and more. Through MLS, we hope to bring ART's strong guarantees to practical implementations across industry. After concluding our analyses we pause for a moment, and start looking towards the future. We argue that for complex protocols like Signal and ART we are reaching the limits of computational methods, and that the future for their analysis lies with symbolic verification tools. To that end we return to the symbolic model and give a number of case studies, in each one showing how a traditional limitation of symbolic models can in fact be seen as a modelling artefact.
| Identifer | oai:union.ndltd.org:bl.uk/oai:ethos.bl.uk:757929 |
| Date | January 2018 |
| Creators | Cohn-Gordon, Katriel |
| Contributors | Rasmussen, Kasper ; Cremers, Cas ; Ryan, Mark |
| Publisher | University of Oxford |
| Source Sets | Ethos UK |
| Detected Language | English |
| Type | Electronic Thesis or Dissertation |
| Source | http://ora.ox.ac.uk/objects/uuid:a6da6196-f216-4d57-9035-72903006197c |
Page generated in 0.0019 seconds