PQXDH in Lean

7.4. Security properties🔗

Definition7.15
Group: Formal security definitions and assumptions for PQXDH, following Bhargavan et al. (USENIX Security 2024). (21)
Hover another entry in this group to preview it.
Preview
Definition 7.1
Blueprint label
  • sig_keypair
Group
  • Formal security definitions and assumptions for PQXDH, following Bhargavan et al. (USENIX Security 2024).
✓L∃∀Nused by 0

Message secrecy: the session key is indistinguishable from random in the AKE security game, where the adversary may control the network, corrupt long-term keys, and reveal session keys, subject to a freshness condition on the test session.

Code for Definition7.15●1 definition
  • opaque MessageSecrecy.{u_1, u_2, u_3, u_4, u_5, u_6, u_7} (GType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. )
  [AddCommGroupAddCommGroup.{u} (G : Type u) : Type uAn additive commutative group is an additive group with commutative `(+)`.  GType u_1] (PKType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) (SK_kemType u_3 : Type u_3A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) (CTType u_4 : Type u_4A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. )
  (SSType u_5 : Type u_5A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) (kemKEM PK SK_kem CT SS : KEMKEM.{u_1, u_2, u_3, u_4} (PK : Type u_1) (SK_kem : Type u_2) (CT : Type u_3) (SS : Type u_4) :
  Type (max (max (max u_1 u_2) u_3) u_4)KEM parameterized by public key `PK`, secret key `SK_kem`,
ciphertext `CT`, and shared secret `SS`. The `correctness` field
guarantees that honest encapsulation/decapsulation round-trips.  PKType u_2 SK_kemType u_3 CTType u_4 SSType u_5) (IType u_6 : Type u_6A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. )
  (KType u_7 : Type u_7A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) (kdfKDF I K : KDFKDF.{u_1, u_2} (I : Type u_1) (K : Type u_2) : Type (max u_1 u_2)KDF as a deterministic function, for correctness proofs.  IType u_6 KType u_7) (freshFreshness : FreshnessFreshness : Type§3.3, p. 473–474: Freshness condition for the AKE security game.

A test session is *fresh* if the adversary has not trivially obtained
the answer. Specifically, a session between Alice (initiator) and
Bob (responder) is fresh if:

  1. The adversary did not `RevealSessionKey` on the test session
     or its matching partner session.
  2. The adversary did not `Corrupt` *both* Alice's and Bob's
     long-term identity keys before the test session completed.
  3. (For forward secrecy) The adversary did not `Corrupt` the
     ephemeral key of the test session.

The exact freshness condition varies by theorem; the paper defines
it within each CryptoVerif game. ) : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    opaque MessageSecrecy.{u_1, u_2, u_3, u_4, u_5,
    u_6, u_7}
  (GType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) [AddCommGroupAddCommGroup.{u} (G : Type u) : Type uAn additive commutative group is an additive group with commutative `(+)`.  GType u_1]
  (PKType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) (SK_kemType u_3 : Type u_3A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. )
  (CTType u_4 : Type u_4A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) (SSType u_5 : Type u_5A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. )
  (kemKEM PK SK_kem CT SS : KEMKEM.{u_1, u_2, u_3, u_4} (PK : Type u_1) (SK_kem : Type u_2) (CT : Type u_3) (SS : Type u_4) :
  Type (max (max (max u_1 u_2) u_3) u_4)KEM parameterized by public key `PK`, secret key `SK_kem`,
ciphertext `CT`, and shared secret `SS`. The `correctness` field
guarantees that honest encapsulation/decapsulation round-trips.  PKType u_2 SK_kemType u_3 CTType u_4 SSType u_5)
  (IType u_6 : Type u_6A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) (KType u_7 : Type u_7A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. )
  (kdfKDF I K : KDFKDF.{u_1, u_2} (I : Type u_1) (K : Type u_2) : Type (max u_1 u_2)KDF as a deterministic function, for correctness proofs.  IType u_6 KType u_7) (freshFreshness : FreshnessFreshness : Type§3.3, p. 473–474: Freshness condition for the AKE security game.

A test session is *fresh* if the adversary has not trivially obtained
the answer. Specifically, a session between Alice (initiator) and
Bob (responder) is fresh if:

  1. The adversary did not `RevealSessionKey` on the test session
     or its matching partner session.
  2. The adversary did not `Corrupt` *both* Alice's and Bob's
     long-term identity keys before the test session completed.
  3. (For forward secrecy) The adversary did not `Corrupt` the
     ephemeral key of the test session.

The exact freshness condition varies by theorem; the paper defines
it within each CryptoVerif game. ) :
  PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    §3.3, p. 474 "Confidentiality" and §3.5, p. 475:
Message secrecy in the AKE security game.
The session key derived by PQXDH is indistinguishable from random
for any adversary that:
  - Controls the network (active MitM).
  - May corrupt long-term keys and reveal session keys.
  - Satisfies the freshness condition for the test session.

Parameterized by the group (for DH), the KEM (for PQ component),
and the KDF (which derives the session key).
This is the "real-or-random" indistinguishability game on the
output of `KDF.derive(DH1 ‖ DH2 ‖ DH3 ‖ DH4 ‖ ss)`.
    complete
Definition7.16
Group: Formal security definitions and assumptions for PQXDH, following Bhargavan et al. (USENIX Security 2024). (21)
Hover another entry in this group to preview it.
Preview
Definition 7.1
Blueprint label
  • sig_keypair
Group
  • Formal security definitions and assumptions for PQXDH, following Bhargavan et al. (USENIX Security 2024).
✓L∃∀Nused by 1

Peer authentication: if a session completes, the peer's identity key was used in the computation.

Code for Definition7.16●1 definition
  • opaque PeerAuth.{u_1, u_2, u_3, u_4, u_5, u_6, u_7} (GType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. )
  [AddCommGroupAddCommGroup.{u} (G : Type u) : Type uAn additive commutative group is an additive group with commutative `(+)`.  GType u_1] (PKType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) (SK_kemType u_3 : Type u_3A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) (CTType u_4 : Type u_4A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. )
  (SSType u_5 : Type u_5A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) (kemKEM PK SK_kem CT SS : KEMKEM.{u_1, u_2, u_3, u_4} (PK : Type u_1) (SK_kem : Type u_2) (CT : Type u_3) (SS : Type u_4) :
  Type (max (max (max u_1 u_2) u_3) u_4)KEM parameterized by public key `PK`, secret key `SK_kem`,
ciphertext `CT`, and shared secret `SS`. The `correctness` field
guarantees that honest encapsulation/decapsulation round-trips.  PKType u_2 SK_kemType u_3 CTType u_4 SSType u_5) (IType u_6 : Type u_6A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. )
  (KType u_7 : Type u_7A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) (kdfKDF I K : KDFKDF.{u_1, u_2} (I : Type u_1) (K : Type u_2) : Type (max u_1 u_2)KDF as a deterministic function, for correctness proofs.  IType u_6 KType u_7) : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    opaque PeerAuth.{u_1, u_2, u_3, u_4, u_5, u_6,
    u_7}
  (GType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) [AddCommGroupAddCommGroup.{u} (G : Type u) : Type uAn additive commutative group is an additive group with commutative `(+)`.  GType u_1]
  (PKType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) (SK_kemType u_3 : Type u_3A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. )
  (CTType u_4 : Type u_4A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) (SSType u_5 : Type u_5A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. )
  (kemKEM PK SK_kem CT SS : KEMKEM.{u_1, u_2, u_3, u_4} (PK : Type u_1) (SK_kem : Type u_2) (CT : Type u_3) (SS : Type u_4) :
  Type (max (max (max u_1 u_2) u_3) u_4)KEM parameterized by public key `PK`, secret key `SK_kem`,
ciphertext `CT`, and shared secret `SS`. The `correctness` field
guarantees that honest encapsulation/decapsulation round-trips.  PKType u_2 SK_kemType u_3 CTType u_4 SSType u_5)
  (IType u_6 : Type u_6A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) (KType u_7 : Type u_7A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. )
  (kdfKDF I K : KDFKDF.{u_1, u_2} (I : Type u_1) (K : Type u_2) : Type (max u_1 u_2)KDF as a deterministic function, for correctness proofs.  IType u_6 KType u_7) : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    §3.3, p. 474 "Mutual Authentication" and Theorem 1, §5.2 p. 479:
Peer authentication with identity and key agreement.
If Bob completes a PQXDH session believing he is talking to Alice,
then Alice initiated a matching session with Bob, and both agree on:
  - Identity keys: IKₐ, IKᵦ  (both parties know who they're talking to)
  - Signed prekey: SPKᵦ       (same medium-term key used)
  - One-time prekey: OPKᵦ     (same one-time key used, if present)

This subsumes "data agreement over the shared pre-key" (which the
paper lists as property (6) of Theorem 1).

This is a correspondence assertion in the ProVerif sense, or
an authentication with agreement property in the CryptoVerif
game.

Caveat (Theorem 2): In X25519, which has cofactor 8, agreement
on DH values holds only modulo the small subgroup of order 8. The
paper notes this explicitly: "modulo the subgroup elements of
X25519."
    complete
Definition7.17
Group: Formal security definitions and assumptions for PQXDH, following Bhargavan et al. (USENIX Security 2024). (21)
Hover another entry in this group to preview it.
Preview
Definition 7.1
Blueprint label
  • sig_keypair
Group
  • Formal security definitions and assumptions for PQXDH, following Bhargavan et al. (USENIX Security 2024).
✓L∃∀Nused by 0

Extended peer authentication: Definition 7.16 plus agreement over the post-quantum signed pre-key (PQSPK / KEM public key). Standard peer authentication does not guarantee PQSPK agreement; this stronger property requires the additional SH-CR assumption on the KEM (Theorem 6).

Code for Definition7.17●1 definition
  • def PeerAuthPQ.{u_1, u_2, u_3, u_4, u_5, u_6, u_7} (GType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. )
  [AddCommGroupAddCommGroup.{u} (G : Type u) : Type uAn additive commutative group is an additive group with commutative `(+)`.  GType u_1] (PKType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) (SK_kemType u_3 : Type u_3A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) (CTType u_4 : Type u_4A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. )
  (SSType u_5 : Type u_5A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) (kemKEM PK SK_kem CT SS : KEMKEM.{u_1, u_2, u_3, u_4} (PK : Type u_1) (SK_kem : Type u_2) (CT : Type u_3) (SS : Type u_4) :
  Type (max (max (max u_1 u_2) u_3) u_4)KEM parameterized by public key `PK`, secret key `SK_kem`,
ciphertext `CT`, and shared secret `SS`. The `correctness` field
guarantees that honest encapsulation/decapsulation round-trips.  PKType u_2 SK_kemType u_3 CTType u_4 SSType u_5) (IType u_6 : Type u_6A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. )
  (KType u_7 : Type u_7A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) (kdfKDF I K : KDFKDF.{u_1, u_2} (I : Type u_1) (K : Type u_2) : Type (max u_1 u_2)KDF as a deterministic function, for correctness proofs.  IType u_6 KType u_7) : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    def PeerAuthPQ.{u_1, u_2, u_3, u_4, u_5, u_6,
    u_7}
  (GType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) [AddCommGroupAddCommGroup.{u} (G : Type u) : Type uAn additive commutative group is an additive group with commutative `(+)`.  GType u_1]
  (PKType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) (SK_kemType u_3 : Type u_3A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. )
  (CTType u_4 : Type u_4A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) (SSType u_5 : Type u_5A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. )
  (kemKEM PK SK_kem CT SS : KEMKEM.{u_1, u_2, u_3, u_4} (PK : Type u_1) (SK_kem : Type u_2) (CT : Type u_3) (SS : Type u_4) :
  Type (max (max (max u_1 u_2) u_3) u_4)KEM parameterized by public key `PK`, secret key `SK_kem`,
ciphertext `CT`, and shared secret `SS`. The `correctness` field
guarantees that honest encapsulation/decapsulation round-trips.  PKType u_2 SK_kemType u_3 CTType u_4 SSType u_5)
  (IType u_6 : Type u_6A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) (KType u_7 : Type u_7A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. )
  (kdfKDF I K : KDFKDF.{u_1, u_2} (I : Type u_1) (K : Type u_2) : Type (max u_1 u_2)KDF as a deterministic function, for correctness proofs.  IType u_6 KType u_7) : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    Theorem 6, §5.3.2 p. 480: Extended peer authentication — `PeerAuth` plus
agreement over the post-quantum signed prekey (PQSPK / KEM public key).
Standard `PeerAuth` (Theorem 2) does NOT guarantee PQSPK agreement.
A malicious server could substitute PQSPK without detection (the
re-encapsulation attack). This stronger property requires the
additional SH-CR assumption on the KEM (Theorem 6).

Definitionally the conjunction of `PeerAuth` and `PQSPKAgreement`, so
`PeerAuthPQ_implies_PeerAuth` falls out as `And.left`.
    complete
Theorem7.18
Group: Formal security definitions and assumptions for PQXDH, following Bhargavan et al. (USENIX Security 2024). (21)
Hover another entry in this group to preview it.
Preview
Definition 7.1
Blueprint label
  • sig_keypair
Group
  • Formal security definitions and assumptions for PQXDH, following Bhargavan et al. (USENIX Security 2024).
✓L∃∀Nused by 0
EffortsmallPrioritymediumTagssecurityauthpq

Post-quantum peer authentication implies classical peer authentication.

Code for Theorem7.18●1 theorem
  • theorem PeerAuthPQ_implies_PeerAuth.{u_1, u_2, u_3, u_4, u_5, u_6, u_7}
  (GType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) [AddCommGroupAddCommGroup.{u} (G : Type u) : Type uAn additive commutative group is an additive group with commutative `(+)`.  GType u_1] (PKType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) (SK_kemType u_3 : Type u_3A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. )
  (CTType u_4 : Type u_4A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) (SSType u_5 : Type u_5A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) (kemKEM PK SK_kem CT SS : KEMKEM.{u_1, u_2, u_3, u_4} (PK : Type u_1) (SK_kem : Type u_2) (CT : Type u_3) (SS : Type u_4) :
  Type (max (max (max u_1 u_2) u_3) u_4)KEM parameterized by public key `PK`, secret key `SK_kem`,
ciphertext `CT`, and shared secret `SS`. The `correctness` field
guarantees that honest encapsulation/decapsulation round-trips.  PKType u_2 SK_kemType u_3 CTType u_4 SSType u_5)
  (IType u_6 : Type u_6A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) (KType u_7 : Type u_7A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) (kdfKDF I K : KDFKDF.{u_1, u_2} (I : Type u_1) (K : Type u_2) : Type (max u_1 u_2)KDF as a deterministic function, for correctness proofs.  IType u_6 KType u_7) :
  PeerAuthPQPeerAuthPQ.{u_1, u_2, u_3, u_4, u_5, u_6, u_7} (G : Type u_1) [AddCommGroup G] (PK : Type u_2) (SK_kem : Type u_3)
  (CT : Type u_4) (SS : Type u_5) (kem : KEM PK SK_kem CT SS) (I : Type u_6) (K : Type u_7) (kdf : KDF I K) : PropTheorem 6, §5.3.2 p. 480: Extended peer authentication — `PeerAuth` plus
agreement over the post-quantum signed prekey (PQSPK / KEM public key).
Standard `PeerAuth` (Theorem 2) does NOT guarantee PQSPK agreement.
A malicious server could substitute PQSPK without detection (the
re-encapsulation attack). This stronger property requires the
additional SH-CR assumption on the KEM (Theorem 6).

Definitionally the conjunction of `PeerAuth` and `PQSPKAgreement`, so
`PeerAuthPQ_implies_PeerAuth` falls out as `And.left`.  GType u_1 PKType u_2 SK_kemType u_3 CTType u_4 SSType u_5 kemKEM PK SK_kem CT SS IType u_6 KType u_7 kdfKDF I K →
    PeerAuthPeerAuth.{u_1, u_2, u_3, u_4, u_5, u_6, u_7} (G : Type u_1) [AddCommGroup G] (PK : Type u_2) (SK_kem : Type u_3)
  (CT : Type u_4) (SS : Type u_5) (kem : KEM PK SK_kem CT SS) (I : Type u_6) (K : Type u_7) (kdf : KDF I K) : Prop§3.3, p. 474 "Mutual Authentication" and Theorem 1, §5.2 p. 479:
Peer authentication with identity and key agreement.
If Bob completes a PQXDH session believing he is talking to Alice,
then Alice initiated a matching session with Bob, and both agree on:
  - Identity keys: IKₐ, IKᵦ  (both parties know who they're talking to)
  - Signed prekey: SPKᵦ       (same medium-term key used)
  - One-time prekey: OPKᵦ     (same one-time key used, if present)

This subsumes "data agreement over the shared pre-key" (which the
paper lists as property (6) of Theorem 1).

This is a correspondence assertion in the ProVerif sense, or
an authentication with agreement property in the CryptoVerif
game.

Caveat (Theorem 2): In X25519, which has cofactor 8, agreement
on DH values holds only modulo the small subgroup of order 8. The
paper notes this explicitly: "modulo the subgroup elements of
X25519."  GType u_1 PKType u_2 SK_kemType u_3 CTType u_4 SSType u_5 kemKEM PK SK_kem CT SS IType u_6 KType u_7 kdfKDF I K
    theorem PeerAuthPQ_implies_PeerAuth.{u_1, u_2,
    u_3, u_4, u_5, u_6, u_7}
  (GType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) [AddCommGroupAddCommGroup.{u} (G : Type u) : Type uAn additive commutative group is an additive group with commutative `(+)`.  GType u_1]
  (PKType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) (SK_kemType u_3 : Type u_3A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. )
  (CTType u_4 : Type u_4A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) (SSType u_5 : Type u_5A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. )
  (kemKEM PK SK_kem CT SS : KEMKEM.{u_1, u_2, u_3, u_4} (PK : Type u_1) (SK_kem : Type u_2) (CT : Type u_3) (SS : Type u_4) :
  Type (max (max (max u_1 u_2) u_3) u_4)KEM parameterized by public key `PK`, secret key `SK_kem`,
ciphertext `CT`, and shared secret `SS`. The `correctness` field
guarantees that honest encapsulation/decapsulation round-trips.  PKType u_2 SK_kemType u_3 CTType u_4 SSType u_5)
  (IType u_6 : Type u_6A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) (KType u_7 : Type u_7A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. )
  (kdfKDF I K : KDFKDF.{u_1, u_2} (I : Type u_1) (K : Type u_2) : Type (max u_1 u_2)KDF as a deterministic function, for correctness proofs.  IType u_6 KType u_7) :
  PeerAuthPQPeerAuthPQ.{u_1, u_2, u_3, u_4, u_5, u_6, u_7} (G : Type u_1) [AddCommGroup G] (PK : Type u_2) (SK_kem : Type u_3)
  (CT : Type u_4) (SS : Type u_5) (kem : KEM PK SK_kem CT SS) (I : Type u_6) (K : Type u_7) (kdf : KDF I K) : PropTheorem 6, §5.3.2 p. 480: Extended peer authentication — `PeerAuth` plus
agreement over the post-quantum signed prekey (PQSPK / KEM public key).
Standard `PeerAuth` (Theorem 2) does NOT guarantee PQSPK agreement.
A malicious server could substitute PQSPK without detection (the
re-encapsulation attack). This stronger property requires the
additional SH-CR assumption on the KEM (Theorem 6).

Definitionally the conjunction of `PeerAuth` and `PQSPKAgreement`, so
`PeerAuthPQ_implies_PeerAuth` falls out as `And.left`.  GType u_1 PKType u_2 SK_kemType u_3 CTType u_4 SSType u_5 kemKEM PK SK_kem CT SS IType u_6 KType u_7
      kdfKDF I K →
    PeerAuthPeerAuth.{u_1, u_2, u_3, u_4, u_5, u_6, u_7} (G : Type u_1) [AddCommGroup G] (PK : Type u_2) (SK_kem : Type u_3)
  (CT : Type u_4) (SS : Type u_5) (kem : KEM PK SK_kem CT SS) (I : Type u_6) (K : Type u_7) (kdf : KDF I K) : Prop§3.3, p. 474 "Mutual Authentication" and Theorem 1, §5.2 p. 479:
Peer authentication with identity and key agreement.
If Bob completes a PQXDH session believing he is talking to Alice,
then Alice initiated a matching session with Bob, and both agree on:
  - Identity keys: IKₐ, IKᵦ  (both parties know who they're talking to)
  - Signed prekey: SPKᵦ       (same medium-term key used)
  - One-time prekey: OPKᵦ     (same one-time key used, if present)

This subsumes "data agreement over the shared pre-key" (which the
paper lists as property (6) of Theorem 1).

This is a correspondence assertion in the ProVerif sense, or
an authentication with agreement property in the CryptoVerif
game.

Caveat (Theorem 2): In X25519, which has cofactor 8, agreement
on DH values holds only modulo the small subgroup of order 8. The
paper notes this explicitly: "modulo the subgroup elements of
X25519."  GType u_1 PKType u_2 SK_kemType u_3 CTType u_4 SSType u_5 kemKEM PK SK_kem CT SS IType u_6 KType u_7 kdfKDF I K
    `PeerAuthPQ` implies `PeerAuth`: PQSPK agreement is strictly
stronger, adding one more agreed parameter.
    complete
Definition7.19
Group: Formal security definitions and assumptions for PQXDH, following Bhargavan et al. (USENIX Security 2024). (21)
Hover another entry in this group to preview it.
Preview
Definition 7.1
Blueprint label
  • sig_keypair
Group
  • Formal security definitions and assumptions for PQXDH, following Bhargavan et al. (USENIX Security 2024).
✓L∃∀Nused by 0

Forward secrecy: compromise of long-term keys does not compromise past session keys.

Code for Definition7.19●1 definition
  • opaque ForwardSecrecy.{u_1, u_2, u_3} (GType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) [AddCommGroupAddCommGroup.{u} (G : Type u) : Type uAn additive commutative group is an additive group with commutative `(+)`.  GType u_1]
  (IType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) (KType u_3 : Type u_3A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) (kdfKDF I K : KDFKDF.{u_1, u_2} (I : Type u_1) (K : Type u_2) : Type (max u_1 u_2)KDF as a deterministic function, for correctness proofs.  IType u_2 KType u_3) : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    opaque ForwardSecrecy.{u_1, u_2, u_3}
  (GType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) [AddCommGroupAddCommGroup.{u} (G : Type u) : Type uAn additive commutative group is an additive group with commutative `(+)`.  GType u_1]
  (IType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) (KType u_3 : Type u_3A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. )
  (kdfKDF I K : KDFKDF.{u_1, u_2} (I : Type u_1) (K : Type u_2) : Type (max u_1 u_2)KDF as a deterministic function, for correctness proofs.  IType u_2 KType u_3) : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    §2.4, p. 472 "Forward secrecy" and Theorem 1, §5.2 p. 479:
Forward secrecy — even if all long-term identity keys (IKₐ, IKᵦ)
are compromised after a session completes, the session key
remains indistinguishable from random.

This holds because the session key depends on ephemeral keys (EKₐ)
and medium-term keys (SPKᵦ) that are deleted after use. The
adversary cannot recompute DH3 = DH(ekₐ, SPKᵦ) without the
ephemeral private key ekₐ, which no longer exists.

In the AKE game: `Corrupt` queries issued *after* the test session
completes do not violate freshness.
    complete
Definition7.20
Group: Formal security definitions and assumptions for PQXDH, following Bhargavan et al. (USENIX Security 2024). (21)
Hover another entry in this group to preview it.
Preview
Definition 7.1
Blueprint label
  • sig_keypair
Group
  • Formal security definitions and assumptions for PQXDH, following Bhargavan et al. (USENIX Security 2024).
✓L∃∀Nused by 0

Key Compromise Impersonation resistance: an adversary who compromises Alice's long-term key cannot impersonate Bob to Alice.

Code for Definition7.20●1 definition
  • opaque KCI_Resistance.{u_1} (GType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) [AddCommGroupAddCommGroup.{u} (G : Type u) : Type uAn additive commutative group is an additive group with commutative `(+)`.  GType u_1] : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    opaque KCI_Resistance.{u_1} (GType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. )
  [AddCommGroupAddCommGroup.{u} (G : Type u) : Type uAn additive commutative group is an additive group with commutative `(+)`.  GType u_1] : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    §2.4, p. 472 "Resistance to key compromise impersonation" and Theorem 1, §5.2 p. 479:
Resistance to Key Compromise Impersonation (KCI).

If Alice's long-term identity key ikₐ is compromised, an attacker
can impersonate Alice to others (since they have her signing key).
However, the attacker cannot impersonate Bob to Alice — Alice
can still authenticate Bob, because authenticating Bob requires
Bob's identity key ikᵦ (via DH2), which the attacker does not have.

Formally: compromise of IKₐ does not help the adversary forge a
session where Alice accepts Bob as the peer.

In the AKE game: a `Corrupt(Alice)` query before the test session
does not violate freshness (only `Corrupt(Alice) ∧ Corrupt(Bob)`
before completion violates freshness).
    complete
Definition7.21
Group: Formal security definitions and assumptions for PQXDH, following Bhargavan et al. (USENIX Security 2024). (21)
Hover another entry in this group to preview it.
Preview
Definition 7.1
Blueprint label
  • sig_keypair
Group
  • Formal security definitions and assumptions for PQXDH, following Bhargavan et al. (USENIX Security 2024).
✓L∃∀Nused by 0

Session independence: compromise of one session key does not compromise other session keys.

Code for Definition7.21●1 definition
  • opaque SessionIndependence.{u_1, u_2, u_3} (GType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) [AddCommGroupAddCommGroup.{u} (G : Type u) : Type uAn additive commutative group is an additive group with commutative `(+)`.  GType u_1]
  (IType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) (KType u_3 : Type u_3A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) (kdfKDF I K : KDFKDF.{u_1, u_2} (I : Type u_1) (K : Type u_2) : Type (max u_1 u_2)KDF as a deterministic function, for correctness proofs.  IType u_2 KType u_3) : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    opaque SessionIndependence.{u_1, u_2, u_3}
  (GType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) [AddCommGroupAddCommGroup.{u} (G : Type u) : Type uAn additive commutative group is an additive group with commutative `(+)`.  GType u_1]
  (IType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) (KType u_3 : Type u_3A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. )
  (kdfKDF I K : KDFKDF.{u_1, u_2} (I : Type u_1) (K : Type u_2) : Type (max u_1 u_2)KDF as a deterministic function, for correctness proofs.  IType u_2 KType u_3) : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    §2.4, p. 472 "Session independence" and Theorem 1, §5.2 p. 479:
Session independence — the session key of one session is
independent of all other session keys.

Compromise of a session key SK_i (via `RevealSessionKey`) does not
help the adversary attack a different session SK_j, provided the
ephemeral keys are independently generated.

In the AKE game: the adversary may `RevealSessionKey` on any
session except the test session (and its partner), and still
cannot distinguish the test session's key from random.
    complete
Definition7.22
Group: Formal security definitions and assumptions for PQXDH, following Bhargavan et al. (USENIX Security 2024). (21)
Hover another entry in this group to preview it.
Preview
Definition 7.1
Blueprint label
  • sig_keypair
Group
  • Formal security definitions and assumptions for PQXDH, following Bhargavan et al. (USENIX Security 2024).
✓L∃∀Nused by 0

Harvest-Now-Decrypt-Later resistance: a quantum adversary who records classical transcripts today cannot decrypt them after obtaining a quantum computer, thanks to the KEM layer.

Code for Definition7.22●1 definition
  • opaque HNDL_Resistance.{u_1, u_2, u_3, u_4, u_5, u_6, u_7} (GType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. )
  [AddCommGroupAddCommGroup.{u} (G : Type u) : Type uAn additive commutative group is an additive group with commutative `(+)`.  GType u_1] (PKType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) (SK_kemType u_3 : Type u_3A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) (CTType u_4 : Type u_4A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. )
  (SSType u_5 : Type u_5A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) (kemKEM PK SK_kem CT SS : KEMKEM.{u_1, u_2, u_3, u_4} (PK : Type u_1) (SK_kem : Type u_2) (CT : Type u_3) (SS : Type u_4) :
  Type (max (max (max u_1 u_2) u_3) u_4)KEM parameterized by public key `PK`, secret key `SK_kem`,
ciphertext `CT`, and shared secret `SS`. The `correctness` field
guarantees that honest encapsulation/decapsulation round-trips.  PKType u_2 SK_kemType u_3 CTType u_4 SSType u_5) (IType u_6 : Type u_6A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. )
  (KType u_7 : Type u_7A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) (kdfKDF I K : KDFKDF.{u_1, u_2} (I : Type u_1) (K : Type u_2) : Type (max u_1 u_2)KDF as a deterministic function, for correctness proofs.  IType u_6 KType u_7) : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    opaque HNDL_Resistance.{u_1, u_2, u_3, u_4, u_5,
    u_6, u_7}
  (GType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) [AddCommGroupAddCommGroup.{u} (G : Type u) : Type uAn additive commutative group is an additive group with commutative `(+)`.  GType u_1]
  (PKType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) (SK_kemType u_3 : Type u_3A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. )
  (CTType u_4 : Type u_4A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) (SSType u_5 : Type u_5A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. )
  (kemKEM PK SK_kem CT SS : KEMKEM.{u_1, u_2, u_3, u_4} (PK : Type u_1) (SK_kem : Type u_2) (CT : Type u_3) (SS : Type u_4) :
  Type (max (max (max u_1 u_2) u_3) u_4)KEM parameterized by public key `PK`, secret key `SK_kem`,
ciphertext `CT`, and shared secret `SS`. The `correctness` field
guarantees that honest encapsulation/decapsulation round-trips.  PKType u_2 SK_kemType u_3 CTType u_4 SSType u_5)
  (IType u_6 : Type u_6A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) (KType u_7 : Type u_7A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. )
  (kdfKDF I K : KDFKDF.{u_1, u_2} (I : Type u_1) (K : Type u_2) : Type (max u_1 u_2)KDF as a deterministic function, for correctness proofs.  IType u_6 KType u_7) : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    §2.4, p. 472 "HNDL protection" and Theorem 3, §5.2 p. 479:
Harvest-Now-Decrypt-Later (HNDL) resistance.

A *passive* quantum adversary who records all ciphertexts today
(including DH public keys and KEM ciphertexts) cannot recover
session keys in the future when a quantum computer becomes
available, provided the KEM remains secure (IND-CCA).

Formally: the adversary is given the power to compute discrete
logarithms (break DH) at some future time t_q. For any session
completed before t_q, if the KEM shared secret ss was part of
the KDF input, the session key remains indistinguishable from
random.

This is the core post-quantum guarantee of PQXDH over X3DH:
the KEM shared secret provides a "quantum-resistant backup" that
protects the session key even when all DH values are computable.
    complete