Documentation / The Signal protocol

The Signal protocol

Model classical X3DH and three Double Ratchet messages, then test what happens when a check is missing or a key is compromised.

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

This guide tests key authentication, signature checks and later compromise in classical X3DH and three alternating Double Ratchet messages. It covers only this exchange. The Signal specifications also describe post-quantum constructions and other parts of the application.

Security goals

Signal aims to keep messages confidential, authenticate participants and limit the damage from key compromise. Each participant has long-term identity keys to authenticate the initial exchange and short-lived ephemeral keys to derive new message keys. Two goals concern key compromise:

• 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

Modeling the key exchange

When the exchange includes Bob’s optional one-time pre-key, 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. See sessions and execution histories for how these values are copied across runs.

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

The Double Ratchet derives each message key from the authenticated master secret and new ephemeral secrets:

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 therefore depends on both the authenticated master secret and the new Diffie–Hellman secret.

The guards on gblongterm and galongterm assume that Alice and Bob have already authenticated each other’s identity keys, for example by comparing Signal safety numbers out of band. 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]

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.

All six queries pass at two sessions, and each verdict reports that the search finished. This result is consistent with earlier formal analyses of Signal (Kobeissi et al. 2017; Cohn-Gordon et al. 2017). The model assumes that both parties have authenticated the identity keys and that 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 observes gblongterm on the wire.
| 2. Attacker replaces gbs, gbo (sent by Bob to Alice) with
| gblongterm, gblongterm. (gbs was PUBKEY(bs); gbo was PUBKEY(bo))
| 3. Attacker observes e1 on the wire, where it is
| AEAD_ENC(akenc1, n_e1, m1, HASH(galongterm, gblongterm, gae2)).
| 4. Attacker is handed alongterm by a leaks declaration in
| Alice#2.
| 5. Attacker constructs DH_KEX(gblongterm, alongterm).
| 6. Attacker observes gae1 on the wire.
| 7. Attacker is handed blongterm by a leaks declaration in Bob#2.
| 8. Attacker constructs DH_KEX(gae1, blongterm).
| 9. Attacker constructs amaster, where it is
| HASH(DH_KEX(gblongterm, alongterm), DH_KEX(gae1, blongterm),
| DH_KEX(gae1, blongterm), DH_KEX(gae1, blongterm)).
| 10. Attacker observes gae2 on the wire.
| 11. Attacker constructs akshared1, where it is DH_KEX(gae2,
| blongterm).
| 12. Attacker constructs ackab1, where it is HKDF(amaster,
| akshared1, nil)|2.
| 13. Attacker constructs MAC(ackab1, nil).
| 14. Attacker constructs akenc1, where it is HKDF(nil,
| MAC(ackab1, nil), nil)|1.
| 15. Attacker observes n_e1 on the wire.
| 16. Attacker opens e1 with akenc1, 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]
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 after the phase 1 disclosure. The trace replaces Bob’s signed and one-time pre-keys with his own identity public key, gblongterm, which Alice now accepts without a valid pre-key signature. Each Diffie–Hellman term in Alice’s master secret then pairs Bob’s identity key with one of her private values. Once both identity private keys leak, the attacker rebuilds amaster, derives akenc1 and decrypts Alice’s first message.

The session count matters here. At one session this variant returns c0a0c0a0c0a0: Bob’s checked decryption rejects Alice’s first message, which is encrypted under the altered master secret, so Bob halts, Alice waits for a reply that never comes, and neither reaches its phase 1 leak. Steps 4 and 7 show what the second session adds. The identity keys are leaked by Alice#2 and Bob#2, whose unmodified exchange completes, while the attacked first session supplies the recorded ciphertext.

Verifpal finds no disclosure of m2 or m3 in this variant. The reported attack exposes only the first message.

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 observes gblongterm on the wire.
| 2. Attacker replaces gbs, gbo (sent by Bob to Alice) with
| gblongterm, gblongterm. (gbs was PUBKEY(bs); gbo was PUBKEY(bo))
| 3. Attacker observes e1 on the wire, where it is
| AEAD_ENC(akenc1, n_e1, m1, HASH(galongterm, gblongterm, gae2)).
| 4. Attacker is handed alongterm by a leaks declaration in
| Alice#2.
| 5. Attacker constructs DH_KEX(gblongterm, alongterm).
| 6. Attacker observes gae1 on the wire.
| 7. Attacker is handed blongterm by a leaks declaration in Bob#2.
| 8. Attacker constructs DH_KEX(gae1, blongterm).
| 9. Attacker constructs amaster, where it is
| HASH(DH_KEX(gblongterm, alongterm), DH_KEX(gae1, blongterm),
| DH_KEX(gae1, blongterm), DH_KEX(gae1, blongterm)).
| 10. Attacker observes gae2 on the wire.
| 11. Attacker constructs akshared1, where it is DH_KEX(gae2,
| blongterm).
| 12. Attacker constructs ackab1, where it is HKDF(amaster,
| akshared1, nil)|2.
| 13. Attacker constructs MAC(ackab1, nil).
| 14. Attacker constructs akenc1, where it is HKDF(nil,
| MAC(ackab1, nil), nil)|1.
| 15. Attacker observes n_e1 on the wire.
| 16. Attacker opens e1 with akenc1, 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 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 galongterm on the wire.
| 4. Attacker constructs DH_KEX(galongterm, nil).
| 5. Attacker observes gae1 on the wire.
| 6. Attacker constructs DH_KEX(gae1, nil).
| 7. Attacker constructs amaster, where it is
| HASH(DH_KEX(galongterm, nil), DH_KEX(gae1, nil), DH_KEX(gae1,
| nil), DH_KEX(gae1, nil)).
| 8. Attacker observes gae2 on the wire.
| 9. Attacker constructs akshared1, where it is DH_KEX(gae2, nil).
| 10. Attacker constructs arkab1, where it is HKDF(amaster,
| akshared1, nil)|1.
| 11. Attacker constructs ackba2, where it is HKDF(arkab1,
| akshared1, nil)|2.
| 12. Attacker constructs MAC(ackba2, nil).
| 13. Attacker constructs akenc2, where it is HKDF(nil,
| MAC(ackba2, nil), nil)|1.
| 14. Attacker constructs HASH(galongterm, PUBKEY(nil),
| PUBKEY(nil)).
| 15. Attacker constructs AEAD_ENC(akenc2, nil, nil,
| HASH(galongterm, PUBKEY(nil), PUBKEY(nil))).
| 16. Attacker replaces gbe, n_e2, e2 (sent by Bob to Alice) with
| PUBKEY(nil), nil, AEAD_ENC(akenc2, nil, nil, HASH(galongterm,
| PUBKEY(nil), PUBKEY(nil))). (gbe was PUBKEY(be); e2 was
| AEAD_ENC(akenc2, n_e2, m2, HASH(galongterm, gblongterm, gbe)))
| 17. Alice's AEAD_DEC(akenc2, nil, AEAD_ENC(akenc2, nil, 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, nil, 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.

The first trace is the leak-based disclosure of the unchecked variant: removing the guard adds no shorter route to m1. Step 2 of the second 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 3–7).

The second trace impersonates Bob. The attacker rebuilds Alice’s ratchet state from the substituted keys (steps 3–13). It then forges a ciphertext using the message key Alice will derive and associated data containing the substituted identity and ratchet keys (steps 14–15), and delivers it with nil as its nonce (step 16). Alice’s checked decryption accepts it (step 17).

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 9 and reuses in step 11. 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.

The attacker learns m1 and m3, but the search finds no disclosure of m2. Only Bob-to-Alice authentication fails; the guard on Alice’s identity key still protects the other direction.

Testing post-compromise recovery requires a different experiment: leak a current root key, chain key or ratchet private key, then query messages after new uncompromised ratchet inputs. These models leak only identity keys, so they do not test that property.

Sources