Documentation / Post-quantum protocol analysis

Post-quantum protocol analysis

Test a PQXDH-inspired exchange for key confusion, then add domain separation and compromise each component in turn.

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

The attacker records messages, then later recovers Diffie–Hellman private values. This guide tests whether adding a post-quantum component keeps those messages secret.

Modeling a quantum attacker

In a harvest-now, decrypt-later attack, an attacker records ciphertexts and waits until it can break the public-key cryptography that protects them. A sufficiently capable quantum computer running Shor’s algorithm would break the discrete-logarithm assumptions used by Diffie–Hellman, allowing recorded session secrets to be reconstructed.

The model represents the consequence of such a break by making every relevant Diffie–Hellman private value available in a later phase. It does not simulate quantum computation or assess algorithmic hardness.

phase[1]

principal Alice[leaks alongterm, ae1]
principal Bob[leaks blongterm, bs, bo]

In phase 0, the protocol runs under the ordinary active attacker. In phase 1, every listed Diffie–Hellman private value leaks (Phases). The confidentiality query then asks whether a phase 0 message remains secret after that later disclosure.

If the attacker has the public keys, you can express private-key recovery by annotating each public-key derivation:

galongterm = PUBKEY[weak from phase 1](alongterm)
gbs        = PUBKEY[weak from phase 1](bs)

The PUBKEY[weak] assumption lets the attacker recover a private value from the corresponding public key from phase 1 onward (Declared Weakening Assumptions). The attacker can then compute the affected Diffie–Hellman secrets.

A leak hands over the private value directly. A weakening annotation requires the attacker to obtain the affected public key; it does not reveal a private key whose public key never becomes available. A leaks clause must list each private value, so update it when adding a key. An annotation applies to a particular public-key derivation and all uses of the resulting term. Using weakening assumptions compares their traces.

Both forms assume the attacker has gained this capability; neither establishes that a cryptographic break is possible.

The first analyses assume that the key-encapsulation mechanism remains secure while the classical exchange fails. It stands for ML-KEM (National Institute of Standards and Technology 2024) or another post-quantum KEM (Hybrid Key Exchange). Verifpal takes the KEM’s security as an assumption. A later variant compromises the KEM instead.

PQXDH

Signal’s PQXDH construction (Kret and Schmidt 2023) extends the X3DH handshake from The Signal protocol. The model in this guide uses all four X3DH Diffie–Hellman values derived from Bob’s identity key, signed pre-key and one-time pre-key.

Bhargavan, Jacomme, Kiefer and Schmidt analyzed PQXDH using ProVerif and CryptoVerif (Bhargavan et al. 2024). That analysis found the key-confusion problem reproduced below and a KEM re-encapsulation attack, and its authors worked with Signal to produce revision 2 of the specification. The first model below follows revision 1; the second adds the key separation required by revision 2.

PQXDH adds a KEM encapsulation key signed by Bob’s identity key. Alice encapsulates to it, obtaining shared secret ss and ciphertext ct. She includes ss with the four Diffie–Hellman values in the master secret and sends ct to Bob, who decapsulates it.

The intended hybrid property is that the session key stays secret as long as at least one component, classical or post-quantum, remains secure.

This teaching model simplifies PQXDH. It omits the identifiers Alice sends to tell Bob which pre-keys to use; the published analysis found that these identifiers did not affect security. It also represents all public keys with PUBKEY, allowing a Diffie–Hellman key in a KEM-key field.

The key substitution below succeeds in this model. Signal’s implementation rejects it because Kyber and X25519 keys have different lengths and carry algorithm bytes. Revision 2 of the specification explicitly requires disjoint encodings for the two key types.¹

The complete models are pqxdh.vp, pqxdh-separated.vp and the named compromise variants in the same directory. Unless a count is stated explicitly, the results use two sessions.

A first model

Begin with Alice’s identity key:

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

Bob signs both the Diffie–Hellman pre-key and the KEM encapsulation key with his identity key:

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

Bob -> Alice: [gblongterm], gbs, gbssig, gbo, ekb, ekbsig

Alice verifies both signatures, encapsulates to the KEM key and combines the KEM secret with four Diffie–Hellman values:

principal Alice[
	generates m1, ae1, r
	gae1 = PUBKEY(ae1)
	valid = SIGNVERIF(gblongterm, gbs, gbssig)?
	kvalid = SIGNVERIF(gblongterm, ekb, ekbsig)?
	ss, ct = KEM_ENCAP(ekb, r)
	akm = HASH(DH_KEX(gbs, alongterm), DH_KEX(gblongterm, ae1), DH_KEX(gbs, ae1), DH_KEX(gbo, ae1), ss)
	amaster = HKDF(nil, akm, info)
	generates n_e1
	e1 = AEAD_ENC(amaster, n_e1, m1,
		HASH(galongterm, gblongterm, gae1))
]

Alice -> Bob: [galongterm], gae1, ct, n_e1, e1

Bob decapsulates the KEM ciphertext, reconstructs the master secret and checks Alice’s ciphertext:

principal Bob[
	bss = KEM_DECAP(dkb, ct)
	bkm = HASH(DH_KEX(galongterm, bs), DH_KEX(gae1, blongterm), DH_KEX(gae1, bs), DH_KEX(gae1, bo), bss)
	bmaster = HKDF(nil, bkm, info)
	m1_d = AEAD_DEC(bmaster, n_e1, e1,
		HASH(galongterm, gblongterm, gae1))?
]

Both identity keys are guarded, so the model excludes identity-key substitution and isolates the future-compromise question. Alice checks both pre-key signatures. The KEM_DECAP call is unchecked, so a mismatched ciphertext leaves an unreduced term and the later AEAD check decides whether Bob continues. This approximates that control flow; it does not model ML-KEM’s implicit-rejection secret (Checked Primitives). The five-input HASH contains the four Diffie–Hellman values and the KEM secret.

Append the phase 1 leak clause from the start of this guide. The queries test message confidentiality and Alice-to-Bob authentication:

queries[
	confidentiality? m1
	authentication? Alice -> Bob: e1
]

With dkb still secret, the KEM component should protect the message after the Diffie–Hellman private values leak. A key substitution defeats that protection in this model.

1. Missing domain separation

The confidentiality query is contradicted:

Fail ✗ confidentiality? m1
Attack trace:
| 1. Attacker observes gbs on the wire.
| 2. Attacker observes gbssig on the wire.
| 3. Attacker replaces ekb, ekbsig (sent by Bob to Alice) with
| gbs, gbssig. (ekb was PUBKEY(dkb); ekbsig was SIGN(blongterm,
| ekb))
| 4. Alice's SIGNVERIF(gblongterm, gbs, gbssig)? passes — the
| attacker controls one of its inputs.
| 5. Attacker observes e1 on the wire, where it is
| AEAD_ENC(amaster, n_e1, m1, HASH(galongterm, gblongterm, gae1)).
| 6. Attacker is handed alongterm by a leaks declaration in Alice.
| 7. Attacker constructs DH_KEX(gbs, alongterm).
| 8. Attacker observes gblongterm on the wire.
| 9. Attacker is handed ae1 by a leaks declaration in Alice.
| 10. Attacker constructs DH_KEX(gblongterm, ae1).
| 11. Attacker constructs DH_KEX(gbs, ae1).
| 12. Attacker observes gbo on the wire.
| 13. Attacker constructs DH_KEX(gbo, ae1).
| 14. Attacker observes ct on the wire, where it is KEM_ENCAP(gbs,
| r)|2.
| 15. Attacker is handed bs by a leaks declaration in Bob#2.
| 16. Attacker opens ct with bs, obtaining ss.
| 17. Attacker constructs akm, where it is HASH(DH_KEX(gbs,
| alongterm), DH_KEX(gblongterm, ae1), DH_KEX(gbs, ae1),
| DH_KEX(gbo, ae1), ss).
| 18. Attacker constructs amaster, where it is HKDF(nil, akm,
| info)|1.
| 19. Attacker observes n_e1 on the wire.
| 20. Attacker opens e1 with amaster, n_e1, obtaining m1.
> m1 (m1) is obtained by Attacker.
Pass ✓ authentication? Alice -> Bob: e1  [search exhausted at 2 sessions]

Fail ✗ 1 of 2 queries failed.

Values affected by the substitution keep their model names, and the trace spells out what they hold in this execution. Step 17, for example, constructs akm from the four Diffie–Hellman terms over the substituted key and the decapsulated ss. The later classical traces need no such expansion because no substitution occurs.

At one session the first model returns c0a0; the attack shown here needs two. The substituted KEM key stops the attacked Bob run before its later leaks. Step 15 therefore takes bs from Bob#2, whose unmodified exchange completes and discloses the shared signed pre-key. Alice’s attacked run supplies the encapsulation and the encrypted message, and her own leaks supply alongterm and ae1 (steps 6 and 9).

Steps 14–16 show the critical dependency. The attacker decapsulates Alice’s KEM ciphertext with bs, the private value for Bob’s Diffie–Hellman signed pre-key, after bs leaks in phase 1. Step 4 is the gate at which Alice’s signature check accepts the substituted key. Alice had computed:

In step 3, the attacker replaces the KEM key ekb with the Diffie–Hellman pre-key gbs, and replaces its signature with the valid gbssig. Both values came from Bob’s public bundle. Alice’s signature check succeeds because Bob did sign gbs; neither the signed message nor the verification context identifies the key’s intended role.

Alice encapsulates to a Diffie–Hellman pre-key. When its private value leaks, the attacker can also recover the KEM secret.

Bind Signatures to Key Roles

Include the key’s role in the signed message. Otherwise, when two key types share a signing key and have no distinct tags, a valid signature for one type may be accepted for the other.

The phase 0 substitution uses only public values already in Bob’s bundle. The phase 1 compromise reveals the private value that completes the attack; it does not create the type-confusion flaw.

2. Domain separation

Domain separation binds each signature to a key role. Assign a public tag to each pre-key type and sign the tagged value:

principal Bob[
	knows public info, ec_tag, kem_tag
	...
	gbssig = SIGN(blongterm, CONCAT(ec_tag, gbs))
	ekbsig = SIGN(blongterm, CONCAT(kem_tag, ekb))
]

principal Alice[
	valid = SIGNVERIF(gblongterm,
		CONCAT(ec_tag, gbs), gbssig)?
	kvalid = SIGNVERIF(gblongterm,
		CONCAT(kem_tag, ekb), ekbsig)?
	...
]

Bob now signs both the role tag and the key. A signature for a curve key therefore fails verification with the KEM tag. The attacker can construct either tagged value because the tags are public and CONCAT hides nothing, but it cannot produce Bob’s signature for the substituted key and tag. The substitution fails:

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

Pass ✓ All 2 queries pass.

After the phase 1 leaks, the attacker reconstructs all four Diffie–Hellman components but not ss. Verifpal finds no contradiction to message confidentiality or authentication under these assumptions.

The published analysis found a second problem that this model cannot express. Under the standard IND-CCA assumption, a KEM may permit re-encapsulation: an attacker holding one compromised decapsulation key can produce a different ciphertext, valid under a different public key, that decapsulates to the same shared secret (Bhargavan et al. 2024). The two parties then need not agree on which KEM key was used. Revision 2 offers two remedies: bind the KEM public key into the AEAD associated data, or require a KEM that ties the shared secret to its public key. Signal relies on the second, which Kyber satisfies.

Verifpal’s KEM_DECAP recovers a shared secret only from a matching KEM_ENCAP term. This rule binds the secret to its public key, so the model cannot represent the re-encapsulation attack.

Guarding ekb also prevents the substitution, but represents a different mechanism. Domain separation makes the signature distinguish key roles. A guard assumes that Alice authenticated the exact KEM key before the exchange. Either assumption blocks this trace, but only the first is provided by the signed bundle itself.

3. Classical X3DH after compromise

To isolate the KEM’s contribution, remove the KEM keys, signatures, encapsulation and decapsulation. The resulting classical X3DH master secret contains only the four Diffie–Hellman values. Keep the phase 1 leak unchanged.

Fail ✗ confidentiality? m1
Attack trace:
| 1. Attacker observes e1 on the wire.
| 2. Attacker observes gbs on the wire.
| 3. Attacker is handed alongterm by a leaks declaration in Alice.
| 4. Attacker constructs DH_KEX(gbs, alongterm).
| 5. Attacker observes gblongterm on the wire.
| 6. Attacker is handed ae1 by a leaks declaration in Alice.
| 7. Attacker constructs DH_KEX(gblongterm, ae1).
| 8. Attacker constructs DH_KEX(gbs, ae1).
| 9. Attacker observes gbo on the wire.
| 10. Attacker constructs DH_KEX(gbo, ae1).
| 11. Attacker constructs akm.
| 12. Attacker constructs amaster.
| 13. Attacker observes n_e1 on the wire.
| 14. Attacker opens e1 with amaster, n_e1, obtaining m1.
> m1 (m1) is obtained by Attacker.
Pass ✓ authentication? Alice -> Bob: e1  [search exhausted at 2 sessions]

Fail ✗ 1 of 2 queries failed.

The attacker changes no messages in this trace. The attacker observes the public values and, after the later leaks, reconstructs the four Diffie–Hellman secrets and derives Alice’s message key. The reduced trace shows only the leaked private values needed for that derivation.

The attacker records traffic in phase 0 and recovers keys in phase 1. No participant receives an altered message during the exchange.

Authentication still passes in the classical model. The attacker derives the session key only in phase 1, whereas e1 was sent in phase 0. A substitution is judged against the knowledge available in the phase of that delivery (Phases), so the later leaks cannot justify a forged ciphertext in the earlier phase. The recorded message can be read after the compromise, but it could not have been forged before it. A leak available before the handshake would state a different threat model. Moving a leak to phase 0 does not by itself move it before the checks that the leaking principal must reach.

Using weakening assumptions

Replace the five phase 1 leaks with weakening annotations on each Diffie–Hellman public-key derivation in the domain-separated model. Leave the KEM key ekb unannotated so that it remains the secure hybrid component:

principal Alice[
	...
	galongterm = PUBKEY[weak from phase 1](alongterm)
	gae1 = PUBKEY[weak from phase 1](ae1)
]
principal Bob[
	...
	gblongterm = PUBKEY[weak from phase 1](blongterm)
	gbs        = PUBKEY[weak from phase 1](bs)
	gbo        = PUBKEY[weak from phase 1](bo)
	ekb        = PUBKEY(dkb)
]

phase[1]

The domain-separated model still passes both queries, now with five weakening-assumption warnings. Removing the KEM again produces the classical failure, with a trace that attributes private-key recovery to the declared assumption:

Warning ▲ Analysis performed under 5 declared weakening assumptions:
Warning ▲ PUBKEY[weak from phase 1](alongterm)
Warning ▲ PUBKEY[weak from phase 1](blongterm)
Warning ▲ PUBKEY[weak from phase 1](bs)
Warning ▲ PUBKEY[weak from phase 1](bo)
Warning ▲ PUBKEY[weak from phase 1](ae1)
Fail ✗ confidentiality? m1
Attack trace:
| 1. Attacker observes e1 on the wire.
| 2. Attacker observes gbs on the wire.
| 3. Attacker observes galongterm on the wire.
| 4. Attacker breaks galongterm under the declared `weak`
| assumption, obtaining alongterm.
| 5. Attacker constructs DH_KEX(gbs, alongterm).
| 6. Attacker observes gblongterm on the wire.
| 7. Attacker observes gae1 on the wire.
| 8. Attacker breaks gae1 under the declared `weak` assumption,
| obtaining ae1.
| 9. Attacker constructs DH_KEX(gblongterm, ae1).
| 10. Attacker constructs DH_KEX(gbs, ae1).
| 11. Attacker observes gbo on the wire.
| 12. Attacker constructs DH_KEX(gbo, ae1).
| 13. Attacker constructs akm.
| 14. Attacker constructs amaster.
| 15. Attacker observes n_e1 on the wire.
| 16. Attacker opens e1 with amaster, n_e1, obtaining m1.
> m1 (m1) is obtained by Attacker.
Pass ✓ authentication? Alice -> Bob: e1  [search exhausted at 2 sessions]

Fail ✗ 1 of 2 queries failed.

Verifpal lists the five annotations once each, although session replication applies them to every session’s copy of the annotated terms (Sessions and execution histories). In the classical model above, a leaks declaration gives alongterm to the attacker. Here, steps 4 and 8 derive alongterm and ae1 by breaking the corresponding public keys, and each step names the assumption it depends on. The resulting attacker knowledge is the same, but the annotation states the assumed cryptographic failure directly. The authentication query passes for the same reason as before: the assumption is in force only from phase 1.

Verifpal prints active assumptions before every result, including passing results. The pass for the domain-separated model depends on the KEM staying secure after the declared classical break.

4. Compromising the KEM

The converse experiment compromises the KEM while leaving Diffie–Hellman intact. In the domain-separated model, replace the classical leaks with a phase 1 leak of dkb:

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

Pass ✓ All 2 queries pass.

Both queries pass. The four Diffie–Hellman secrets remain unavailable to the attacker, preventing it from reconstructing the message key.

If phase 1 reveals both the Diffie–Hellman private values and dkb, the confidentiality query fails: the trace decapsulates ct with the leaked dkb and then follows the classical derivation. With both components compromised, the attacker can recover the message. The authentication query still passes, because the compromise occurs after the message was sent.

Sources