Documentation / The Signal protocol

The Signal protocol

Model classical X3DH and three Double Ratchet messages, then investigate checks, trust assumptions and later compromise.

For running these models and interpreting trace excerpts, see Reproducing the examples.

This guide models the classical X3DH handshake and three alternating Double Ratchet messages. The Signal specifications also describe newer post-quantum constructions; this example does not model the entire current Signal application. Its purpose is to examine how key authentication, signature checks and later compromise affect a small exchange.

Security Goals

Signal aims to provide message confidentiality, mutual authentication and protection across key compromise. Each participant maintains long-term identity keys and short-lived ephemeral keys. Identity keys authenticate session establishment; ephemeral keys contribute to message-key evolution. This separation supports two additional goals:

• Forward-secure authenticated key exchange. Revealing long-term identity keys after session establishment should not reveal earlier message contents.¹

• Per-message forward secrecy and post-compromise security. A state compromise should expose only a bounded range of messages, and later uncompromised ratchet steps should restore protection.²

Signal also supports asynchronous session establishment. Alice can establish a session and send a message while Bob is offline. Bob publishes pre-generated key material to a server, allowing Alice to complete the initial key exchange without a live response.

The model omits skipped-message storage, counters, out-of-order delivery and explicit key erasure. Its final compromise reveals only the named identity keys, not the whole device state.

Principals

The model first defines Signal’s initial key exchange and then a three-message exchange using the Double Ratchet.

Modeling the Key Exchange

In the complete X3DH exchange (Modeling the Key Exchange), Alice derives four Diffie–Hellman secrets:

1. Alice’s long-term private key with Bob’s signed pre-key, which Bob generates in advance, signs with his identity key and uploads to the server;

2. Alice’s new ephemeral private key with Bob’s long-term public key;

3. Alice’s ephemeral private key with Bob’s signed pre-key; and

4. Alice’s ephemeral private key with Bob’s one-time pre-key, which Bob generates in advance and uploads without an individual signature.³

The four values are combined into a master secret. Alice can include an encrypted message with the handshake because every value she needs is available from the server. The model begins with Alice’s identity key and Bob’s identity, signed pre-key and one-time pre-key:

attacker[active]
principal Alice[
		knows private alongterm
		galongterm = PUBKEY(alongterm)
	]

principal Bob[
		knows private blongterm, bs
		generates bo
		gblongterm = PUBKEY(blongterm)
		gbs = PUBKEY(bs)
		gbo = PUBKEY(bo)
		gbssig = SIGN(blongterm, gbs)
	]

The model declares the signed pre-key bs with knows because it is shared across sessions. It declares the one-time pre-key bo with generates because each session consumes a distinct value. These declarations reproduce the two key lifetimes under Verifpal’s session model (Sessions and Execution Histories).

Alice receives Bob’s public bundle, verifies the signed pre-key and derives amaster:

Bob -> Alice: [gblongterm], gbssig, gbs, gbo
principal Alice[
		_ = SIGNVERIF(gblongterm, gbs, gbssig)?
		generates ae1
		gae1 = PUBKEY(ae1)
		amaster = HASH(DH_KEX(gbs, alongterm), DH_KEX(gblongterm, ae1), DH_KEX(gbs, ae1), DH_KEX(gbo, ae1))
	]

The checked SIGNVERIF appears before any use of gbs. A failed signature therefore stops Alice before key derivation, as required by X3DH. The anonymous output _ indicates that only the success or failure matters.

Modeling Messages and the Double Ratchet

After the handshake, authentication derives from the master secret, while evolving ephemeral secrets refresh message confidentiality. Signal’s Double Ratchet combines these sources as follows:

principal Alice[
		generates m1, ae2, n_e1
		gae2 = PUBKEY(ae2)
		akshared1 = DH_KEX(gbs, ae2)
		arkab1, ackab1 = HKDF(amaster, akshared1, nil)
		akenc1 = HKDF(nil, MAC(ackab1, nil), nil)
		e1 = AEAD_ENC(akenc1, n_e1, m1,
			HASH(galongterm, gblongterm, gae2))
	]
Alice -> Bob: [galongterm], gae1, gae2, n_e1, e1

Alice generates the ephemeral key pair (ae2, gae2) and derives akshared1. The root-key step passes the previous root value as the HKDF salt and the fresh Diffie–Hellman secret as input key material. It produces a new root key arkab1 and chain key ackab1. A second derivation produces the message key akenc1. The message key thus depends on both the authenticated master secret and new ephemeral material.

The guards on gblongterm and galongterm model mutual pre-authentication of the identity keys, such as out-of-band comparison of Signal safety numbers. The values remain visible but cannot be replaced in transit.

Alice encrypts m1 as e1. Its associated data contains both identity keys and the header’s ratchet public key. This binds the ciphertext to the session. The identity keys use the same ordering in both message directions; the ratchet key identifies the current header. Each message also carries its own generated nonce, which travels beside the ciphertext because Bob needs it to decrypt (Nonces and Nonce Reuse). The Double Ratchet specification permits several nonce strategies, including a random transmitted nonce when message keys are used once.⁴ This model chooses a fresh transmitted nonce. It does not test any implementation's nonce-generation procedure.

Bob derives the same master secret and message key, then checks authenticated decryption:

principal Bob[
		bmaster = HASH(DH_KEX(galongterm, bs), DH_KEX(gae1, blongterm), DH_KEX(gae1, bs), DH_KEX(gae1, bo))
	]

principal Bob[
		bkshared1 = DH_KEX(gae2, bs)
		brkab1, bckab1 = HKDF(bmaster, bkshared1, nil)
		bkenc1 = HKDF(nil, MAC(bckab1, nil), nil)
		m1_d = AEAD_DEC(bkenc1, n_e1, e1,
			HASH(galongterm, gblongterm, gae2))?
	]

Bob uses the opposite half of each key pair. Diffie–Hellman commutativity makes his four inputs equivalent to Alice’s (Public Keys and Key Exchange).

For the reply, Bob generates a new ratchet key pair and mixes its Diffie–Hellman secret with the previous root key. He encrypts m2 under the resulting message key:

principal Bob[
		generates m2, be, n_e2
		gbe = PUBKEY(be)
		bkshared2 = DH_KEX(gae2, be)
		brkba2, bckba2 = HKDF(brkab1, bkshared2, nil)
		bkenc2 = HKDF(nil, MAC(bckba2, nil), nil)
		e2 = AEAD_ENC(bkenc2, n_e2, m2,
			HASH(galongterm, gblongterm, gbe))
	]
Bob -> Alice: gbe, n_e2, e2

After decrypting Bob’s reply, Alice advances the ratchet again and sends m3:

principal Alice[
		akshared2 = DH_KEX(gbe, ae2)
		arkba2, ackba2 = HKDF(arkab1, akshared2, nil)
		akenc2 = HKDF(nil, MAC(ackba2, nil), nil)
		m2_d = AEAD_DEC(akenc2, n_e2, e2,
			HASH(galongterm, gblongterm, gbe))?
	]

principal Alice[
		generates m3, ae3, n_e3
		gae3 = PUBKEY(ae3)
		akshared3 = DH_KEX(gbe, ae3)
		arkab3, ackab3 = HKDF(arkba2, akshared3, nil)
		akenc3 = HKDF(nil, MAC(ackab3, nil), nil)
		e3 = AEAD_ENC(akenc3, n_e3, m3,
			HASH(galongterm, gblongterm, gae3))
	]
Alice -> Bob: gae3, n_e3, e3

principal Bob[
		bkshared3 = DH_KEX(gae3, be)
		brkab3, bckab3 = HKDF(brkba2, bkshared3, nil)
		bkenc3 = HKDF(nil, MAC(bckab3, nil), nil)
		m3_d = AEAD_DEC(bkenc3, n_e3, e3,
			HASH(galongterm, gblongterm, gae3))?
	]

After the exchange, phase 1 leaks both long-term private keys but no ephemeral key. This models a later disclosure of both identity keys (Phases):

phase[1]

principal Alice[leaks alongterm]
principal Bob[leaks blongterm]

The completed model contains an authenticated key exchange, three ratcheted messages and a later compromise of both identity keys.

Queries and Analysis

The queries test confidentiality for all three plaintexts and authentication for each ciphertext in its sending direction:

queries[
		confidentiality? m1
		authentication? Alice -> Bob: e1
		confidentiality? m2
		authentication? Bob -> Alice: e2
		confidentiality? m3
		authentication? Alice -> Bob: e3
	]

The initial model produces these verdicts:

Pass ✓ confidentiality? m1  [search exhausted at 2 sessions]
Pass ✓ authentication? Alice -> Bob: e1  [search exhausted at 2 sessions]
Pass ✓ confidentiality? m2  [search exhausted at 2 sessions]
Pass ✓ authentication? Bob -> Alice: e2  [search exhausted at 2 sessions]
Pass ✓ confidentiality? m3  [search exhausted at 2 sessions]
Pass ✓ authentication? Alice -> Bob: e3  [search exhausted at 2 sessions]

Pass ✓ All 6 queries pass.

Verifpal finds no contradiction under the model’s assumptions, and every envelope records that the two-session search was exhausted. This result is consistent with earlier formal analyses of Signal (Kobeissi et al. 2017; Cohn-Gordon et al. 2017). The scope matters: both parties pre-authenticate identity keys, and Alice stops if Bob’s signed pre-key fails verification. The confidentiality queries still pass after both identity private keys leak in phase 1, which is the modeled forward-secrecy result.

The first variant removes ? from Alice’s SIGNVERIF. Alice now continues after an invalid signed pre-key:

Fail ✗ confidentiality? m1
Attack trace:
| 1. Attacker constructs PUBKEY(nil).
| 2. Attacker replaces gbs#2, gbo#2 (sent by Bob#2 to Alice#2) with
| PUBKEY(nil), PUBKEY(nil). (gbs#2 was PUBKEY(bs);
| gbo#2 was PUBKEY(bo#2))
| 3. Attacker observes e1#2 on the wire.
| 4. Attacker is handed alongterm by a leaks declaration.
| 5. Attacker constructs DH_KEX(PUBKEY(nil), alongterm).
| 6. Attacker observes gae1#2 on the wire.
| 7. Attacker is handed blongterm by a leaks declaration.
| 8. Attacker constructs DH_KEX(gae1#2, blongterm).
| 9. Attacker constructs DH_KEX(gae1#2, nil).
| 10. Attacker constructs amaster#2.
| 11. Attacker observes gae2#2 on the wire.
| 12. Attacker constructs akshared1#2.
| 13. Attacker constructs ackab1#2.
| 14. Attacker constructs MAC(ackab1#2, nil).
| 15. Attacker constructs akenc1#2.
| 16. Attacker observes n_e1#2 on the wire.
| 17. Attacker opens e1#2 with akenc1#2 and n_e1#2, obtaining m1#2.
> m1#2 (m1#2) is obtained by Attacker.
Pass ✓ authentication? Alice -> Bob: e1#2  [search exhausted at 2 sessions]
Pass ✓ confidentiality? m2  [search exhausted at 2 sessions]
Pass ✓ authentication? Bob -> Alice: e2  [search exhausted at 2 sessions]
Pass ✓ confidentiality? m3  [search exhausted at 2 sessions]
Pass ✓ authentication? Alice -> Bob: e3  [search exhausted at 2 sessions]

Fail ✗ 1 of 6 queries failed.

The missing check exposes m1 in the second session after the phase 1 disclosure. The trace replaces the second run’s signed and one-time pre-keys, so its session-local values carry #2. The attacker reconstructs that run’s master secret from the substituted pre-keys, the observed public keys and the later leaked identity keys, then derives its message key and decrypts its first message.

The session count matters here. At one session this variant returns c0a0c0a0c0a0: the altered exchange prevents the run from reaching all the later leaks needed by this attack. At two sessions, an unmodified run reaches the disclosure of the shared long-term keys while the other supplies the recorded ciphertext. The trace cannot be shortened to a one-session attack simply by removing its suffixes.

The later plaintext queries remain uncontradicted in this variant. The disrupted exchange and its later ratchet steps do not supply a disclosure of those plaintexts in the explored executions. The variant therefore identifies both the property lost and the interval affected by the missing check.

The second variant starts from the unchecked model and also removes the guard from Bob’s identity public key, modeling a session in which Alice did not pre-authenticate that key:

Fail ✗ confidentiality? m1
Attack trace:
| 1. Attacker constructs PUBKEY(nil).
| 2. Attacker replaces gblongterm, gbs, gbo (sent by Bob to
| Alice) with PUBKEY(nil), PUBKEY(nil), PUBKEY(nil).
| (gblongterm was PUBKEY(blongterm); gbs was PUBKEY(bs);
| gbo was PUBKEY(bo))
| 3. Attacker observes e1 on the wire.
| 4. Attacker observes galongterm on the wire.
| 5. Attacker constructs DH_KEX(galongterm, nil).
| 6. Attacker observes gae1 on the wire.
| 7. Attacker constructs DH_KEX(gae1, nil).
| 8. Attacker constructs amaster.
| 9. Attacker observes gae2 on the wire.
| 10. Attacker constructs akshared1.
| 11. Attacker constructs ackab1.
| 12. Attacker constructs MAC(ackab1, nil).
| 13. Attacker constructs akenc1.
| 14. Attacker observes n_e1 on the wire.
| 15. Attacker opens e1 with akenc1 and n_e1, obtaining m1.
> m1 (m1) is obtained by Attacker.
Pass ✓ authentication? Alice -> Bob: e1  [search exhausted at 2 sessions]
Pass ✓ confidentiality? m2  [search exhausted at 2 sessions]

Fail ✗ authentication? Bob -> Alice: e2
Attack trace:
| 1. Attacker constructs PUBKEY(nil).
| 2. Attacker observes galongterm on the wire.
| 3. Attacker constructs DH_KEX(galongterm, nil).
| 4. Attacker observes gae1 on the wire.
| 5. Attacker constructs DH_KEX(gae1, nil).
| 6. Attacker constructs HASH(DH_KEX(galongterm, nil),
| DH_KEX(gae1, nil), DH_KEX(gae1, nil), DH_KEX(gae1, nil)).
| 7. Attacker observes gae2 on the wire.
| 8. Attacker constructs DH_KEX(gae2, nil).
| 9. Attacker constructs HKDF(amaster, akshared1, nil)|1.
| 10. Attacker constructs HKDF(arkab1, akshared1, nil)|2.
| 11. Attacker constructs MAC(ackba2, nil).
| 12. Attacker constructs HKDF(nil, MAC(ackba2, nil), nil)|1.
| 13. Attacker observes n_e2 on the wire.
| 14. Attacker replaces gblongterm, gbs, gbo (sent by Bob to
| Alice) with PUBKEY(nil), PUBKEY(nil), PUBKEY(nil).
| (gblongterm was PUBKEY(blongterm); gbs was PUBKEY(bs);
| gbo was PUBKEY(bo))
| 15. Attacker replaces gbe, e2 (sent by Bob to Alice) with
| PUBKEY(nil), AEAD_ENC(akenc2, n_e2, nil, HASH(galongterm,
| PUBKEY(nil), PUBKEY(nil))). (gbe was PUBKEY(be); e2 was
| AEAD_ENC(bkenc2, n_e2, m2, HASH(galongterm, gblongterm,
| gbe)))
| 16. Alice's AEAD_DEC(akenc2, n_e2, AEAD_ENC(akenc2, n_e2,
| nil, HASH(galongterm, PUBKEY(nil), PUBKEY(nil))),
| HASH(galongterm, PUBKEY(nil), PUBKEY(nil)))? passes —
| the attacker controls one of its inputs.
> e2 (AEAD_ENC(akenc2, n_e2, nil, HASH(galongterm,
PUBKEY(nil), PUBKEY(nil)))), sent by Attacker and not by
Bob, is successfully used in AEAD_DEC(akenc2, n_e2, e2,
HASH(galongterm, gblongterm, gbe))? within Alice's state.
Fail ✗ confidentiality? m3
(Trace omitted: the same forgery of Bob's reply,
after which the attacker follows Alice's next ratchet step
to akenc3 and opens e3)
Pass ✓ authentication? Alice -> Bob: e3  [search exhausted at 2 sessions]
Fail ✗ 3 of 6 queries failed.

Step 2 of the first trace replaces three public keys at once. Goal-directed search derives each replacement independently from the requirement to reconstruct amaster; it does not enumerate three-element substitution sets (Active Search). With every key on Bob’s side under attacker control, amaster needs no leaked value at all: the attacker computes all four Diffie–Hellman inputs from Alice’s public keys and nil (steps 4–8).

The second trace impersonates Bob. The attacker rebuilds Alice’s ratchet state from the substituted keys (steps 3–12), forges a ciphertext under the message key that Alice will derive, with associated data that names the substituted identity and ratchet keys (step 15), and Alice’s checked decryption accepts it (step 16). The nonce needs no forging: Bob published n_e2 beside the ciphertext, so the attacker reads it off the wire in step 13 and seals its own plaintext under the same one. Because gbs and gbe are both replaced by PUBKEY(nil), Alice’s two ratchet secrets collapse to the same term DH_KEX(gae2, nil), which the trace names akshared1 in step 10. The omitted trace for m3 performs the same forgery and then follows Alice’s next ratchet step, which now depends only on attacker-known values.

The query authentication? Alice -> Bob: e1 still passes because Alice’s identity key galongterm remains guarded. The attacker can impersonate Bob to Alice but not Alice to Bob under this variant.

Confidentiality fails for m1 and m3, while m2 remains protected. Authentication fails only for Bob-to-Alice traffic. The remaining guard therefore preserves one direction of authentication and the properties that depend on it.

These experiments do not test post-compromise recovery: they never expose a current root key, chain key or ratchet private key and then query messages after recovery. To investigate that property, add the appropriate state disclosure at the compromise point and extend the modeled ratchet with fresh uncompromised input. Do not infer it from a later identity-key leak alone.

In the initial model, both identity keys are guarded, Alice checks the signed pre-key and both identity private keys leak only after the exchange. Verifpal finds no attack on the six queries under those assumptions.

Sources