PQXDH in Lean

7.3. Cryptographic assumptions🔗

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

The Gap Diffie-Hellman assumption: given a DDH oracle, the CDH problem remains hard (section 2.5, assumption 1.A).

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

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

Every proposition is propositionally equal to either `True` or `False`. 
    §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.
    complete
Definition7.7
Group: Formal security definitions and assumptions for PQXDH, following Bhargavan et al. (USENIX Security 2024). (21)
Hover another entry in this group to preview it.
Preview
Definition 7.1
Blueprint label
  • sig_keypair
Group
  • Formal security definitions and assumptions for PQXDH, following Bhargavan et al. (USENIX Security 2024).
✓L∃∀Nused by 0

KEM IND-CCA security: an attacker who sees the public key and ciphertext cannot distinguish the shared secret from random, even with a decapsulation oracle for other ciphertexts (section 2.5, assumption 1.B).

Code for Definition7.7●1 definition
  • opaque KEM_IND_CCA.{u_1, u_2, u_3, u_4} (PKType 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)`. )
  (CTType 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 SK_kem CT SS : KEMKEM.{u_1, u_2, u_3, u_4} (PK : Type u_1) (SK_kem : Type u_2) (CT : Type u_3) (SS : Type u_4) :
  Type (max (max (max u_1 u_2) u_3) u_4)KEM parameterized by public key `PK`, secret key `SK_kem`,
ciphertext `CT`, and shared secret `SS`. The `correctness` field
guarantees that honest encapsulation/decapsulation round-trips.  PKType u_1 SK_kemType u_2 CTType u_3 SSType u_4) : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    opaque KEM_IND_CCA.{u_1, u_2, u_3, u_4}
  (PKType 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)`. )
  (CTType 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 SK_kem CT SS : KEMKEM.{u_1, u_2, u_3, u_4} (PK : Type u_1) (SK_kem : Type u_2) (CT : Type u_3) (SS : Type u_4) :
  Type (max (max (max u_1 u_2) u_3) u_4)KEM parameterized by public key `PK`, secret key `SK_kem`,
ciphertext `CT`, and shared secret `SS`. The `correctness` field
guarantees that honest encapsulation/decapsulation round-trips.  PKType u_1 SK_kemType u_2 CTType u_3 SSType u_4) : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    §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.
    complete
Definition7.8
Group: Formal security definitions and assumptions for PQXDH, following Bhargavan et al. (USENIX Security 2024). (21)
Hover another entry in this group to preview it.
Preview
Definition 7.1
Blueprint label
  • sig_keypair
Group
  • Formal security definitions and assumptions for PQXDH, following Bhargavan et al. (USENIX Security 2024).
✓L∃∀Nused by 1

The KDF behaves as a random oracle: its output is indistinguishable from a uniformly random key (section 2.5, assumption 4).

Code for Definition7.8●1 definition
  • opaque KDF_RandomOracle.{u_1, u_2} (IType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) (KType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. )
  (kdfKDF I K : KDFKDF.{u_1, u_2} (I : Type u_1) (K : Type u_2) : Type (max u_1 u_2)KDF as a deterministic function, for correctness proofs.  IType u_1 KType u_2) : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    opaque KDF_RandomOracle.{u_1, u_2} (IType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. )
  (KType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) (kdfKDF I K : KDFKDF.{u_1, u_2} (I : Type u_1) (K : Type u_2) : Type (max u_1 u_2)KDF as a deterministic function, for correctness proofs.  IType u_1 KType u_2) : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    §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).
    complete
Definition7.9
Group: Formal security definitions and assumptions for PQXDH, following Bhargavan et al. (USENIX Security 2024). (21)
Hover another entry in this group to preview it.
Preview
Definition 7.1
Blueprint label
  • sig_keypair
Group
  • Formal security definitions and assumptions for PQXDH, following Bhargavan et al. (USENIX Security 2024).
✓L∃∀Nused by 0

The KDF is a pseudorandom function. Used in the post-quantum proof (Theorem 3) instead of ROM, because CryptoVerif's post-quantum soundness result does not capture the QROM (section 2.5 and section 3.5).

Code for Definition7.9●1 definition
  • opaque KDF_PRF.{u_1, u_2} (IType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) (KType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) (kdfKDF I K : KDFKDF.{u_1, u_2} (I : Type u_1) (K : Type u_2) : Type (max u_1 u_2)KDF as a deterministic function, for correctness proofs.  IType u_1 KType u_2) : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    opaque KDF_PRF.{u_1, u_2} (IType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. )
  (KType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) (kdfKDF I K : KDFKDF.{u_1, u_2} (I : Type u_1) (K : Type u_2) : Type (max u_1 u_2)KDF as a deterministic function, for correctness proofs.  IType u_1 KType u_2) : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    §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.
    complete
Definition7.10
Group: Formal security definitions and assumptions for PQXDH, following Bhargavan et al. (USENIX Security 2024). (21)
Hover another entry in this group to preview it.
Preview
Definition 7.1
Blueprint label
  • sig_keypair
Group
  • Formal security definitions and assumptions for PQXDH, following Bhargavan et al. (USENIX Security 2024).
✓L∃∀Nused by 0

AEAD satisfies both IND-CPA and INT-CTXT, which together imply IND-CCA2 (section 2.5, assumption 3).

Code for Definition7.10●1 definition
  • opaque AEAD_IND_CPA_INT_CTXT.{u_1, u_2, u_3, u_4} (KType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. )
  (PTType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) (CTType u_3 : Type u_3A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) (ADType u_4 : Type u_4A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. )
  (aeadAEAD K PT CT 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.  KType u_1 PTType u_2 CTType u_3 ADType u_4) : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    opaque AEAD_IND_CPA_INT_CTXT.{u_1, u_2, u_3, u_4}
  (KType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) (PTType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. )
  (CTType u_3 : Type u_3A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) (ADType u_4 : Type u_4A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. )
  (aeadAEAD K PT CT 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.  KType u_1 PTType u_2 CTType u_3 ADType u_4) : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    §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.
    complete
Definition7.11
Group: Formal security definitions and assumptions for PQXDH, following Bhargavan et al. (USENIX Security 2024). (21)
Hover another entry in this group to preview it.
Preview
Definition 7.1
Blueprint label
  • sig_keypair
Group
  • Formal security definitions and assumptions for PQXDH, following Bhargavan et al. (USENIX Security 2024).
✓L∃∀Nused by 0

The signature scheme is existentially unforgeable under chosen message attacks (section 2.5, assumption 2).

Code for Definition7.11●1 definition
  • opaque Sig_EUF_CMA.{u_1, u_2, u_3, u_4} (PK_sigType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) (SK_sigType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. )
  (MType u_3 : Type u_3A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) (SType u_4 : Type u_4A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) (sigSig PK_sig SK_sig M S : 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_1 SK_sigType u_2 MType u_3 SType u_4) : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    opaque Sig_EUF_CMA.{u_1, u_2, u_3, u_4}
  (PK_sigType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) (SK_sigType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. )
  (MType u_3 : Type u_3A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) (SType u_4 : Type u_4A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. )
  (sigSig PK_sig SK_sig M S : 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_1 SK_sigType u_2 MType u_3 SType u_4) : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    §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.
    complete
Definition7.12
Group: Formal security definitions and assumptions for PQXDH, following Bhargavan et al. (USENIX Security 2024). (21)
Hover another entry in this group to preview it.
Preview
Definition 7.1
Blueprint label
  • sig_keypair
Group
  • Formal security definitions and assumptions for PQXDH, following Bhargavan et al. (USENIX Security 2024).
✓L∃∀Nused by 0

Temporal 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). Used in Theorem 3, where Sig_EUF_CMA is required only at exchange time.

Code for Definition7.12●1 definition
  • opaque HeldAtExchange (assumptionProp : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. ) : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    opaque HeldAtExchange (assumptionProp : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. ) : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    Temporal 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.
    complete
Definition7.13
Group: Formal security definitions and assumptions for PQXDH, following Bhargavan et al. (USENIX Security 2024). (21)
Hover another entry in this group to preview it.
Preview
Definition 7.1
Blueprint label
  • sig_keypair
Group
  • Formal security definitions and assumptions for PQXDH, following Bhargavan et al. (USENIX Security 2024).
✓L∃∀Nused by 0

Semi-Honest Collision Resistance (Definition 1, section 4): an adversary who knows the KEM secret key cannot find a different ciphertext that decapsulates to the same shared secret. Prevents the KEM re-encapsulation attack discovered in PQXDH v1.

Code for Definition7.13●1 definition
  • opaque KEM_SH_CR.{u_1, u_2, u_3, u_4} (PKType 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)`. )
  (CTType 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 SK_kem CT SS : KEMKEM.{u_1, u_2, u_3, u_4} (PK : Type u_1) (SK_kem : Type u_2) (CT : Type u_3) (SS : Type u_4) :
  Type (max (max (max u_1 u_2) u_3) u_4)KEM parameterized by public key `PK`, secret key `SK_kem`,
ciphertext `CT`, and shared secret `SS`. The `correctness` field
guarantees that honest encapsulation/decapsulation round-trips.  PKType u_1 SK_kemType u_2 CTType u_3 SSType u_4) : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    opaque KEM_SH_CR.{u_1, u_2, u_3, u_4}
  (PKType 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)`. )
  (CTType 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 SK_kem CT SS : KEMKEM.{u_1, u_2, u_3, u_4} (PK : Type u_1) (SK_kem : Type u_2) (CT : Type u_3) (SS : Type u_4) :
  Type (max (max (max u_1 u_2) u_3) u_4)KEM parameterized by public key `PK`, secret key `SK_kem`,
ciphertext `CT`, and shared secret `SS`. The `correctness` field
guarantees that honest encapsulation/decapsulation round-trips.  PKType u_1 SK_kemType u_2 CTType u_3 SSType u_4) : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    Definition 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 ]
    complete
Definition7.14
Group: Formal security definitions and assumptions for PQXDH, following Bhargavan et al. (USENIX Security 2024). (21)
Hover another entry in this group to preview it.
Preview
Definition 7.1
Blueprint label
  • sig_keypair
Group
  • Formal security definitions and assumptions for PQXDH, following Bhargavan et al. (USENIX Security 2024).
✓L∃∀Nused by 0

The hash functions internal to Kyber (H, G, XOF) behave as Random Oracles. Distinct from Definition 7.8 — this concerns hashes inside the KEM construction, not the protocol-level KDF. The paper proves Kyber satisfies SH-CR under this assumption (Theorem 5, section 5.3.2).

Code for Definition7.14●1 definition
  • opaque KEM_InternalHash_ROM.{u_1, u_2, u_3, u_4} (PKType 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)`. ) (CTType 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 SK_kem CT SS : KEMKEM.{u_1, u_2, u_3, u_4} (PK : Type u_1) (SK_kem : Type u_2) (CT : Type u_3) (SS : Type u_4) :
  Type (max (max (max u_1 u_2) u_3) u_4)KEM parameterized by public key `PK`, secret key `SK_kem`,
ciphertext `CT`, and shared secret `SS`. The `correctness` field
guarantees that honest encapsulation/decapsulation round-trips.  PKType u_1 SK_kemType u_2 CTType u_3 SSType u_4) : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    opaque KEM_InternalHash_ROM.{u_1, u_2, u_3, u_4}
  (PKType 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)`. )
  (CTType 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 SK_kem CT SS : KEMKEM.{u_1, u_2, u_3, u_4} (PK : Type u_1) (SK_kem : Type u_2) (CT : Type u_3) (SS : Type u_4) :
  Type (max (max (max u_1 u_2) u_3) u_4)KEM parameterized by public key `PK`, secret key `SK_kem`,
ciphertext `CT`, and shared secret `SS`. The `correctness` field
guarantees that honest encapsulation/decapsulation round-trips.  PKType u_1 SK_kemType u_2 CTType u_3 SSType u_4) : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    §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.
    complete