Cryptology ePrint Archive: Report 2016/1013

A Formal Security Analysis of the Signal Messaging Protocol

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

Abstract: Signal is a new security protocol and accompanying app that provides end-to-end encryption for instant messaging. The core protocol has recently been adopted by WhatsApp, Facebook Messenger, and Google Allo among many others; the first two of these have at least 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. Despite its importance and novelty, there has been little to no academic analysis of the Signal protocol.

We conduct the first security analysis of Signal's Key Agreement and Double Ratchet as a multi-stage 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. We then prove the security of Signal's 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 starting point for other analyses of this widely adopted protocol.

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

Original Publication (with major differences): IEEE EuroS&P 2017

Date: received 25 Oct 2016, last revised 10 Nov 2017

Contact author: cas cremers at cs ox ac uk

Available format(s): PDF | BibTeX Citation

Note: Update to V2.0.

Version: 20171110:111419 (All versions of this report)

Short URL: ia.cr/2016/1013

Discussion forum: Show discussion | Start new discussion


[ Cryptology ePrint archive ]