CISPA
Browse

File(s) not publicly available

A Formal Security Analysis of the Signal Messaging Protocol

journal contribution
posted on 2023-11-29, 18:06 authored by Katriel Cohn-Gordon, Cas CremersCas Cremers, Benjamin Dowling, Luke Garratt, Douglas Stebila
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.

History

Preferred Citation

Katriel Cohn-Gordon, Cas Cremers, Benjamin Dowling, Luke Garratt and Douglas Stebila. A Formal Security Analysis of the Signal Messaging Protocol. In: Journal of Cryptology. 2020.

Primary Research Area

  • Algorithmic Foundations and Cryptography

Legacy Posted Date

2020-10-08

Journal

Journal of Cryptology

Open Access Type

  • Unknown

Sub Type

  • Article

BibTeX

@article{cispa_all_3243, title = "A Formal Security Analysis of the Signal Messaging Protocol", author = "Cohn-Gordon, Katriel and Cremers, Cas and Dowling, Benjamin and Garratt, Luke and Stebila, Douglas", journal="{Journal of Cryptology}", year="2020", }

Usage metrics

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC