A formal Security Analysis of the Signal Messaging Protocol

Add to your list(s) Download to your calendar using vCal

• Luke Garratt (University of Oxford)
• Thursday 23 February 2017, 11:00-12:00
• Computer Science, The Sloman Lounge (UG).

If you have a question about this talk, please contact Andreea Radu.

Signal is a new messaging protocol with end-to-end encryption, used by over 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 to first define 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 long-term 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.

This talk is part of the Computer Security Seminars series.

This talk is included in these lists:

• Computer Science Departmental Series
• Computer Science Distinguished Seminars
• Computer Science, The Sloman Lounge (UG)
• Computer Security Seminars
• computer sience

Note that ex-directory lists are not shown.