Documentation / Post-quantum protocol analysis

Post-quantum protocol analysis

Investigate PQXDH key-role confusion, domain separation and hybrid security under future compromise.

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

This guide models a future adversary that records a protocol execution and later gains the ability to recover Diffie–Hellman private values. It then tests whether a hybrid post-quantum exchange protects the recorded message.

A Symbolic Quantum Threat Model

In a harvest-now, decrypt-later attack, an adversary records ciphertexts that are secure today and retains them until the underlying public-key problem becomes tractable. 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 symbolic model does not represent quantum computation or algorithmic hardness. It can represent the protocol-level consequence: every relevant Diffie–Hellman private value becomes available in a later phase.

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.

For public keys available to the attacker, the corresponding recovery can be expressed by weakening each affected 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). Ordinary reconstruction then derives every affected Diffie–Hellman secret.

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. The formulations also differ in maintenance and scope. A leaks clause names particular private values and must be updated when the model adds a key. A weakening annotation states the failure at each public-key call site and automatically affects all uses of that term. Modeling Failure with Weakening Assumptions compares their traces.

Neither form models Shor’s algorithm. Both are assumptions supplied by the model author about the information available to the future attacker.

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 cannot validate that computational assumption; it can only analyze its protocol consequences. A later variant reverses the assumption.

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.

PQXDH has been analyzed before, by Bhargavan, Jacomme, Kiefer and Schmidt 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 two analyses in this guide follow that history: the first model is shaped like revision 1, and the second adds what revision 2 requires.

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 resulting session key depends on both classical and post-quantum components. The intended hybrid property is that it remains protected while either component remains secure (Hybrid Key Exchange).

This is a teaching model inspired by PQXDH, not a complete transcription of the specification. It omits the key identifiers Alice sends so that Bob can retrieve the right pre-keys, which the published analysis found to carry no security weight, and it treats every public key through the same PUBKEY constructor. In particular, it permits a Diffie–Hellman key to occupy a KEM-key field. The cross-role substitution below illustrates a missing binding in this model; it does not establish that a deployed PQXDH implementation accepts that substitution. Signal’s own does not: Kyber and X25519 keys differ in length and each carries an algorithm byte. Revision 2 of the specification makes the requirement explicit, demanding that the encoding functions for the two key types have disjoint ranges.¹

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
]

Because dkb remains secret, the intended hybrid argument predicts that the KEM component will preserve the message after every Diffie–Hellman private value leaks. The analysis exposes a key-role substitution that defeats this argument.

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

Fail ✗ 1 of 2 queries failed.

The trace prints whole terms where a reader might expect names such as ss#2 or amaster#2. That is deliberate: once the attacker installs a value into ekb#2, every value computed from it is shadowed, and naming it after the slot it displaced would describe the honest run rather than this one. The names return in the classical traces later in this guide, where nothing is substituted.

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. Another run can complete honestly and disclose the shared classical keys, including bs. Alice’s attacked run supplies the encapsulation and encrypted message. Keep the #2 suffixes when reconstructing that execution.

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 therefore encapsulates to a key whose private value belongs to the classical exchange. The supposed post-quantum component becomes another classical component and fails under the same future disclosure.

Bind Signatures to Key Roles

A signature authenticates its message, but the message must also encode the value’s protocol role. If two key types are signed under the same identity key without distinct tags, a valid signed value from one role may be accepted in the other. The signature is valid; its context is wrong.

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.

Analysis Two: 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)?
	...
]

Each signature is now made over a tagged encoding of the key rather than the bare key, so a signature produced for the curve role cannot satisfy a verification for the KEM role. The tags are public and CONCAT hides nothing: the attacker can wrap either tag around any key it holds. What it cannot produce is Bob’s signature over the encoding it needs. The separation rests on the signature covering the role marker, not on the marker being secret. The cross-role substitution now 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 inverts only the matching KEM_ENCAP, so it has that binding by construction and the attack has no symbolic counterpart here. A symbolic model provides the properties its primitives declare; it cannot warn about an assumption it never had.

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.

Analysis Three: Classical X3DH Under Future 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.
| 4. Attacker constructs DH_KEX(gbs, alongterm).
| 5. Attacker observes gblongterm on the wire.
| 6. Attacker is handed ae1 by a leaks declaration.
| 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 confidentiality trace contains no mutation. The attacker observes the public values and, after the later leaks, reconstructs the four Diffie–Hellman secrets and derives Alice’s message key. The minimized trace shows only the leaked private values needed for that derivation.

This is the harvest-now, decrypt-later threat: passive recording in phase 0 followed by key recovery in phase 1. Unlike a substitution or reflection attack, it creates no anomalous phase 0 message for a participant to detect.

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.

Modeling Failure with Weakening Assumptions

The preceding analyses enumerate five phase 1 leaks. An alternative is to remove those leaks and annotate every 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]

This form produces the same passing verdicts as Analysis Two, now accompanied by 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 Analysis Three, a leaks declaration hands 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 Analysis Two verdict is therefore explicitly conditional on the KEM remaining secure after the declared classical break.

Analysis Four: Post-Quantum Component Compromise

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.

Verifpal again finds no contradiction because the four Diffie–Hellman values remain unavailable. This is the intended hybrid behavior in the symbolic model: the remaining secret component prevents the shown key reconstruction.

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. The hybrid property ends when neither component remains secret. The authentication query still passes, because the compromise occurs after the message was sent.

Sources