A Formal Security Analysis of the Signal Messaging Protocol
- PDF / 3,417,610 Bytes
- 70 Pages / 439.37 x 666.142 pts Page_size
- 6 Downloads / 182 Views
A Formal Security Analysis of the Signal Messaging Protocol Katriel Cohn-Gordon Oxford, UK [email protected]
Cas Cremers CISPA Helmholtz Center for Information Security, Saarbrücken, Germany [email protected]
Benjamin Dowling ETH Zürich, Zurich, Switzerland [email protected]
Luke Garratt Cisco Systems, San Jose, USA [email protected]
Douglas Stebila University of Waterloo, Waterloo, Canada [email protected] Communicated by Hugo Krawczyk Received 8 November 2017 / Revised 4 June 2020
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 multistage 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
K. Cohn-Gordon et al.
1. Introduction Revelations about mass surveillance of communications have made consumers more privacy-aware. In response, scientists and developers have proposed techniques which can provide security for end users even if they do not fully trust the service providers. For example, the popular messaging service WhatsApp was unable to comply with Brazilian government demands for users’ plaintext messages [15] because of its end-toend encryption. Early instant messaging systems did not provide much security. While some systems did encrypt traffic between the user and the service provider, the service provider retained the ability to read the plaintext of users’ messages. Off-the-Record Messaging [16,29] was one of the first security protocols for instant messaging: acting as a plug-in to a variety of instant messaging applications, users could authenticate each other using public keys or a shared secret passphrase and obtain end-to-end confidentiality and integrity. One novel feature of OTR was its fine-grained key freshness: along with each message round trip, users established a fresh ephemeral Diffie–Hellman (DH) shared secret. Since it was not possible to work backward from a later state to an earlier state and decrypt past messages, this technique became known as ratcheting;
Data Loading...
