The double ratchet: Security notions, proofs, and modularization for the signal protocol

Joël Alwen, Sandro Coretti, Yevgeniy Dodis

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

Signal is a famous secure messaging protocol used by billions of people, by virtue of many secure text messaging applications including Signal itself, WhatsApp, Facebook Messenger, Skype, and Google Allo. At its core it uses the concept of “double ratcheting,” where every message is encrypted and authenticated using a fresh symmetric key; it has many attractive properties, such as forward security, post-compromise security, and “immediate (no-delay) decryption,” which had never been achieved in combination by prior messaging protocols. While the formal analysis of the Signal protocol, and ratcheting in general, has attracted a lot of recent attention, we argue that none of the existing analyses is fully satisfactory. To address this problem, we give a clean and general definition of secure messaging, which clearly indicates the types of security we expect, including forward security, post-compromise security, and immediate decryption. We are the first to explicitly formalize and model the immediate decryption property, which implies (among other things) that parties seamlessly recover if a given message is permanently lost—a property not achieved by any of the recent “provable alternatives to Signal.” We build a modular “generalized Signal protocol” from the following components: (a) continuous key agreement (CKA), a clean primitive we introduce and which can be easily and generically built from public-key encryption (not just Diffie-Hellman as is done in the current Signal protocol) and roughly models “public-key ratchets;” (b) forward-secure authenticated encryption with associated data (FS-AEAD), which roughly captures “symmetric-key ratchets;” and (c) a two-input hash function that is a pseudorandom function (resp. generator with input) in its first (resp. second) input, which we term PRF-PRNG. As a result, in addition to instantiating our framework in a way resulting in the existing, widely-used Diffie-Hellman based Signal protocol, we can easily get post-quantum security and not rely on random oracles in the analysis.

Original languageEnglish (US)
Title of host publicationAdvances in Cryptology – EUROCRYPT 2019 - 38th Annual International Conference on the Theory and Applications of Cryptographic Techniques, Proceedings
EditorsYuval Ishai, Vincent Rijmen
PublisherSpringer-Verlag
Pages129-158
Number of pages30
ISBN (Print)9783030176525
DOIs
StatePublished - Jan 1 2019
Event38th Annual International Conference on the Theory and Applications of Cryptographic Techniques, Eurocrypt 2019 - Darmstadt, Germany
Duration: May 19 2019May 23 2019

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume11476 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference38th Annual International Conference on the Theory and Applications of Cryptographic Techniques, Eurocrypt 2019
CountryGermany
CityDarmstadt
Period5/19/195/23/19

Fingerprint

Modularization
Security Proof
Ratchet
Cryptography
Text messaging
Function generators
Hash functions
Forward Security
Diffie-Hellman
Authenticated Encryption
Pseudorandom Function
Key Agreement
Random Oracle
Public Key Encryption
Formal Analysis
Public key
Hash Function
Thing
Generator
Imply

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Alwen, J., Coretti, S., & Dodis, Y. (2019). The double ratchet: Security notions, proofs, and modularization for the signal protocol. In Y. Ishai, & V. Rijmen (Eds.), Advances in Cryptology – EUROCRYPT 2019 - 38th Annual International Conference on the Theory and Applications of Cryptographic Techniques, Proceedings (pp. 129-158). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11476 LNCS). Springer-Verlag. https://doi.org/10.1007/978-3-030-17653-2_5

The double ratchet : Security notions, proofs, and modularization for the signal protocol. / Alwen, Joël; Coretti, Sandro; Dodis, Yevgeniy.

Advances in Cryptology – EUROCRYPT 2019 - 38th Annual International Conference on the Theory and Applications of Cryptographic Techniques, Proceedings. ed. / Yuval Ishai; Vincent Rijmen. Springer-Verlag, 2019. p. 129-158 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11476 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Alwen, J, Coretti, S & Dodis, Y 2019, The double ratchet: Security notions, proofs, and modularization for the signal protocol. in Y Ishai & V Rijmen (eds), Advances in Cryptology – EUROCRYPT 2019 - 38th Annual International Conference on the Theory and Applications of Cryptographic Techniques, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 11476 LNCS, Springer-Verlag, pp. 129-158, 38th Annual International Conference on the Theory and Applications of Cryptographic Techniques, Eurocrypt 2019, Darmstadt, Germany, 5/19/19. https://doi.org/10.1007/978-3-030-17653-2_5
Alwen J, Coretti S, Dodis Y. The double ratchet: Security notions, proofs, and modularization for the signal protocol. In Ishai Y, Rijmen V, editors, Advances in Cryptology – EUROCRYPT 2019 - 38th Annual International Conference on the Theory and Applications of Cryptographic Techniques, Proceedings. Springer-Verlag. 2019. p. 129-158. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-030-17653-2_5
Alwen, Joël ; Coretti, Sandro ; Dodis, Yevgeniy. / The double ratchet : Security notions, proofs, and modularization for the signal protocol. Advances in Cryptology – EUROCRYPT 2019 - 38th Annual International Conference on the Theory and Applications of Cryptographic Techniques, Proceedings. editor / Yuval Ishai ; Vincent Rijmen. Springer-Verlag, 2019. pp. 129-158 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{d88449c68bac450389713e2ca06a6e3e,
title = "The double ratchet: Security notions, proofs, and modularization for the signal protocol",
abstract = "Signal is a famous secure messaging protocol used by billions of people, by virtue of many secure text messaging applications including Signal itself, WhatsApp, Facebook Messenger, Skype, and Google Allo. At its core it uses the concept of “double ratcheting,” where every message is encrypted and authenticated using a fresh symmetric key; it has many attractive properties, such as forward security, post-compromise security, and “immediate (no-delay) decryption,” which had never been achieved in combination by prior messaging protocols. While the formal analysis of the Signal protocol, and ratcheting in general, has attracted a lot of recent attention, we argue that none of the existing analyses is fully satisfactory. To address this problem, we give a clean and general definition of secure messaging, which clearly indicates the types of security we expect, including forward security, post-compromise security, and immediate decryption. We are the first to explicitly formalize and model the immediate decryption property, which implies (among other things) that parties seamlessly recover if a given message is permanently lost—a property not achieved by any of the recent “provable alternatives to Signal.” We build a modular “generalized Signal protocol” from the following components: (a) continuous key agreement (CKA), a clean primitive we introduce and which can be easily and generically built from public-key encryption (not just Diffie-Hellman as is done in the current Signal protocol) and roughly models “public-key ratchets;” (b) forward-secure authenticated encryption with associated data (FS-AEAD), which roughly captures “symmetric-key ratchets;” and (c) a two-input hash function that is a pseudorandom function (resp. generator with input) in its first (resp. second) input, which we term PRF-PRNG. As a result, in addition to instantiating our framework in a way resulting in the existing, widely-used Diffie-Hellman based Signal protocol, we can easily get post-quantum security and not rely on random oracles in the analysis.",
author = "Jo{\"e}l Alwen and Sandro Coretti and Yevgeniy Dodis",
year = "2019",
month = "1",
day = "1",
doi = "10.1007/978-3-030-17653-2_5",
language = "English (US)",
isbn = "9783030176525",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer-Verlag",
pages = "129--158",
editor = "Yuval Ishai and Vincent Rijmen",
booktitle = "Advances in Cryptology – EUROCRYPT 2019 - 38th Annual International Conference on the Theory and Applications of Cryptographic Techniques, Proceedings",

}

TY - GEN

T1 - The double ratchet

T2 - Security notions, proofs, and modularization for the signal protocol

AU - Alwen, Joël

AU - Coretti, Sandro

AU - Dodis, Yevgeniy

PY - 2019/1/1

Y1 - 2019/1/1

N2 - Signal is a famous secure messaging protocol used by billions of people, by virtue of many secure text messaging applications including Signal itself, WhatsApp, Facebook Messenger, Skype, and Google Allo. At its core it uses the concept of “double ratcheting,” where every message is encrypted and authenticated using a fresh symmetric key; it has many attractive properties, such as forward security, post-compromise security, and “immediate (no-delay) decryption,” which had never been achieved in combination by prior messaging protocols. While the formal analysis of the Signal protocol, and ratcheting in general, has attracted a lot of recent attention, we argue that none of the existing analyses is fully satisfactory. To address this problem, we give a clean and general definition of secure messaging, which clearly indicates the types of security we expect, including forward security, post-compromise security, and immediate decryption. We are the first to explicitly formalize and model the immediate decryption property, which implies (among other things) that parties seamlessly recover if a given message is permanently lost—a property not achieved by any of the recent “provable alternatives to Signal.” We build a modular “generalized Signal protocol” from the following components: (a) continuous key agreement (CKA), a clean primitive we introduce and which can be easily and generically built from public-key encryption (not just Diffie-Hellman as is done in the current Signal protocol) and roughly models “public-key ratchets;” (b) forward-secure authenticated encryption with associated data (FS-AEAD), which roughly captures “symmetric-key ratchets;” and (c) a two-input hash function that is a pseudorandom function (resp. generator with input) in its first (resp. second) input, which we term PRF-PRNG. As a result, in addition to instantiating our framework in a way resulting in the existing, widely-used Diffie-Hellman based Signal protocol, we can easily get post-quantum security and not rely on random oracles in the analysis.

AB - Signal is a famous secure messaging protocol used by billions of people, by virtue of many secure text messaging applications including Signal itself, WhatsApp, Facebook Messenger, Skype, and Google Allo. At its core it uses the concept of “double ratcheting,” where every message is encrypted and authenticated using a fresh symmetric key; it has many attractive properties, such as forward security, post-compromise security, and “immediate (no-delay) decryption,” which had never been achieved in combination by prior messaging protocols. While the formal analysis of the Signal protocol, and ratcheting in general, has attracted a lot of recent attention, we argue that none of the existing analyses is fully satisfactory. To address this problem, we give a clean and general definition of secure messaging, which clearly indicates the types of security we expect, including forward security, post-compromise security, and immediate decryption. We are the first to explicitly formalize and model the immediate decryption property, which implies (among other things) that parties seamlessly recover if a given message is permanently lost—a property not achieved by any of the recent “provable alternatives to Signal.” We build a modular “generalized Signal protocol” from the following components: (a) continuous key agreement (CKA), a clean primitive we introduce and which can be easily and generically built from public-key encryption (not just Diffie-Hellman as is done in the current Signal protocol) and roughly models “public-key ratchets;” (b) forward-secure authenticated encryption with associated data (FS-AEAD), which roughly captures “symmetric-key ratchets;” and (c) a two-input hash function that is a pseudorandom function (resp. generator with input) in its first (resp. second) input, which we term PRF-PRNG. As a result, in addition to instantiating our framework in a way resulting in the existing, widely-used Diffie-Hellman based Signal protocol, we can easily get post-quantum security and not rely on random oracles in the analysis.

UR - http://www.scopus.com/inward/record.url?scp=85065919124&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85065919124&partnerID=8YFLogxK

U2 - 10.1007/978-3-030-17653-2_5

DO - 10.1007/978-3-030-17653-2_5

M3 - Conference contribution

AN - SCOPUS:85065919124

SN - 9783030176525

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 129

EP - 158

BT - Advances in Cryptology – EUROCRYPT 2019 - 38th Annual International Conference on the Theory and Applications of Cryptographic Techniques, Proceedings

A2 - Ishai, Yuval

A2 - Rijmen, Vincent

PB - Springer-Verlag

ER -