Post-compromise security and the Signal protocol
- 14:00 28th October 2016 ( week 3, Michaelmas Term 2016 )Tony Hoare Room, Robert Hooke Building
Signal is a new messaging protocol with end-to-end encryption, likely used by up to a billion people through its implementations in WhatsApp, Facebook Messenger and Google Allo. Despite this massive uptake, Signal has seen little security analysis; challenges include the complex, stateful design involving over ten different types of key, the lack of documentation or specification, and the novelty of some of its claimed properties.
We performed a formal security analysis of Signal, proving it secure in a game-based model. This required us first to figure out what Signal *is*, which meant working backwards to a specification from the open-source implementation. We also had to work out which security properties we think it was intended to achieve, which include a form of post-compromise security (PCS). PCS is a recently-formalised property encoding the inability of an attacker to impersonate someone even *after* stealing their key. There is much more to be done, however, and I'll talk about some of the interesting research questions that are still left open.
Speaker bio
Katriel is a DPhil student from the first year of the Cyber Security CDT at Oxford, studying practical security protocols under the watchful eye of Professor Cas Cremers. He is interested in formal analysis of the protocols underlying the modern Internet, including TLS and the web public key infrastructure. He studied mathematics at Cambridge University before moving to postgraduate study at Oxford, and has worked with Google's fuzzing team as well as various less-interesting financial institutions.Share this:
