Generic Signal Messaging Protocol: Specification and Implementation

About

The (original) Signal protocol is an open source secure messaging protocol that provides end-to-end authenticated encryption with forward security, post-compromise security, asynchronicity and many other appealing security advantages. The protocol is extensively deployed and secures the daily communication of billions of users via popular (mobile as well as desktop) messaging applications such as Signal (originally TextSecure), WhatsApp, Google Allo, Facebook Messenger, Skype, etc.

The Signal protocol (strictly speaking its core component, the double ratchet algorithm) is formally analyzed and abstracted in the paper “The Double Ratchet: Security Notions, Proofs, and Modularization for the Signal Protocol” by Joël Alwen, Sandro Coretti and Yevgeniy Dodis. The paper proposes a decomposition of the double ratchet algorithm into multiple generic cryptographic modules. The modularization enables customization of the algorithm using different instances of the modules, which naturally leads to post-quantum variants of the Signal protocol by employing quantum-safe module instances.

The implementation of the generic Signal protocol here follows the modularization and is provided as a C library.

Specification

In [1] it is described how the generic Signal protocol can be decomposed into continuous key agreement (CKA), PRF-PRNG (PRGF), authenticated encryption with associated data (AEAD) and PRG, as well as how to construct CKA from key encapsulation mechanism (KEM) and PRGF from HKDF.

[2] describes a standard construction of HKDF from HMAC.

[3] mentions the canonical “encrypt-then-MAC” construction of AEAD from SKE and HMAC.

By definition there exists a trivial construction of PRG from PRF, namely PRG(k) = PRF(k,0) | PRF(k,1) | PRF(k,2) | ....

References

1. Joël Alwen, Sandro Coretti and Yevgeniy Dodis, “The Double Ratchet: Security Notions, Proofs, and Modularization for the Signal Protocol”.
2. H. Krawczyk and P. Eronen, “HMAC-based Extract-and-Expand Key Derivation Function (HKDF)” (RFC 5869).
3. D. McGrew, “An Interface and Algorithms for Authenticated Encryption” (RFC 5116).

Implementation

The C implementation follows the specification of the modularization.

Refer to README.md in code archive for details about the usage as well as the functionality of the library.

Downloads

• 2019.04.21: Version 0.1.0

Release Notes

• 0.1.0: basic support for the generic Signal protocol as well as the modules and their instances including:
  • CKA (compressed DH with Curve25519, compressed Frodo[640,976,1344], KEM-based),
  • PRGF (HKDF-based),
  • PRG (PRF-based),
  • AEAD (AES-[128,192,256]-SIV, SKE-HMAC-based),
  • KEM (DH with Curve25519, simplified DH with Curve25519, Frodo[640,976,1344], simplified Frodo[640,976,1344]),
  • HKDF (SHA-[256,512], HMAC-based),
  • HMAC (SHA-[256,512]),
  • PRF (SHA-[256,512]),
  • SKE (AES-[128,192,256]-CBC).

Future Features

• libsignal-compatible interfaces.
• Complete documentations.
• Support for more post-quantum libraries.

Dependencies

• Botan: C++ library of cryptographic primitives, with FFI for C
• FrodoKEM: C Implementation of FrodoKEM, a post-quantum KEM scheme whose security derives from the learning with errors problem

Contributors

• Yi Tang