University of Birmingham > Talks@bham > Computer Security Seminars > A formal Security Analysis of the Signal Messaging Protocol

A formal Security Analysis of the Signal Messaging Protocol

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

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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


Talks@bham, University of Birmingham. Contact Us | Help and Documentation | Privacy and Publicity.
talks@bham is based on from the University of Cambridge.