Metadata only
Date
2020-10Type
- Journal Article
Citations
Cited 24 times in
Web of Science
Cited 26 times in
Scopus
ETH Bibliography
yes
Altmetrics
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 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. © International Association for Cryptologic Research 2020. Show more
Publication status
publishedExternal links
Journal / series
Journal of CryptologyVolume
Pages / Article No.
Publisher
SpringerOrganisational unit
09653 - Paterson, Kenneth / Paterson, Kenneth
More
Show all metadata
Citations
Cited 24 times in
Web of Science
Cited 26 times in
Scopus
ETH Bibliography
yes
Altmetrics