Paper 2016/1013

A Formal Security Analysis of the Signal Messaging Protocol

Katriel Cohn-Gordon, Cas Cremers, Benjamin Dowling, Luke Garratt, and Douglas Stebila

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.

Note: Fix omission in description of initial X3DH handshake, reorganize figures for improved presentation. Full list of changes in Appendix D.

Metadata
Available format(s)
PDF
Category
Cryptographic protocols
Publication info
Published elsewhere. Major revision. IEEE EuroS&P 2017
Keywords
protocolsmessagingpost-compromise securitySignalfuture secrecyauthenticated key exchangeprovable securitymulti-stage key exchange
Contact author(s)
dstebila @ uwaterloo ca
History
2019-07-04: last of 5 revisions
2016-10-27: received
See all versions
Short URL
https://ia.cr/2016/1013
License
Creative Commons Attribution
CC BY

BibTeX

@misc{cryptoeprint:2016/1013,
      author = {Katriel Cohn-Gordon and Cas Cremers and Benjamin Dowling and Luke Garratt and Douglas Stebila},
      title = {A Formal Security Analysis of the Signal Messaging Protocol},
      howpublished = {Cryptology ePrint Archive, Paper 2016/1013},
      year = {2016},
      note = {\url{https://eprint.iacr.org/2016/1013}},
      url = {https://eprint.iacr.org/2016/1013}
}
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.