Skip to content
PQ Stealth Addresses

MLKEM

Proved: the three DecidableEq instances VCVio's concrete encoding lacks (it sets all encoded types to ByteArray but as a plain def); that the concrete ciphertext type is INFINITE, hence SampleableType on it is provably uninhabited and the SPR simulator must be an explicit argument; the uniform-1088-byte FIPS 203 simulator and the u half of its layout against what honest K-PKE encryption emits; and the three capstones -- _le, _le_full_decomposition, _le_indCpa -- with no instance hypotheses left open.

Assumed: the v-half byte count, taken from FIPS 203 because VCVio's byteEncode_size is private; and KEM-IND-CPA → MLWE, the missing upstream lemma recorded below. See docs/spr-two-hop.md.

recorded

lemma recorded below. See `docs/spr-two-hop.md`.
-/

MLKEM.lean:20-22 ↗

instDecidableEqMlkem768EncodedTHat

Decidable equality on encoded t̂, through the ByteArray representation.

instance instDecidableEqMlkem768EncodedTHat : DecidableEq mlkem768Encoding.EncodedTHat :=
  inferInstanceAs (DecidableEq ByteArray)

MLKEM.lean:32-34 ↗

instDecidableEqMlkem768EncodedU

instance instDecidableEqMlkem768EncodedU : DecidableEq mlkem768Encoding.EncodedU :=
  inferInstanceAs (DecidableEq ByteArray)

MLKEM.lean:36-38 ↗

instDecidableEqMlkem768EncodedV

instance instDecidableEqMlkem768EncodedV : DecidableEq mlkem768Encoding.EncodedV :=
  inferInstanceAs (DecidableEq ByteArray)

MLKEM.lean:40-42 ↗

Decidable equality on the concrete encoded types

infinite_byteArray

ByteArray is infinite: the all-zero arrays have pairwise distinct lengths.

theorem infinite_byteArray : Infinite ByteArray :=
  Infinite.of_injective (fun n : ℕ => ByteArray.mk (Array.replicate n 0)) (by
    intro a b hab
    have h := congrArg ByteArray.size hab
    simp only [ByteArray.size, Array.size_replicate] at h
    exact h)

MLKEM.lean:48-54 ↗

infinite_mlkem768Ciphertext

theorem infinite_mlkem768Ciphertext :
    Infinite (Ciphertext mlkem768 mlkem768Encoding) :=
  haveI := infinite_byteArray
  Infinite.of_injective
    (fun b : ByteArray =>
      (⟨b, ByteArray.mk #[]⟩ : Ciphertext mlkem768 mlkem768Encoding))
    (by intro a b hab; exact congrArg KPKE.Ciphertext.uEncoded hab)

MLKEM.lean:57-64 ↗

isEmpty_sampleableType_mlkem768Ciphertext

axioms: propext, Classical.choice, Quot.sound · sorry-free ✓

theorem isEmpty_sampleableType_mlkem768Ciphertext :
    IsEmpty (SampleableType (Ciphertext mlkem768 mlkem768Encoding)) :=
  ⟨fun h =>
    haveI := infinite_mlkem768Ciphertext
    @not_finite _ inferInstance (@SampleableType.Finite _ h)⟩

MLKEM.lean:68-73 ↗

The concrete ciphertext type is infinite

uEncodedBytes

Bytes occupied by the u component of an encoded ciphertext: k polynomials, du bits per coefficient, 256 coefficients each.

def uEncodedBytes (params : Params) : ℕ := 32 * params.du * params.k

MLKEM.lean:78-79 ↗

vEncodedBytes

def vEncodedBytes (params : Params) : ℕ := 32 * params.dv

MLKEM.lean:82-83 ↗

uEncodedBytes_add_vEncodedBytes_eq_ciphertextBytes

theorem uEncodedBytes_add_vEncodedBytes_eq_ciphertextBytes (params : Params) :
    uEncodedBytes params + vEncodedBytes params = params.ciphertextBytes := by
proof
  simp only [uEncodedBytes, vEncodedBytes, Params.ciphertextBytes]
  ring

MLKEM.lean:86-90 ↗

uEncodedBytes_mlkem768

theorem uEncodedBytes_mlkem768 : uEncodedBytes mlkem768 = 960 := by decide

MLKEM.lean:92-93 ↗

vEncodedBytes_mlkem768

theorem vEncodedBytes_mlkem768 : vEncodedBytes mlkem768 = 128 := by decide

MLKEM.lean:95-96 ↗

size_byteEncodeDUVec_mlkem768

theorem size_byteEncodeDUVec_mlkem768 (u : RqVec mlkem768.k) :
    (mlkem768Encoding.byteEncodeDUVec u : ByteArray).size = uEncodedBytes mlkem768 := by
proof
  simp only [ByteArray.size, mlkem768Encoding, concreteEncoding, byteEncodeVec,
    Array.size_ofFn, uEncodedBytes]

MLKEM.lean:98-102 ↗

size_uEncoded_encrypt_mlkem768

theorem size_uEncoded_encrypt_mlkem768
    (ek : EncapsulationKey mlkem768 mlkem768Encoding) (msg : Message) (coins : Coins) :
    ((KPKE.encrypt concreteNTTRingOps mlkem768Encoding mlkem768Primitives ek msg
        coins).uEncoded : ByteArray).size = uEncodedBytes mlkem768 :=
  size_byteEncodeDUVec_mlkem768 _

MLKEM.lean:106-111 ↗

The FIPS 203 ciphertext byte layout

mlkem768UniformCiphertext

Uniform over the ML-KEM-768 ciphertext byte space: 960 bytes of u, 128 of v. The key-independent simulator the SPR argument compares real encapsulations against, and sharper than uniform-over-the-encoded-type would be.

def mlkem768UniformCiphertext : ProbComp (Ciphertext mlkem768 mlkem768Encoding) := do
  let u ← $ᵗ (Bytes (uEncodedBytes mlkem768))
  let v ← $ᵗ (Bytes (vEncodedBytes mlkem768))
  return ⟨ByteArray.mk u.toArray, ByteArray.mk v.toArray⟩

MLKEM.lean:117-121 ↗

The uniform-ciphertext-bytes simulator

mlkem768KEM

Our KEM, at the FIPS 203 ML-KEM-768 parameter set. Since KEM is KEMScheme over ProbComp with the type arguments reordered, this IS MLKEM.asKEMScheme, not a transport of it.

def mlkem768KEM :
    KEM (EncapsulationKey mlkem768 mlkem768Encoding)
      (DecapsulationKey mlkem768 mlkem768Encoding)
      (Ciphertext mlkem768 mlkem768Encoding) SharedSecret :=
  MLKEM.asKEMScheme concreteNTTRingOps mlkem768Encoding mlkem768Primitives

MLKEM.lean:127-132 ↗

mlkem768StealthScheme

The post-quantum stealth scheme on ML-KEM-768: discovery via real ML-KEM, announcement (ciphertext, auxGen sharedSecret encapsulationKey).

def mlkem768StealthScheme :
    StealthScheme (EncapsulationKey mlkem768 mlkem768Encoding)
      (DecapsulationKey mlkem768 mlkem768Encoding
        × EncapsulationKey mlkem768 mlkem768Encoding)
      (Ciphertext mlkem768 mlkem768Encoding × Aux) :=
  StealthScheme.ofKEMFull mlkem768KEM auxGen

MLKEM.lean:140-146 ↗

mlkem768_unlinkAdvantage_le

axioms: propext, Classical.choice, Quot.sound · sorry-free ✓

theorem mlkem768_unlinkAdvantage_le
    (adv : StealthScheme.UnlinkAdv (EncapsulationKey mlkem768 mlkem768Encoding)
      (Ciphertext mlkem768 mlkem768Encoding × Aux)) :
    (mlkem768StealthScheme auxGen).unlinkAdvantage adv ≤
      sharedSecretHiding mlkem768KEM auxGen adv true
      + auxKeyIndependence mlkem768KEM auxGen adv
      + mlkem768KEM.anonAdvantage (adv.cipherOf auxGen)
      + sharedSecretHiding mlkem768KEM auxGen adv false :=
  unlinkAdvantage_ofKEMFull_le mlkem768KEM auxGen adv

MLKEM.lean:150-159 ↗

mlkem768_unlinkAdvantage_le_full_decomposition

axioms: propext, Classical.choice, Quot.sound · sorry-free ✓

theorem mlkem768_unlinkAdvantage_le_full_decomposition
    (adv : StealthScheme.UnlinkAdv (EncapsulationKey mlkem768 mlkem768Encoding)
      (Ciphertext mlkem768 mlkem768Encoding × Aux)) :
    (mlkem768StealthScheme auxGen).unlinkAdvantage adv ≤
      sharedSecretHiding mlkem768KEM auxGen adv true
      + auxKeyIndependence mlkem768KEM auxGen adv
      + (mlkem768KEM.sprAdv mlkem768UniformCiphertext (adv.cipherOf auxGen) true
         + mlkem768KEM.sprAdv mlkem768UniformCiphertext (adv.cipherOf auxGen) false)
      + sharedSecretHiding mlkem768KEM auxGen adv false :=
  unlinkAdvantage_ofKEMFull_le_full_decomposition mlkem768KEM auxGen
    mlkem768UniformCiphertext adv

MLKEM.lean:163-174 ↗

mlkem768_unlinkAdvantage_le_indCpa

axioms: propext, Classical.choice, Quot.sound · sorry-free ✓

theorem mlkem768_unlinkAdvantage_le_indCpa
    (adv : StealthScheme.UnlinkAdv (EncapsulationKey mlkem768 mlkem768Encoding)
      (Ciphertext mlkem768 mlkem768Encoding × Aux)) :
    (mlkem768StealthScheme auxGen).unlinkAdvantage adv ≤
      KEMScheme.IND_CPA_Advantage ProbCompRuntime.probComp
        (indCpaAdv mlkem768KEM auxGen adv true)
      + auxKeyIndependence mlkem768KEM auxGen adv
      + mlkem768KEM.anonAdvantage (adv.cipherOf auxGen)
      + KEMScheme.IND_CPA_Advantage ProbCompRuntime.probComp
        (indCpaAdv mlkem768KEM auxGen adv false) :=
  unlinkAdvantage_ofKEMFull_le_indCpa mlkem768KEM auxGen adv

MLKEM.lean:178-189 ↗

The scheme at ML-KEM-768

MLKEM.kem_ind_cpa_security

theorem MLKEM.kem_ind_cpa_security {params : Params} (ring : NTTRingOps)
    (encoding : Encoding params) (prims : Primitives params encoding)
    [DecidableEq encoding.EncodedTHat] [DecidableEq encoding.EncodedU]
    [DecidableEq encoding.EncodedV] [SampleableType SharedSecret] :
    ∃ mlwe : LearningWithErrors.Problem
        (TqMatrix params.k params.k) (TqVec params.k) (TqVec params.k),
      ∀ cpaAdv : (MLKEM.asKEMScheme ring encoding prims).IND_CPA_Adversary,
        ∃ mlweAdv : LearningWithErrors.Adversary mlwe,
          KEMScheme.IND_CPA_Advantage ProbCompRuntime.probComp cpaAdv ≤
            |LearningWithErrors.advantage mlwe mlweAdv|

LatticeCrypto/MLKEM/Security.lean supplies kpke_ind_cpa_security instead: it is about K-PKE rather than the KEM, and is sorry upstream. The step between them is the T-transform half of Fujisaki-Okamoto. See docs/spr-two-hop.md. -/


[`MLKEM.lean:200-215 ↗`](https://github.com/Skanislav/pq-sap/blob/main/lean/PqStealth/MLKEM.lean#L200-L215)