theorem PQXDH_symbolic_security.{u_1, u_2, u_3,
    u_4, u_5, u_6}
  {GType u_5 : Type u_5A 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_5]
  {PK_kemType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } {SK_kemType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  {CT_kemType u_3 : Type u_3A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } {SSType u_4 : Type u_4A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  {SK_sessionType u_6 : Type u_6A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  (kemKEM PK_kem SK_kem CT_kem 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.  PK_kemType u_1 SK_kemType u_2 CT_kemType u_3 SSType u_4)
  (kdfKDF ((G × G × G × G) × SS) SK_session :
    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.  (Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`.(Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`.GType u_5 ×Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. GType u_5 ×Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. GType u_5 ×Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. GType u_5)Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. ×Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. SSType u_4)Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. SK_sessionType u_6)
  (_adversaryDolevYao : DolevYaoDolevYao : Type§3.1, p. 473 and §3.4, p. 474: The Dolev-Yao adversary model (symbolic/ProVerif).

A marker type indicating the analysis is carried out in the symbolic
model, where:
  - The adversary controls the network (active MitM): it can
    intercept, inject, replay, and modify all messages.
  - Cryptographic primitives are ideal black boxes — the
    adversary cannot break encryption, forge signatures, or invert
    hashes except by using the appropriate key.
  - The adversary may compromise long-term keys at any time
    (adaptive corruption).

Security properties are expressed as correspondence assertions:
  "if event A occurred (e.g. Bob completed a session with Alice),
   then event B must have occurred (e.g. Alice initiated it)."

In the post-quantum extension, the adversary is additionally given
the power to break DH (compute discrete logs) at some point in
time, modeling a future quantum computer. Security of sessions
completed *before* this point is then analyzed.

Since all primitives are ideal, no computational hardness
assumptions appear as hypotheses in the symbolic model.
Theorem 1 depends only on the protocol logic. ) :
  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_5 PK_kemType u_1 SK_kemType u_2 CT_kemType u_3 SSType u_4 kemKEM PK_kem SK_kem CT_kem SS
      (Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`.(Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`.GType u_5 ×Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. GType u_5 ×Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. GType u_5 ×Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. GType u_5)Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. ×Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. SSType u_4)Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. SK_sessionType u_6
      kdfKDF ((G × G × G × G) × SS) SK_session ∧And (a b : Prop) : Prop`And a b`, or `a ∧ b`, is the conjunction of propositions. It can be
constructed and destructed like a pair: if `ha : a` and `hb : b` then
`⟨ha, hb⟩ : a ∧ b`, and if `h : a ∧ b` then `h.left : a` and `h.right : b`.


Conventions for notations in identifiers:

 * The recommended spelling of `∧` in identifiers is `and`.

 * The recommended spelling of `/\` in identifiers is `and` (prefer `∧` over `/\`).
    ForwardSecrecyForwardSecrecy.{u_1, u_2, u_3} (G : Type u_1) [AddCommGroup G] (I : Type u_2) (K : Type u_3) (kdf : KDF I K) : Prop§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.  GType u_5
        (Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`.(Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`.GType u_5 ×Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. GType u_5 ×Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. GType u_5 ×Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. GType u_5)Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. ×Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. SSType u_4)Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. SK_sessionType u_6
        kdfKDF ((G × G × G × G) × SS) SK_session ∧And (a b : Prop) : Prop`And a b`, or `a ∧ b`, is the conjunction of propositions. It can be
constructed and destructed like a pair: if `ha : a` and `hb : b` then
`⟨ha, hb⟩ : a ∧ b`, and if `h : a ∧ b` then `h.left : a` and `h.right : b`.


Conventions for notations in identifiers:

 * The recommended spelling of `∧` in identifiers is `and`.

 * The recommended spelling of `/\` in identifiers is `and` (prefer `∧` over `/\`).
      KCI_ResistanceKCI_Resistance.{u_1} (G : Type u_1) [AddCommGroup G] : Prop§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).  GType u_5 ∧And (a b : Prop) : Prop`And a b`, or `a ∧ b`, is the conjunction of propositions. It can be
constructed and destructed like a pair: if `ha : a` and `hb : b` then
`⟨ha, hb⟩ : a ∧ b`, and if `h : a ∧ b` then `h.left : a` and `h.right : b`.


Conventions for notations in identifiers:

 * The recommended spelling of `∧` in identifiers is `and`.

 * The recommended spelling of `/\` in identifiers is `and` (prefer `∧` over `/\`).
        SessionIndependenceSessionIndependence.{u_1, u_2, u_3} (G : Type u_1) [AddCommGroup G] (I : Type u_2) (K : Type u_3) (kdf : KDF I K) : Prop§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.  GType u_5
            (Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`.(Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`.GType u_5 ×Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. GType u_5 ×Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. GType u_5 ×Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. GType u_5)Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. ×Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. SSType u_4)Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`.
            SK_sessionType u_6 kdfKDF ((G × G × G × G) × SS) SK_session ∧And (a b : Prop) : Prop`And a b`, or `a ∧ b`, is the conjunction of propositions. It can be
constructed and destructed like a pair: if `ha : a` and `hb : b` then
`⟨ha, hb⟩ : a ∧ b`, and if `h : a ∧ b` then `h.left : a` and `h.right : b`.


Conventions for notations in identifiers:

 * The recommended spelling of `∧` in identifiers is `and`.

 * The recommended spelling of `/\` in identifiers is `and` (prefer `∧` over `/\`).
          HNDL_ResistanceHNDL_Resistance.{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§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.  GType u_5 PK_kemType u_1 SK_kemType u_2
            CT_kemType u_3 SSType u_4 kemKEM PK_kem SK_kem CT_kem SS
            (Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`.(Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`.GType u_5 ×Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. GType u_5 ×Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. GType u_5 ×Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. GType u_5)Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. ×Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. SSType u_4)Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`.
            SK_sessionType u_6 kdfKDF ((G × G × G × G) × SS) SK_session

theorem PQXDH_classical_security.{u_1, u_2, u_3,
    u_4, u_5, u_6, u_7, u_8, u_9, u_10,
    u_11, u_12, u_13}
  {GType u_5 : Type u_5A 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_5]
  {PK_kemType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } {SK_kemType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  {CT_kemType u_3 : Type u_3A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } {SSType u_4 : Type u_4A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  {PK_sigType u_10 : Type u_10A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  {SK_sigType u_11 : Type u_11A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } {MType u_12 : Type u_12A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  {S_sigType u_13 : Type u_13A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  {SK_sessionType u_6 : Type u_6A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } {PTType u_7 : Type u_7A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  {CT_aeadType u_8 : Type u_8A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } {ADType u_9 : Type u_9A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  (G₀G : GType u_5)
  (kemKEM PK_kem SK_kem CT_kem 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.  PK_kemType u_1 SK_kemType u_2 CT_kemType u_3 SSType u_4)
  (kdfKDF ((G × G × G × G) × SS) SK_session :
    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.  (Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`.(Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`.GType u_5 ×Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. GType u_5 ×Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. GType u_5 ×Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. GType u_5)Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. ×Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. SSType u_4)Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. SK_sessionType u_6)
  (aeadAEAD SK_session PT CT_aead AD : AEADAEAD.{u_1, u_2, u_3, u_4} (K : Type u_1) (PT : Type u_2) (CT : Type u_3) (AD : Type u_4) :
  Type (max (max (max u_1 u_2) u_3) u_4)AEAD scheme parameterized by key `K`, plaintext `PT`, ciphertext `CT`,
and associated data `AD`. The `correctness` field guarantees that decrypting
an honestly encrypted ciphertext with the correct key and AD recovers the
original plaintext.  SK_sessionType u_6 PTType u_7 CT_aeadType u_8 ADType u_9)
  (sigSig PK_sig SK_sig M S_sig : SigSig.{u_1, u_2, u_3, u_4} (PK_sig : Type u_1) (SK_sig : Type u_2) (M : Type u_3) (S : Type u_4) :
  Type (max (max (max u_1 u_2) u_3) u_4)§2.5, p. 472 assumption 2 and Figure 1, p. 471: Abstract digital signature
scheme. The paper uses "the signature Sig (XEdDSA), is EUF-CMA" (§2.5, p. 472).
In Figure 1, Alice verifies "sign(SPKᵦᵖᵏ, IKᵦˢᵏ), sign(PQSPKᵦᵖᵏ, IKᵦˢᵏ)".
Correctness requires that honestly generated signatures verify under the matching
public key. Concrete instantiation: XEdDSA over Curve25519.  PK_sigType u_10 SK_sigType u_11 MType u_12 S_sigType u_13)
  (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. )
  (h_gapdhGapDH_Hard G G₀ : GapDH_HardGapDH_Hard.{u_1} (G : Type u_1) [AddCommGroup G] (_gen : G) : Prop§2.5, p. 472, assumption 1.A: the gap Diffie-Hellman (gapDH) problem is
hard on X25519.

Game: The challenger samples a, b ←$ ℤ_q and gives the adversary
(G, [a]·G, [b]·G) plus access to a DDH oracle (which, on input
(U, V, W), returns whether W = DH(u, V) for the unknown u).
The adversary must compute [ab]·G.

gapDH is stronger than CDH (the DDH oracle helps) but the protocol
proof requires it because CryptoVerif uses DDH-like transitions
internally. The concrete group is X25519 (Curve25519).

Security means: no efficient adversary computes the answer with
non-negligible probability.  GType u_5 G₀G)
  (h_kdf_roKDF_RandomOracle ((G × G × G × G) × SS) SK_session kdf :
    KDF_RandomOracleKDF_RandomOracle.{u_1, u_2} (I : Type u_1) (K : Type u_2) (kdf : KDF I K) : Prop§2.5, p. 473, assumption 4: the KDF is a Random Oracle (classical variant).

Model: The KDF is replaced by a truly random function — for each
new input, the output is sampled uniformly at random; repeated queries
with the same input return the same output.

This is the standard ROM (Random Oracle Model) assumption used in
the classical CryptoVerif proof. It is stronger than PRF but allows
a tighter reduction.

Concrete instantiation: HKDF-SHA-256 (RFC 5869). 
      (Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`.(Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`.GType u_5 ×Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. GType u_5 ×Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. GType u_5 ×Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. GType u_5)Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. ×Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. SSType u_4)Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. SK_sessionType u_6
      kdfKDF ((G × G × G × G) × SS) SK_session)
  (h_aeadAEAD_IND_CPA_INT_CTXT SK_session PT CT_aead AD aead :
    AEAD_IND_CPA_INT_CTXTAEAD_IND_CPA_INT_CTXT.{u_1, u_2, u_3, u_4} (K : Type u_1) (PT : Type u_2) (CT : Type u_3) (AD : Type u_4)
  (aead : AEAD K PT CT AD) : Prop§2.5, p. 472, assumption 3: the AEAD scheme is IND-CPA + INT-CTXT.

This is a conjunction of two standard security notions:

IND-CPA (indistinguishability under chosen-plaintext attack):
Adversary chooses two plaintexts; receives encryption of one
(chosen by coin flip); must guess which. Security means the
advantage is negligible.

INT-CTXT (integrity of ciphertext):
Adversary has access to an encryption oracle; must produce a
new valid ciphertext (one not output by the oracle). Security
means the probability of success is negligible.

Together, IND-CPA + INT-CTXT imply IND-CCA2 (Bellare & Namprempre).

Concrete instantiation: AES-256-CBC + HMAC in Encrypt-Then-MAC mode.  SK_sessionType u_6 PTType u_7
      CT_aeadType u_8 ADType u_9 aeadAEAD SK_session PT CT_aead AD)
  (h_sigSig_EUF_CMA PK_sig SK_sig M S_sig sig :
    Sig_EUF_CMASig_EUF_CMA.{u_1, u_2, u_3, u_4} (PK_sig : Type u_1) (SK_sig : Type u_2) (M : Type u_3) (S : Type u_4)
  (sig : Sig PK_sig SK_sig M S) : Prop§2.5, p. 472, assumption 2: the signature scheme is EUF-CMA (existentially
unforgeable under chosen-message attack).

Game:
  1. Challenger runs (pk, sk) ← Sig.keygen, gives pk to adversary.
  2. Adversary adaptively queries a signing oracle Sign(sk, ·),
     receiving signatures on messages of its choice.
  3. Adversary outputs (m*, σ*) where m* was never queried.

Security means: Pr[Verify(pk, m*, σ*) = true] is negligible.

Concrete instantiation: XEdDSA over Curve25519.  PK_sigType u_10 SK_sigType u_11 MType u_12 S_sigType u_13
      sigSig PK_sig SK_sig M S_sig) :
  MessageSecrecyMessageSecrecy.{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)
  (fresh : Freshness) : Prop§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)`.  GType u_5 PK_kemType u_1 SK_kemType u_2 CT_kemType u_3 SSType u_4
      kemKEM PK_kem SK_kem CT_kem SS (Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`.(Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`.GType u_5 ×Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. GType u_5 ×Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. GType u_5 ×Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. GType u_5)Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. ×Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. SSType u_4)Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`.
      SK_sessionType u_6 kdfKDF ((G × G × G × G) × SS) SK_session freshFreshness ∧And (a b : Prop) : Prop`And a b`, or `a ∧ b`, is the conjunction of propositions. It can be
constructed and destructed like a pair: if `ha : a` and `hb : b` then
`⟨ha, hb⟩ : a ∧ b`, and if `h : a ∧ b` then `h.left : a` and `h.right : b`.


Conventions for notations in identifiers:

 * The recommended spelling of `∧` in identifiers is `and`.

 * The recommended spelling of `/\` in identifiers is `and` (prefer `∧` over `/\`).
    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_5 PK_kemType u_1 SK_kemType u_2 CT_kemType u_3 SSType u_4 kemKEM PK_kem SK_kem CT_kem SS
      (Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`.(Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`.GType u_5 ×Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. GType u_5 ×Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. GType u_5 ×Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. GType u_5)Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. ×Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. SSType u_4)Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. SK_sessionType u_6
      kdfKDF ((G × G × G × G) × SS) SK_session

theorem PQXDH_postquantum_security.{u_1, u_2, u_3,
    u_4, u_5, u_6, u_7, u_8, u_9, u_10,
    u_11, u_12, u_13}
  {GType u_5 : Type u_5A 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_5]
  {PK_kemType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } {SK_kemType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  {CT_kemType u_3 : Type u_3A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } {SSType u_4 : Type u_4A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  {PK_sigType u_10 : Type u_10A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  {SK_sigType u_11 : Type u_11A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } {MType u_12 : Type u_12A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  {S_sigType u_13 : Type u_13A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  {SK_sessionType u_6 : Type u_6A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } {PTType u_7 : Type u_7A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  {CT_aeadType u_8 : Type u_8A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } {ADType u_9 : Type u_9A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  (kemKEM PK_kem SK_kem CT_kem 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.  PK_kemType u_1 SK_kemType u_2 CT_kemType u_3 SSType u_4)
  (kdfKDF ((G × G × G × G) × SS) SK_session :
    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.  (Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`.(Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`.GType u_5 ×Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. GType u_5 ×Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. GType u_5 ×Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. GType u_5)Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. ×Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. SSType u_4)Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. SK_sessionType u_6)
  (aeadAEAD SK_session PT CT_aead AD : AEADAEAD.{u_1, u_2, u_3, u_4} (K : Type u_1) (PT : Type u_2) (CT : Type u_3) (AD : Type u_4) :
  Type (max (max (max u_1 u_2) u_3) u_4)AEAD scheme parameterized by key `K`, plaintext `PT`, ciphertext `CT`,
and associated data `AD`. The `correctness` field guarantees that decrypting
an honestly encrypted ciphertext with the correct key and AD recovers the
original plaintext.  SK_sessionType u_6 PTType u_7 CT_aeadType u_8 ADType u_9)
  (sigSig PK_sig SK_sig M S_sig : SigSig.{u_1, u_2, u_3, u_4} (PK_sig : Type u_1) (SK_sig : Type u_2) (M : Type u_3) (S : Type u_4) :
  Type (max (max (max u_1 u_2) u_3) u_4)§2.5, p. 472 assumption 2 and Figure 1, p. 471: Abstract digital signature
scheme. The paper uses "the signature Sig (XEdDSA), is EUF-CMA" (§2.5, p. 472).
In Figure 1, Alice verifies "sign(SPKᵦᵖᵏ, IKᵦˢᵏ), sign(PQSPKᵦᵖᵏ, IKᵦˢᵏ)".
Correctness requires that honestly generated signatures verify under the matching
public key. Concrete instantiation: XEdDSA over Curve25519.  PK_sigType u_10 SK_sigType u_11 MType u_12 S_sigType u_13)
  (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. )
  (h_kem_ccaKEM_IND_CCA PK_kem SK_kem CT_kem SS kem :
    KEM_IND_CCAKEM_IND_CCA.{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)
  (kem : KEM PK SK_kem CT SS) : Prop§2.5, p. 472, assumption 1.B: the KEM is IND-CCA (indistinguishable under
chosen-ciphertext attack). "Or the PQ-KEM (Kyber1024) is IND-CCA".

Game:
  1. Challenger runs (pk, sk) ← KEM.keygen.
  2. Challenger computes (ss₀, ct*) ← KEM.encaps(pk), samples ss₁ ←$ SS.
  3. Challenger flips coin b ∈ {0,1}, gives adversary (pk, ct*, ssᵦ).
  4. Adversary has access to a decapsulation oracle KEM.decaps(sk, ·)
     for any ciphertext ct ≠ ct*.
  5. Adversary outputs guess b'.

Security means: |Pr[b' = b] − 1/2| is negligible.
Concrete instantiation: Kyber-1024 (ML-KEM), secure under Module-LWE.  PK_kemType u_1 SK_kemType u_2 CT_kemType u_3 SSType u_4
      kemKEM PK_kem SK_kem CT_kem SS)
  (h_kdf_prfKDF_PRF ((G × G × G × G) × SS) SK_session kdf :
    KDF_PRFKDF_PRF.{u_1, u_2} (I : Type u_1) (K : Type u_2) (kdf : KDF I K) : Prop§2.5, p. 473 and §3.5, p. 475: the KDF is a PRF (post-quantum variant).
(pseudorandom function).

Game:
  1. Challenger samples a key k ←$ K and flips coin b ∈ {0,1}.
  2. If b = 0, the oracle returns KDF.derive(k, ·).
     If b = 1, the oracle returns a truly random function f(·).
  3. Adversary queries the oracle adaptively and outputs guess b'.

Security means: |Pr[b' = b] − 1/2| is negligible.

The post-quantum CryptoVerif proof uses PRF instead of ROM because
CryptoVerif's post-quantum soundness result does not capture the
Quantum Random Oracle Model (QROM). PRF suffices for the
post-quantum secrecy guarantee.  (Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`.(Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`.GType u_5 ×Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. GType u_5 ×Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. GType u_5 ×Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. GType u_5)Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. ×Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. SSType u_4)Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`.
      SK_sessionType u_6 kdfKDF ((G × G × G × G) × SS) SK_session)
  (h_aeadAEAD_IND_CPA_INT_CTXT SK_session PT CT_aead AD aead :
    AEAD_IND_CPA_INT_CTXTAEAD_IND_CPA_INT_CTXT.{u_1, u_2, u_3, u_4} (K : Type u_1) (PT : Type u_2) (CT : Type u_3) (AD : Type u_4)
  (aead : AEAD K PT CT AD) : Prop§2.5, p. 472, assumption 3: the AEAD scheme is IND-CPA + INT-CTXT.

This is a conjunction of two standard security notions:

IND-CPA (indistinguishability under chosen-plaintext attack):
Adversary chooses two plaintexts; receives encryption of one
(chosen by coin flip); must guess which. Security means the
advantage is negligible.

INT-CTXT (integrity of ciphertext):
Adversary has access to an encryption oracle; must produce a
new valid ciphertext (one not output by the oracle). Security
means the probability of success is negligible.

Together, IND-CPA + INT-CTXT imply IND-CCA2 (Bellare & Namprempre).

Concrete instantiation: AES-256-CBC + HMAC in Encrypt-Then-MAC mode.  SK_sessionType u_6 PTType u_7
      CT_aeadType u_8 ADType u_9 aeadAEAD SK_session PT CT_aead AD)
  (h_sig_at_exchangeHeldAtExchange (Sig_EUF_CMA PK_sig SK_sig M S_sig sig) :
    HeldAtExchangeHeldAtExchange (assumption : Prop) : PropTemporal qualification for a cryptographic assumption: the
assumption held at the time the key exchange completed, but
may have been broken since (e.g. by a quantum computer).

In Theorem 3, the paper requires that the signature scheme was
EUF-CMA at the time Alice and Bob ran the protocol. The adversary
may later gain the ability to forge signatures (via a quantum
computer), but this does not retroactively compromise sessions
that were already established under valid signatures.

We distinguish this from the atemporal `Sig_EUF_CMA` used in
Theorem 2, where the assumption is required to hold throughout. 
      (Sig_EUF_CMASig_EUF_CMA.{u_1, u_2, u_3, u_4} (PK_sig : Type u_1) (SK_sig : Type u_2) (M : Type u_3) (S : Type u_4)
  (sig : Sig PK_sig SK_sig M S) : Prop§2.5, p. 472, assumption 2: the signature scheme is EUF-CMA (existentially
unforgeable under chosen-message attack).

Game:
  1. Challenger runs (pk, sk) ← Sig.keygen, gives pk to adversary.
  2. Adversary adaptively queries a signing oracle Sign(sk, ·),
     receiving signatures on messages of its choice.
  3. Adversary outputs (m*, σ*) where m* was never queried.

Security means: Pr[Verify(pk, m*, σ*) = true] is negligible.

Concrete instantiation: XEdDSA over Curve25519.  PK_sigType u_10 SK_sigType u_11 MType u_12 S_sigType u_13
        sigSig PK_sig SK_sig M S_sig)) :
  HNDL_ResistanceHNDL_Resistance.{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§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.  GType u_5 PK_kemType u_1 SK_kemType u_2 CT_kemType u_3
    SSType u_4 kemKEM PK_kem SK_kem CT_kem SS (Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`.(Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`.GType u_5 ×Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. GType u_5 ×Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. GType u_5 ×Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. GType u_5)Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. ×Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. SSType u_4)Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`.
    SK_sessionType u_6 kdfKDF ((G × G × G × G) × SS) SK_session

theorem Kyber_SH_CR.{u_1, u_2, u_3, u_4}
  {PK_kemType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } {SK_kemType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  {CT_kemType u_3 : Type u_3A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } {SSType u_4 : Type u_4A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  (kemKEM PK_kem SK_kem CT_kem 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.  PK_kemType u_1 SK_kemType u_2 CT_kemType u_3 SSType u_4)
  (h_hash_romKEM_InternalHash_ROM PK_kem SK_kem CT_kem SS kem :
    KEM_InternalHash_ROMKEM_InternalHash_ROM.{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)
  (kem : KEM PK SK_kem CT SS) : Prop§5.3.2, p. 480, Theorem 5 hypothesis: Kyber's internal hash functions (H, G,
XOF) behave as Random Oracles.

This is distinct from `KDF_RandomOracle` — it concerns the hash
functions *inside* the KEM construction (Kyber/ML-KEM), not the
protocol-level KDF. The paper proves that Kyber satisfies SH-CR
under this assumption.  PK_kemType u_1 SK_kemType u_2
      CT_kemType u_3 SSType u_4 kemKEM PK_kem SK_kem CT_kem SS) :
  KEM_SH_CRKEM_SH_CR.{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)
  (kem : KEM PK SK_kem CT SS) : PropDefinition 1, §5.3.1, p. 480: Semi-Honest Collision Resistance (SH-CR).

Game (2 phases):

  Setup: Challenger runs (pk, sk) ← KEM.keygen.

  Phase 1: Adversary receives sk (the "semi-honest" party's
  compromised secret key). Adversary outputs an arbitrary public
  key pk' (possibly ≠ pk).

  Challenge: Challenger computes (ss, ct) ← KEM.encaps(pk').
  Adversary receives ct.

  Phase 2: Adversary outputs ct'.

  Winning condition: ct' ≠ ct ∧ KEM.decaps(sk, ct') = ss.

That is: the adversary, knowing sk, finds a *different* ciphertext
ct' that decapsulates (under the honest sk) to the same shared
secret ss that was encapsulated under the adversary-chosen pk'.

Security means: the probability of winning is negligible.

Formally:
  Adv^{SH-CR}_{KEM}(A) =
    Pr[ (pk,sk) ← keygen;
        pk' ← A(sk);
        (ss, ct) ← encaps(pk');
        ct' ← A(ct)
      : ct' ≠ ct ∧ decaps(sk, ct') = ss ]
 PK_kemType u_1 SK_kemType u_2 CT_kemType u_3 SSType u_4 kemKEM PK_kem SK_kem CT_kem SS

theorem PQXDH_KEM_pubkey_agreement.{u_1, u_2, u_3,
    u_4, u_5, u_6, u_7, u_8, u_9, u_10,
    u_11, u_12, u_13}
  {GType u_5 : Type u_5A 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_5]
  {PK_kemType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } {SK_kemType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  {CT_kemType u_3 : Type u_3A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } {SSType u_4 : Type u_4A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  {PK_sigType u_10 : Type u_10A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  {SK_sigType u_11 : Type u_11A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } {MType u_12 : Type u_12A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  {S_sigType u_13 : Type u_13A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  {SK_sessionType u_6 : Type u_6A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } {PTType u_7 : Type u_7A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  {CT_aeadType u_8 : Type u_8A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } {ADType u_9 : Type u_9A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  (G₀G : GType u_5)
  (kemKEM PK_kem SK_kem CT_kem 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.  PK_kemType u_1 SK_kemType u_2 CT_kemType u_3 SSType u_4)
  (kdfKDF ((G × G × G × G) × SS) SK_session :
    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.  (Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`.(Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`.GType u_5 ×Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. GType u_5 ×Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. GType u_5 ×Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. GType u_5)Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. ×Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. SSType u_4)Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. SK_sessionType u_6)
  (aeadAEAD SK_session PT CT_aead AD : AEADAEAD.{u_1, u_2, u_3, u_4} (K : Type u_1) (PT : Type u_2) (CT : Type u_3) (AD : Type u_4) :
  Type (max (max (max u_1 u_2) u_3) u_4)AEAD scheme parameterized by key `K`, plaintext `PT`, ciphertext `CT`,
and associated data `AD`. The `correctness` field guarantees that decrypting
an honestly encrypted ciphertext with the correct key and AD recovers the
original plaintext.  SK_sessionType u_6 PTType u_7 CT_aeadType u_8 ADType u_9)
  (sigSig PK_sig SK_sig M S_sig : SigSig.{u_1, u_2, u_3, u_4} (PK_sig : Type u_1) (SK_sig : Type u_2) (M : Type u_3) (S : Type u_4) :
  Type (max (max (max u_1 u_2) u_3) u_4)§2.5, p. 472 assumption 2 and Figure 1, p. 471: Abstract digital signature
scheme. The paper uses "the signature Sig (XEdDSA), is EUF-CMA" (§2.5, p. 472).
In Figure 1, Alice verifies "sign(SPKᵦᵖᵏ, IKᵦˢᵏ), sign(PQSPKᵦᵖᵏ, IKᵦˢᵏ)".
Correctness requires that honestly generated signatures verify under the matching
public key. Concrete instantiation: XEdDSA over Curve25519.  PK_sigType u_10 SK_sigType u_11 MType u_12 S_sigType u_13)
  (h_gapdhGapDH_Hard G G₀ : GapDH_HardGapDH_Hard.{u_1} (G : Type u_1) [AddCommGroup G] (_gen : G) : Prop§2.5, p. 472, assumption 1.A: the gap Diffie-Hellman (gapDH) problem is
hard on X25519.

Game: The challenger samples a, b ←$ ℤ_q and gives the adversary
(G, [a]·G, [b]·G) plus access to a DDH oracle (which, on input
(U, V, W), returns whether W = DH(u, V) for the unknown u).
The adversary must compute [ab]·G.

gapDH is stronger than CDH (the DDH oracle helps) but the protocol
proof requires it because CryptoVerif uses DDH-like transitions
internally. The concrete group is X25519 (Curve25519).

Security means: no efficient adversary computes the answer with
non-negligible probability.  GType u_5 G₀G)
  (h_kdf_roKDF_RandomOracle ((G × G × G × G) × SS) SK_session kdf :
    KDF_RandomOracleKDF_RandomOracle.{u_1, u_2} (I : Type u_1) (K : Type u_2) (kdf : KDF I K) : Prop§2.5, p. 473, assumption 4: the KDF is a Random Oracle (classical variant).

Model: The KDF is replaced by a truly random function — for each
new input, the output is sampled uniformly at random; repeated queries
with the same input return the same output.

This is the standard ROM (Random Oracle Model) assumption used in
the classical CryptoVerif proof. It is stronger than PRF but allows
a tighter reduction.

Concrete instantiation: HKDF-SHA-256 (RFC 5869). 
      (Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`.(Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`.GType u_5 ×Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. GType u_5 ×Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. GType u_5 ×Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. GType u_5)Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. ×Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. SSType u_4)Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. SK_sessionType u_6
      kdfKDF ((G × G × G × G) × SS) SK_session)
  (h_aeadAEAD_IND_CPA_INT_CTXT SK_session PT CT_aead AD aead :
    AEAD_IND_CPA_INT_CTXTAEAD_IND_CPA_INT_CTXT.{u_1, u_2, u_3, u_4} (K : Type u_1) (PT : Type u_2) (CT : Type u_3) (AD : Type u_4)
  (aead : AEAD K PT CT AD) : Prop§2.5, p. 472, assumption 3: the AEAD scheme is IND-CPA + INT-CTXT.

This is a conjunction of two standard security notions:

IND-CPA (indistinguishability under chosen-plaintext attack):
Adversary chooses two plaintexts; receives encryption of one
(chosen by coin flip); must guess which. Security means the
advantage is negligible.

INT-CTXT (integrity of ciphertext):
Adversary has access to an encryption oracle; must produce a
new valid ciphertext (one not output by the oracle). Security
means the probability of success is negligible.

Together, IND-CPA + INT-CTXT imply IND-CCA2 (Bellare & Namprempre).

Concrete instantiation: AES-256-CBC + HMAC in Encrypt-Then-MAC mode.  SK_sessionType u_6 PTType u_7
      CT_aeadType u_8 ADType u_9 aeadAEAD SK_session PT CT_aead AD)
  (h_sigSig_EUF_CMA PK_sig SK_sig M S_sig sig :
    Sig_EUF_CMASig_EUF_CMA.{u_1, u_2, u_3, u_4} (PK_sig : Type u_1) (SK_sig : Type u_2) (M : Type u_3) (S : Type u_4)
  (sig : Sig PK_sig SK_sig M S) : Prop§2.5, p. 472, assumption 2: the signature scheme is EUF-CMA (existentially
unforgeable under chosen-message attack).

Game:
  1. Challenger runs (pk, sk) ← Sig.keygen, gives pk to adversary.
  2. Adversary adaptively queries a signing oracle Sign(sk, ·),
     receiving signatures on messages of its choice.
  3. Adversary outputs (m*, σ*) where m* was never queried.

Security means: Pr[Verify(pk, m*, σ*) = true] is negligible.

Concrete instantiation: XEdDSA over Curve25519.  PK_sigType u_10 SK_sigType u_11 MType u_12 S_sigType u_13 sigSig PK_sig SK_sig M S_sig)
  (h_shcrKEM_SH_CR PK_kem SK_kem CT_kem SS kem :
    KEM_SH_CRKEM_SH_CR.{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)
  (kem : KEM PK SK_kem CT SS) : PropDefinition 1, §5.3.1, p. 480: Semi-Honest Collision Resistance (SH-CR).

Game (2 phases):

  Setup: Challenger runs (pk, sk) ← KEM.keygen.

  Phase 1: Adversary receives sk (the "semi-honest" party's
  compromised secret key). Adversary outputs an arbitrary public
  key pk' (possibly ≠ pk).

  Challenge: Challenger computes (ss, ct) ← KEM.encaps(pk').
  Adversary receives ct.

  Phase 2: Adversary outputs ct'.

  Winning condition: ct' ≠ ct ∧ KEM.decaps(sk, ct') = ss.

That is: the adversary, knowing sk, finds a *different* ciphertext
ct' that decapsulates (under the honest sk) to the same shared
secret ss that was encapsulated under the adversary-chosen pk'.

Security means: the probability of winning is negligible.

Formally:
  Adv^{SH-CR}_{KEM}(A) =
    Pr[ (pk,sk) ← keygen;
        pk' ← A(sk);
        (ss, ct) ← encaps(pk');
        ct' ← A(ct)
      : ct' ≠ ct ∧ decaps(sk, ct') = ss ]
 PK_kemType u_1 SK_kemType u_2 CT_kemType u_3 SSType u_4
      kemKEM PK_kem SK_kem CT_kem SS) :
  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_5 PK_kemType u_1 SK_kemType u_2 CT_kemType u_3 SSType u_4 kemKEM PK_kem SK_kem CT_kem SS
    (Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`.(Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`.GType u_5 ×Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. GType u_5 ×Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. GType u_5 ×Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. GType u_5)Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. ×Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. SSType u_4)Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. SK_sessionType u_6 kdfKDF ((G × G × G × G) × SS) SK_session