Top

Journal of Cryptology

Published in:

23-09-2020

A Formal Security Analysis of the Signal Messaging Protocol

Authors: Katriel Cohn-Gordon, Cas Cremers, Benjamin Dowling, Luke Garratt, Douglas Stebila

Published in: Journal of Cryptology | Issue 4/2020

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

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.

previous article Cryptanalysis of OCB2: Attacks on Authenticity and Confidentiality

next article Non-malleable Encryption: Simpler, Shorter, Stronger

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Available only for authorised users

TextSecure v1 was based on OTR; in v2 it migrated to the Axolotl Ratchet and in v3 made some changes to the cryptographic primitives and the wire protocol. Signal is based on TextSecure v3.

The tagged releases of libsignal lag behind the current codebase. The commit hash of the state of the repository as of our reading is listed in the bibliography. Note that there are separate implementations in C, JavaScript and Java; the latter is used by Android mobile apps and is the one we have read most carefully.

The key exchange protocol was previously referred to as TripleDH, from the three Diffie–Hellman (DH) shared secrets always used in the KDF (although in most configurations four shared secrets are used). The name QuadrupleDH has also been used for the variant which includes the long-term/long-term Diffie–Hellman (DH) value, not as might be expected the variant which includes the one-time prekey.

If the initial message from Alice is invalid, Bob will in fact not complete a session. This does not affect our analysis, which considers only secrecy of session keys, but may become important if, e.g., analysing deniability.

Future secrecy means “a leak of keys to a passive eavesdropper will be healed by introducing new Diffie–Hellman (DH) ratchet keys” [60].

A vertex cover of a graph is a set of nodes incident to every edge.

In our model, there are two ephemeral/medium-term pairs: \((\textit{prepk}^{B})^{\textit{ek}^{A}}\) and \((\textit{prepk}^{B})^{\textit{rchk}^{A}_{0}}\). Our security model treats \(\textit{ek}^{A} \) and \(\textit{rchk}^{A}_{0} \) as being revealed by the same query, so one predicate covers both terms.

This is done in practice by reinterpreting the Curve25519 point as an Ed25519 key and computing an EdDSA signature.

The implementation of group messaging is not specified at the protocol layer. If it is implemented using multiple pairwise sessions, its security may follow in a relatively straightforward fashion—however, there are many other possible security properties which might be desired, such as transcript consistency.

J. Alwen, S. Coretti, Y. Dodis, The Double Ratchet: security notions, proofs, and modularization for the Signal protocol, in IACR Cryptology ePrint Archive 2018 (2018), p. 1037. https://eprint.iacr.org/2018/1037

C. Bader, D. Hofheinz, T. Jager, E. Kiltz, Y. Li, Tightly-secure authenticated key exchange, in TCC 2015, Part I, LNCS, vol. 9014. (Springer, Heidelberg, 2015), pp. 629–658MATH

C. Bader, T. Jager, Y. Li, S. Schäge, On the Impossibility of Tight Cryptographic Reductions. Cryptology ePrint Archive, Report 2015/374 (2015). http://eprint.iacr.org/2015/374

C. Ballinger, ChatSecure. https://chatsecure.org/blog/chatsecure-v4-released/ (visited on 01/2017)

M. Bellare, A. Boldyreva, A. Palacio, An uninstantiable random-oracle-model scheme for a hybrid-encryption problem, in Advances in Cryptology-EUROCRYPT 2004 (Springer, 2004), pp. 171–188

M. Bellare, R. Canetti, H. Krawczyk, A modular approach to the design and analysis of authentication and key exchange protocols (extended abstract), in 30th ACM STOC. (ACM Press, 1998), pp. 419–428

M. Bellare, D. Pointcheval, P. Rogaway, Authenticated key exchange secure against dictionary attacks, in EUROCRYPT 2000, LNCS, vol. 1807 (Springer, Heidelberg, 2000), pp. 139–155MATH

M. Bellare, P. Rogaway, Entity authentication and key distribution, in CRYPTO’93., LNCS, vol. 773 (Springer, Heidelberg, 1994), pp. 232–249

M. Bellare, P. Rogaway, Random oracles are practical: a paradigm for designing efficient protocols, in Proceedings of the 1st ACM conference on Computer and communications security (ACM. 1993), pp. 62–73

10.

M. Bellare, A.C. Singh, J. Jaeger, M. Nyayapati, I. Stepanovs, Ratcheted encryption and key exchange: the security of messaging. Cryptology ePrint Archive, Report 2016/1028 (2016). http://eprint.iacr.org/2016/1028

11.

M. Bellare, B.S. Yee, Forward-security in private-key cryptography, in CT-RSA 2003, LNCS, vol. 2612 (Springer, Heidelberg, 2003), pp. 1–18MATH

12.

D.J. Bernstein, Curve25519: new Diffie–Hellman speed records, in PKC 2006, LNCS, vol. 3958 (Springer, Heidelberg, 2006), pp. 207–228MATH

13.

D.J. Bernstein, N. Duif, T. Lange, P. Schwabe, B.-Y. Yang, High-speed high-security signatures, in CHES 2011, LNCS, vol. 6917 (Springer, Heidelberg, 2011), pp. 124–142MATH

14.

K. Bhargavan, C. Brzuska, C. Fournet, M. Green, M. Kohlweiss, S. Zanella-Béguelin, Downgrade resilience in key-exchange protocols, in 2016 IEEE Symposium on Security and Privacy (IEEE Computer Society Press, 2016), pp. 506–525

15.

D. Bogado, D. O’Brien, Punished for a Paradox. Mar. 2, 2016. https://www.eff.org/deeplinks/2016/03/punished-forparadox-brazils-facebook (visited on 07/2016)

16.

N. Borisov, I. Goldberg, E. Brewer, Off-the-record communication, or, why not to use PGP, in WPES (ACM, Washington DC, 2004), pp. 77–84

17.

C. Boyd, C. Cremers, M. Feltz, K.G. Paterson, B. Poettering, D. Stebila, ASICS: authenticated key exchange security incorporating certification systems, in ESORICS 2013, LNCS, vol. 8134 (Springer, Heidelberg, 2013), pp. 381–399MATH

18.

J. Brendel, M. Fischlin, F. Günther, C. Janson, PRF-ODH: relations, instantiations, and impossibility results, in CRYPTO 2017, Part III LNCS, vol. 10403 (Springer, Heidelberg, 2017), pp. 651–681MATH

19.

R. Canetti, O. Goldreich, S. Halevi, The random oracle methodology, revisited, in Journal of the ACM (JACM) 51.4 (2004), pp. 557–594MathSciNetCrossRef

20.

R. Canetti, S. Halevi, J. Katz, A forward-secure public-key encryption scheme, in EUROCRYPT 2003, LNCS, vol. 2656 (Springer, Heidelberg, 2003), pp. 255–271MATH

21.

R. Canetti, H. Krawczyk, Analysis of key-exchange protocols and their use for building secure channels, in EUROCRYPT 2001, LNCS, vol. 2045 (Springer, Heidelberg, 2001), pp. 453–474MATH

22.

K. Cohn-Gordon, C. Cremers, Mind the Gap: Where Provable Security and Real-World Messaging Don’t Quite Meet. Cryptology ePrint Archive, Report 2017/982 (2017). http://eprint.iacr.org/2017/982

23.

K. Cohn-Gordon, C. Cremers, L. Garratt, On Post-Compromise Security. (A shorter version of this paper appears at CSF 2016) (2016). http://eprint.iacr.org/2016/221

24.

Conversations. https://conversations.im/ (visited on 07/2016)

25.

C. Cremers, M. Feltz, One-round Strongly Secure Key Exchange with Perfect Forward Secrecy and Deniability. Cryptology ePrint Archive, Report 2011/300 (2011). http://eprint.iacr.org/2011/300

26.

C. Cremers, M. Horvat, S. Scott, T. van der Merwe, Automated analysis and verification of TLS 1.3: 0-RTT, resumption and delayed authentication, in 2016 IEEE Symposium on Security and Privacy (IEEE Computer Society Press, 2016)

27.

J.P. Degabriele, A. Lehmann, K.G. Paterson, N.P. Smart, M. Strefler, On the joint security of encryption and signature in EMV, in CT-RSA 2012, LNCS, vol. 7178 (Springer, Heidelberg, 2012), pp. 116–135MATH

28.

M. Di Raimondo, R. Gennaro, H. Krawczyk, Deniable authentication and key exchange, in ACM CCS 2006 (ACM Press, 2006), pp. 400–409

29.

M. Di Raimondo, R. Gennaro, H. Krawczyk, Secure off-the-record messaging, in WPES. (ACM, Alexandria, VA, 2005), pp. 81–89

30.

B. Dowling, M. Fischlin, F. Günther, D. Stebila, A cryptographic analysis of the TLS 1.3 handshake protocol candidates, in ACM CCS 2015 (ACM Press, 2015), pp. 1197–1210

31.

F. Betül Durak, S. Vaudenay, Bidirectional asynchronous ratcheted key agreement without key-update primitives, in IACR Cryptology ePrint Archive 2018 (2018), p. 889. https://eprint.iacr.org/2018/889

32.

Electronic Frontier Foundation, Secure messaging scorecard (2016). https://www.eff.org/node/82654

33.

Facebook. Messenger Secret Conversations, Technical report (2016). https://fbnewsroomus.files.wordpress.com/2016/07/secret_conversations_whitepaper-1.pdf (visited on 07/2016)

34.

M. Fischlin, F. Gúnther, Multi-stage key exchange and the case of Google’s QUIC protocol, in ACM CCS 2014 (ACM Press, 2014), pp. 1193–1204

35.

T. Frosch, C. Mainka, C. Bader, F. Bergsma, J. Schwenk, T. Holz, How Secure is TextSecure? Cryptology ePrint Archive, Report 2014/904 (2014). http://eprint.iacr.org/2014/904 (Version from April 5, 2016)

36.

T. Frosch, C. Mainka, C. Bader, F. Bergsma, J. Schwenk, T. Holz, How secure is TextSecure?, in 1st IEEE European Symposium on Security and Privacy (IEEE Computer Society Press, 2016)

37.

C. Garman, M. Green, G. Kaptchuk, I. Miers, M. Rushanan, Dancing on the lip of the volcano: chosen ciphertext attacks on Apple iMessage, in Usenix Security 2016 (2016)

38.

Wire Swiss GmbH. Wire Security Whitepaper, in (Aug. 17, 2018). https://wire-docs.wire.com/download/Wire+Security+Whitepaper.pdf (visited on 01/2019)

39.

S. Goldwasser, Y.T. Kalai, Cryptographic assumptions: a position paper, in IACR Cryptology ePrint Archive 2015 (2015), p. 907

40.

M.D. Green, I. Miers, Forward secure asynchronous messaging from puncturable encryption, in 2015 IEEE Symposium on Security and Privacy (IEEE Computer Society Press, 2015), pp. 305–320

41.

M. Hamburg, Ed448-Goldilocks, a New Elliptic Curve. Cryptology ePrint Archive, Report 2015/625 (2015). http://eprint.iacr.org/2015/625

42.

T. Jager, F. Kohlar, S. Schäge, J. Schwenk, On the security of TLS-DHE in the standard model, in CRYPTO 2012, LNCS, vol. 7417 (Springer, Heidelberg, 2012), pp. 273–293MATH

43.

T. Jager, J. Schwenk, J. Somorovsky, On the security of TLS 1.3 and QUIC against weaknesses in PKCS#1 v1.5 Encryption, in ACM CCS 2015 (ACM Press, 2015), pp. 1185–1196

44.

D. Jost, U. Maurer, M. Mularczyk, Efficient ratcheting: almost-optimal guarantees for secure messaging, in IACR Cryptology ePrint Archive 2018 (2018), p. 954. https://eprint.iacr.org/2018/954

45.

N. Kobeissi, K. Bhargavan, B. Blanchet, Automated verification for secure messaging protocols and their implementations: a symbolic and computational approach, in 2nd IEEE European Symposium on Security and Privacy (IEEE Computer Society Press, 2017)

46.

N. Koblitz, A.J. Menezes, The random oracle model: a twenty-year retrospective, in Designs, Codes and Cryptography 77.2-3 (2015), pp. 587–610MathSciNetCrossRef

47.

M. Kohlweiss, U. Maurer, C. Onete, B. Tackmann, D. Venturi, (De-)constructing TLS 1.3, in INDOCRYPT 2015, LNCS, vol. 9462 (Springer, Heidelberg, 2015), pp. 85–102

48.

H. Krawczyk, Cryptographic extraction and key derivation: the HKDF scheme, in CRYPTO 2010, LNCS, vol. 6223 (Springer, Heidelberg, 2010), pp. 631–648MATH

49.

H. Krawczyk, HMQV: a high-performance secure Diffie–Hellman protocol, in CRYPTO 2005, LNCS, vol. 3621 (Springer, Heidelberg, 2005), pp. 546–566MATH

50.

C. Kudla, K.G. Paterson, Modular security proofs for key agreement protocols, in ASIACRYPT 2005, LNCS, vol. 3788 (Springer, Heidelberg, 2005), pp. 549–565MATH

51.

B.A. LaMacchia, K. Lauter, A. Mityagin, Stronger security of authenticated key exchange, in ProvSec 2007, LNCS, vol. 4784 (Springer, Heidelberg, 2007), pp. 1–16MATH

52.

A. Langley. Pond. (2014). https://pond.imperialviolet.org/ (visited on 06/22/2015)

53.

X. Li, J. Xu, Z. Zhang, D. Feng, H. Hu, Multiple handshakes security of TLS 1.3 candidates, in 2016 IEEE Symposium on Security and Privacy. (IEEE Computer Society Press, 2016), pp. 486–505

54.

libsignal-protocol-java. GitHub repository, commit hash 4a7bc1667a68c1d8e6af0151be30b84b94fd1e38 (2016). https://github.com/WhisperSystems/libsignal-protocol-java (visited on 07/2016)

55.

M. Marlinspike, Advanced Cryptographic Ratcheting. Blog. 2013. https://whispersystems.org/blog/advanced-ratcheting/ (visited on 07/2016)

56.

A. Menezes, B. Ustaoglu, On reusing ephemeral keys in Diffie–Hellman key agreement protocols, in Int. J. Appl. Cryptol. 2.2 (2010), pp. 154–158MathSciNetCrossRef

57.

V. Moscaritolo, G. Belvin, P. Zimmermann, Silent Circle Instant Messaging Protocol Specification. Technical report Archived from the original. Dec. 5, 2012. https://web.archive.org/web/20150402122917/, https://silentcircle.com/sites/default/themes/silentcircle/assets/downloads/SCIMP_paper.pdf (visited on 07/2016)

58.

T. Okamoto, D. Pointcheval, The Gap-problems: a new class of problems for the security of cryptographic schemes, in PKC 2001, LNCS, vol. 1992 (Springer, Heidelberg, 2001), pp. 104–118MATH

59.

K.G. Paterson, J.C.N. Schuldt, M. Stam, S. Thomson, On the joint security of encryption and signature, Revisited, in ASIACRYPT 2011, LNCS, vol. 7073 (Springer, Heidelberg, 2011), pp. 161–178MATH

60.

T. Perrin, Double Ratchet Algorithm. GitHub wiki (2016). https://github.com/trevp/double_ratchet/wiki (visited on 07/22/2016)

61.

T. Perrin, The XEdDSA and VXEdDSA Signature Schemes. Specification (2016). https://whispersystems.org/docs/specifications/xeddsa/ (visited on 07/2016)

62.

T. Perrin, M. Marlinspike, The Double Ratchet Algorithm. Specification (2016). https://whispersystems.org/docs/specifications/doubleratchet/ (visited on 01/2017)

63.

T. Perrin, M. Marlinspike, The X3DH Key Agreement Protocol. Specification (2016). https://whispersystems.org/docs/specifications/x3dh/ (visited on 01/2017)

64.

B. Poettering, P. Rösler, Towards bidirectional ratcheted key exchange, in Advances in Cryptology—CRYPTO 2018—38th Annual International Cryptology Conference, Santa Barbara, CA, USA, August 19–23, 2018, Proceedings, Part I, Lecture Notes in Computer Science, vol. 10991 (Springer, 2018), pp. 3–32. ISBN:978-3-319-96883-4. https://doi.org/10.1007/978-3-319-96884-15C_1

65.

J. Reardon, D. Basin, S. Capkun, SoK: secure data deletion, in 2013 IEEE Symposium on Security and Privacy (SP), (2013), pp. 301–315

66.

E. Rescorla, The Transport Layer Security (TLS) Protocol Version 1.3. Internet-Draft draft-ietf-tls-tls13–14 (2016). http://www.ietf.org/internet-drafts/draft-ietf-tls-tls13-14.txt

67.

P. Rogaway, Authenticated-encryption with associated-data, in ACM CCS 2002 (ACM Press, 2002), pp. 98–107

68.

P. Rösler, C. Mainka, J. Schwenk, More is less: on the end-to-end security of group chats in Signal, WhatsApp, and Threema, in 2018 IEEE European Symposium on Security and Privacy, EuroS&P 2018, (London, UK, April 24–26), 2018 (IEEE, 2018), pp. 415–429. ISBN:978-1-5386-4228-3. https://doi.org/10.1109/EuroSP.2018.00036

69.

A. Straub, OMEMO Encryption. Oct. 25, 2015. https://conversations.im/xeps/multi-end.html (visited on 07/2016)

70.

N. Unger, S. Dechand, J. Bonneau, S. Fahl, H. Perl, I. Goldberg, M. Smith, SoK: secure messaging, in 2015 IEEE Symposium on Security and Privacy (IEEE Computer Society Press, 2015), pp. 232–249

71.

N. Unger, I. Goldberg, Deniable key exchanges for secure messaging, in ACM CCS 2015 (ACM Press, 2015), pp. 1211–1223

72.

WhatsApp, WhatsApp Encryption Overview. Technical report (2016). https://www.whatsapp.com/security/WhatsApp-Security-Whitepaper.pdf (visited on 07/2016)

Title: A Formal Security Analysis of the Signal Messaging Protocol
Authors: Katriel Cohn-Gordon
Cas Cremers
Benjamin Dowling
Luke Garratt
Douglas Stebila
Publication date: 23-09-2020
Publisher: Springer US
Published in: Journal of Cryptology / Issue 4/2020
Print ISSN: 0933-2790
Electronic ISSN: 1432-1378
DOI: https://doi.org/10.1007/s00145-020-09360-1

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Other articles of this Issue 4/2020

-Secure Multiparty Computation without an Honest Majority and the Best of Both Worlds

Cryptanalysis of OCB2: Attacks on Authenticity and Confidentiality

Adaptively Secure Non-interactive CCA-Secure Threshold Cryptosystems: Generic Framework and Constructions

Non-malleable Encryption: Simpler, Shorter, Stronger

Foundations of Fully Dynamic Group Signatures

Joint State Composition Theorems for Public-Key Encryption and Digital Signature Functionalities with Local Computation

Premium Partner