Visualizing the Signal Double Ratchet

An interactive, animated demo of the self-healing protocol.

First, a Secure Handshake (X3DH)

Before any messages are sent, Signal establishes a shared secret using X3DH. This lets Alice set up a secure channel even if Bob is offline.

  1. Bob uploads a "prekey bundle" to the server (his Identity Key, a Signed Prekey, and One-Time Prekeys).
  2. Alice fetches this bundle, generates her own keys, and performs 3-4 Diffie-Hellman (DH) calculations.
  3. The results are combined to create the very first Root Key.

This simulation starts after X3DH is complete. Alice and Bob now share their first Root Key and are ready to chat.

Alice

DH_A_1
RK_1
CK_S_A_1
CK_R_A_1

Watch the packets fly!

Colored boxes = keys
Watch them animate!

Bob

DH_B_1
RK_1
CK_S_B_1
CK_R_B_1

How It Works

  • Symmetric-key Ratchet: Each message advances the sender's Sending Chain Key. The receiver's Receiving Chain advances to decrypt.
  • DH Ratchet: When someone replies, they generate a new Diffie-Hellman keypair. This creates a new Root Key, which re-seeds both Sending and Receiving Chains.
  • The Result: Forward Secrecy (past messages stay safe) + Post-Compromise Security (future messages heal after a breach).

Event Log

Simulation Ready. It's Alice's turn to talk.

What Makes This Special?

Forward Secrecy

Even if an attacker steals today's keys, they cannot decrypt yesterday's messages. Each message key is derived and then discarded.

Post-Compromise Security

If keys are stolen, the conversation heals itself after a single round-trip. The DH Ratchet introduces fresh entropy from new DH keypairs.

The Future: Post-Quantum Signal

Quantum computers threaten to break today's elliptic-curve cryptography. Signal is ready with PQXDH and the Triple Ratchet:

  • PQXDH: Combines quantum-resistant ML-KEM with the existing X3DH in a hybrid design.
  • Triple Ratchet: Runs both classic (ECDH) and post-quantum (ML-KEM) ratchets in parallel. An attacker must break both systems.
  • Verified From The Start: The new protocol was co-designed with formal verification using tools like ProVerif and F*.

References

Marlinspike, M., & Perrin, T. (2016). The X3DH key agreement protocol. Signal Messenger.
Perrin, T., & Marlinspike, M. (2013). The Double Ratchet algorithm. Signal Messenger.
Dia, D. (2025, October). Project Everest: Building a provably secure HTTPS ecosystem with F*. American University of Beirut.
Pierce, B. C. (1991). A foundational theory of subtyping for dependent type theory. Carnegie Mellon University.
Wadler, P. (2015). Propositions as types. Communications of the ACM, 58(12), 75-84.
Zinzindohoué, J. K., Bhargavan, K., Protzenko, J., & Beurdouche, B. (2017). HACL*: A verified modern cryptographic library. In Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security (pp. 1789-1806). ACM.
Kocher, P. C. (1996). Timing attacks on implementations of Diffie-Hellman, RSA, DSS, and other systems. In Advances in Cryptology — CRYPTO '96 (pp. 104-113). Springer.
Blanchet, B. (n.d.). ProVerif: Cryptographic protocol verifier. https://proverif.inria.fr/
Meier, S., Schmidt, B., Cremers, C., & Basin, D. (n.d.). The TAMARIN prover. https://tamarin-prover.github.io/
Cohn-Gordon, K., Cremers, C., Dowling, B., Garratt, L., & Stebila, D. (2017). A formal security analysis of the Signal messaging protocol. In 2017 IEEE European Symposium on Security and Privacy (EuroS&P) (pp. 451-466). IEEE.
Frosch, C., Mainka, C., Bader, C., Bergsma, F., Schwenk, J., & Holz, T. (2016). On the security of asynchronous group messaging. Ruhr-Universität Bochum.
Shor, P. W. (1994). Algorithms for quantum computation: Discrete logarithms and factoring. In Proceedings 35th Annual Symposium on Foundations of Computer Science (pp. 124-134). IEEE.
Signal Team. (2023, September). Quantum resistance and the Signal protocol. Signal Blog. https://signal.org/blog/
Bos, J., Ducas, L., Kiltz, E., Lepoint, T., Lyubashevsky, V., Schanck, J. M., Schwabe, P., Seiler, G., & Stehlé, D. (2018). CRYSTALS-Kyber: A CCA-secure module-lattice-based KEM. In 2018 IEEE European Symposium on Security and Privacy (EuroS&P) (pp. 353-367). IEEE.
Bindel, N., Brendel, J., Fischlin, M., Goncalves, B., & Stebila, D. (2017). Hybrid key encapsulation mechanisms and authenticated key exchange. In International Conference on Post-Quantum Cryptography (pp. 143-171). Springer.
Connell, G., & Schmidt, R. (2025, October). Signal protocol and post-quantum ratchets. Signal Blog. https://signal.org/blog/
Reed, I. S., & Solomon, G. (1960). Polynomial codes over certain finite fields. Journal of the Society for Industrial and Applied Mathematics, 8(2), 300-304.
Fromherz, A., Erbsen, A., Yoon, N., & Protzenko, J. (2025). hax: Verifying security-critical Rust software using multiple provers. IACR Cryptology ePrint Archive.