Douglas Stebila

A formal security analysis of the Signal messaging protocol

Signal protocol

Abstract

The Signal protocol is a cryptographic messaging protocol that provides end-to-end encryption for instant messaging in WhatsApp, Wire, and Facebook Messenger among many others, serving well over 1 billion active users. Signal includes several uncommon security properties (such as “future secrecy” or “post-compromise security”), enabled by a novel technique called ratcheting in which session keys are updated with every message sent.

We conduct a formal security analysis of Signal's initial extended triple Diffie-Hellman (X3DH) key agreement and Double Ratchet protocols as a multi-stage authenticated key exchange protocol. We extract from the implementation a formal description of the abstract protocol, and define a security model which can capture the ratcheting key update structure as a multi-stage model where there can be a tree of stages, rather than just a sequence. We then prove the security of Signal's key exchange core in our model, demonstrating several standard security properties. We have found no major flaws in the design, and hope that our presentation and results can serve as a foundation for other analyses of this widely adopted protocol.

Keywords: messaging, post-compromise security, Signal, future secrecy, authenticated key exchange, provable security, multi-stage key exchange

Reference

Katriel Cohn-Gordon, Cas Cremers, Benjamin Dowling, Luke Garratt, Douglas Stebila. A formal security analysis of the Signal messaging protocol. In Proc. IEEE European Symposium on Security and Privacy (EuroS&P) 2017. IEEE, April 2017. © IEEE.

Download

Media

• 2016-11-14: Heise: Gute Noten für Signals Krypto-Protokoll.
• 2016-11-10: Threat Post: Signal audit reveals protocol cryptographically sound.
• 2016-11-08: Cyberscoop: Signal’s protocol gets glowing reviews in first security audit.
• 2016-11-08: The Register: 'Trust it': Results of Signal's first formal crypto analysis are in.

BibTeX

@inproceedings{EuroSP:CCDGS17,
 	Author = {Katriel Cohn-Gordon and Cas Cremers and Benjamin Dowling and Luke Garratt and Douglas Stebila},
 	Booktitle = {Proc. {IEEE} European Symposium on Security and Privacy (EuroS\&P) 2017},
 	Month = {April},
 	Publisher = {IEEE},
 	Title = {A formal security analysis of the {S}ignal messaging protocol},
 	Year = {2017}
 }

Funding

• Australian Research Council (ARC) Discovery Project grant DP130104304
• Natural Sciences and Engineering Research Council of Canada (NSERC) Discovery grant RGPIN-2016-05146
• NSERC Discovery Accelerator Supplement grant RGPIN-2016-05146
• Oxford CDT in Cyber Security