6.1. ML-KEM🔗

Definition6.1.1

Group: Module-Lattice Key Encapsulation Mechanism (ML-KEM, FIPS 203). (4)

Group member previews

Preview

Definition 6.1.2

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 1

Used by 5

Reverse dependency previews

Preview

Definition 6.1.2

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

\todo

def mlkemScheme (p : ParameterSet) (ring : NTTRingOps)
    (prims : Primitives (ParameterSet.params p)
      (Concrete.concreteEncoding (ParameterSet.params p))) :
    KEMScheme ProbComp SharedSecret
      (EncapsulationKey (ParameterSet.params p)
        (Concrete.concreteEncoding (ParameterSet.params p)))
      (DecapsulationKey (ParameterSet.params p)
        (Concrete.concreteEncoding (ParameterSet.params p)))
      (Ciphertext (ParameterSet.params p)
        (Concrete.concreteEncoding (ParameterSet.params p))) :=
  asKEMScheme ring (Concrete.concreteEncoding (ParameterSet.params p)) prims

uses Definition 6.3.2 · github #215

Lean code for Definition6.1.1●1 definition

defdefined in SecureMessaging/KEM/MLKEM/Construction.lean

complete

def MLKEM.mlkemScheme (p : MLKEM.ParameterSet) (ring : MLKEM.NTTRingOps)
  (prims :
    MLKEM.Primitives p.params
      (MLKEM.Concrete.concreteEncoding p.params)) :
  KEMScheme ProbComp MLKEM.SharedSecret
    (MLKEM.EncapsulationKey p.params
      (MLKEM.Concrete.concreteEncoding p.params))
    (MLKEM.DecapsulationKey p.params
      (MLKEM.Concrete.concreteEncoding p.params))
    (MLKEM.Ciphertext p.params
      (MLKEM.Concrete.concreteEncoding p.params))

def MLKEM.mlkemScheme (p : MLKEM.ParameterSet)
  (ring : MLKEM.NTTRingOps)
  (prims :
    MLKEM.Primitives p.params
      (MLKEM.Concrete.concreteEncoding
        p.params)) :
  KEMScheme ProbComp MLKEM.SharedSecret
    (MLKEM.EncapsulationKey p.params
      (MLKEM.Concrete.concreteEncoding
        p.params))
    (MLKEM.DecapsulationKey p.params
      (MLKEM.Concrete.concreteEncoding
        p.params))
    (MLKEM.Ciphertext p.params
      (MLKEM.Concrete.concreteEncoding
        p.params))

The ML-KEM key-encapsulation mechanism at the approved parameter set `p`
(FIPS 203 Section 7). Key generation samples K-PKE key-generation randomness
`d` and an independent implicit-rejection seed `z`, then runs
`ML-KEM.KeyGen_internal` (Algorithm 19); encapsulation samples the message `m`
and runs `ML-KEM.Encaps_internal` (Algorithm 20); decapsulation runs
`ML-KEM.Decaps_internal` with implicit rejection (Algorithm 21). Byte encoding
and compression are the executable FIPS 203 codec; the NTT `ring` and the
SHA-3 family `prims` are the supplied slots. Input validation lives in the
checked interface `MLKEM.encaps` / `MLKEM.decaps`.

Definition6.1.2

Group: Module-Lattice Key Encapsulation Mechanism (ML-KEM, FIPS 203). (4)

Group member previews

Preview

Definition 6.1.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 1used by 0✓L∃∀N

ML-KEM randomness leakage

def mlkemRandLeak (p : ParameterSet) (ring : NTTRingOps)
    (prims : Primitives (ParameterSet.params p)
      (Concrete.concreteEncoding (ParameterSet.params p))) :
    (mlkemScheme p ring prims).RandLeak where
  KeygenRand := Seed32 × Seed32
  EncapsRand := Message
  keygenRleak := do
    let d ← $ᵗ Seed32
    let z ← $ᵗ Seed32
    return (keygenInternal ring (Concrete.concreteEncoding (ParameterSet.params p)) prims d z,
      (d, z))
  encapsRleak := fun ek => do
    let m ← $ᵗ Message
    let (k, c) := encapsInternal ring (Concrete.concreteEncoding (ParameterSet.params p))
      prims ek m
    return ((c, k), m)
  keygen_fst := byp:ParameterSetring:NTTRingOpsprims:Primitives p.params (Concrete.concreteEncoding p.params)⊢ (do
    let out ←
      do
        let d ← $ᵗ Seed32
        let z ← $ᵗ Seed32
        pure (keygenInternal ring (Concrete.concreteEncoding p.params) prims d z, d, z)
    pure out.1) =
  (mlkemScheme p ring prims).keygen
    simp only [mlkemScheme, asKEMScheme, keygen, bind_assoc, pure_bind]All goals completed! 🐙
  encaps_fst := fun _ek => byp:ParameterSetring:NTTRingOpsprims:Primitives p.params (Concrete.concreteEncoding p.params)_ek:EncapsulationKey p.params (Concrete.concreteEncoding p.params)⊢ (do
    let out ←
      do
        let m ← $ᵗ Message
        match encapsInternal ring (Concrete.concreteEncoding p.params) prims _ek m with
          | (k, c) => pure ((c, k), m)
    pure out.1) =
  (mlkemScheme p ring prims).encaps _ek
    simp only [mlkemScheme, asKEMScheme, bind_assoc, pure_bind]All goals completed! 🐙

uses Definition 6.1.1

Lean code for Definition6.1.2●1 definition

defdefined in SecureMessaging/KEM/MLKEM/Construction.lean

complete

def MLKEM.mlkemRandLeak (p : MLKEM.ParameterSet) (ring : MLKEM.NTTRingOps)
  (prims :
    MLKEM.Primitives p.params
      (MLKEM.Concrete.concreteEncoding p.params)) :
  (MLKEM.mlkemScheme p ring prims).RandLeak

def MLKEM.mlkemRandLeak
  (p : MLKEM.ParameterSet)
  (ring : MLKEM.NTTRingOps)
  (prims :
    MLKEM.Primitives p.params
      (MLKEM.Concrete.concreteEncoding
        p.params)) :
  (MLKEM.mlkemScheme p ring
      prims).RandLeak

Randomness-leakage package for `mlkemScheme`. Key generation leaks the
FIPS 203 seeds `(d, z)`; encapsulation leaks the sampled message `m`.

Theorem6.1.3

Group: Module-Lattice Key Encapsulation Mechanism (ML-KEM, FIPS 203). (4)

Group member previews

Preview

Definition 6.1.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 1used by 0✓L∃∀N

\todo

theorem deltaCorrect_fips203 (p : ParameterSet) (ring : NTTRingOps)
    (prims : Primitives (ParameterSet.params p)
      (Concrete.concreteEncoding (ParameterSet.params p)))
    (hRing : NTTRingLaws ring) (hModel : CoefficientFailureBound p ring prims) :
    (mlkemScheme p ring prims).deltaCorrect ProbCompRuntime.probComp
      (fips203DecapsulationFailureBound p)

`δ`-correctness predicate

def deltaCorrect (kem : KEMScheme m K PK SK C)
    (runtime : ProbCompRuntime m) (delta : ℝ≥0∞) : Prop :=
  kem.correctnessError runtime ≤ delta

FIPS 203 Table 1 exponents

def decapsulationFailureExponent : ParameterSet → ℚ
  | .MLKEM512 => 138.8
  | .MLKEM768 => 164.8
  | .MLKEM1024 => 174.8

failure bound δ_p = 2^{-e_p}

noncomputable def fips203DecapsulationFailureBound (p : ParameterSet) : ℝ≥0∞ :=
  2 ^ (-(decapsulationFailureExponent p : ℝ))

uses Definition 6.1.1 · github #219

Lean code for Theorem6.1.3●1 theorem

theoremdefined in SecureMessaging/KEM/MLKEM/Correctness.lean

complete

theorem MLKEM.deltaCorrect_fips203 (p : MLKEM.ParameterSet)
  (ring : MLKEM.NTTRingOps)
  (prims :
    MLKEM.Primitives p.params
      (MLKEM.Concrete.concreteEncoding p.params))
  (hRing : MLKEM.NTTRingLaws ring)
  (hModel : MLKEM.CoefficientFailureBound p ring prims) :
  (MLKEM.mlkemScheme p ring prims).deltaCorrect ProbCompRuntime.probComp
    (MLKEM.fips203DecapsulationFailureBound p)

theorem MLKEM.deltaCorrect_fips203
  (p : MLKEM.ParameterSet)
  (ring : MLKEM.NTTRingOps)
  (prims :
    MLKEM.Primitives p.params
      (MLKEM.Concrete.concreteEncoding
        p.params))
  (hRing : MLKEM.NTTRingLaws ring)
  (hModel :
    MLKEM.CoefficientFailureBound p ring
      prims) :
  (MLKEM.mlkemScheme p ring
        prims).deltaCorrect
    ProbCompRuntime.probComp
    (MLKEM.fips203DecapsulationFailureBound
      p)

Under the coefficient-distribution comparison
`CoefficientFailureBound`, ML-KEM at parameter set `p` is `δ`-correct for
`δ=2^(-e_p)`.

Theorem6.1.4

Group: Module-Lattice Key Encapsulation Mechanism (ML-KEM, FIPS 203). (4)

Group member previews

Preview

Definition 6.1.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 1used by 1✓L∃∀N

\todo

δ-correctness from EasyCrypt bounds

theorem deltaCorrect_mlkem768_easycrypt_of_le {failprob hsadv prfadv : ℝ≥0∞}
    (hcb : EasyCryptMLKEM768.correctnessBoundError ≤ failprob)
    (hhs : EasyCryptMLKEM768.smoothingAdvantage ≤ hsadv)
    (hkg : EasyCryptMLKEM768.keygenPRFAdvantage ≤ prfadv)
    (henc : EasyCryptMLKEM768.encapsPRFAdvantage ≤ prfadv) :
    mlkem768Scheme.deltaCorrect ProbCompRuntime.probComp (failprob + hsadv + 2 * prfadv)

uses Definition 6.1.1 · github #226

Lean code for Theorem6.1.4●1 theorem

theoremdefined in SecureMessaging/KEM/MLKEM/Correctness/EasyCryptBoundary.lean

complete

theorem MLKEM.deltaCorrect_mlkem768_easycrypt_of_le
  {failprob hsadv prfadv : ENNReal}
  (hcb : MLKEM.EasyCryptMLKEM768.correctnessBoundError ≤ failprob)
  (hhs : MLKEM.EasyCryptMLKEM768.smoothingAdvantage ≤ hsadv)
  (hkg : MLKEM.EasyCryptMLKEM768.keygenPRFAdvantage ≤ prfadv)
  (henc : MLKEM.EasyCryptMLKEM768.encapsPRFAdvantage ≤ prfadv) :
  MLKEM.mlkem768Scheme.deltaCorrect ProbCompRuntime.probComp
    (failprob + hsadv + 2 * prfadv)

theorem MLKEM.deltaCorrect_mlkem768_easycrypt_of_le
  {failprob hsadv prfadv : ENNReal}
  (hcb :
    MLKEM.EasyCryptMLKEM768.correctnessBoundError ≤
      failprob)
  (hhs :
    MLKEM.EasyCryptMLKEM768.smoothingAdvantage ≤
      hsadv)
  (hkg :
    MLKEM.EasyCryptMLKEM768.keygenPRFAdvantage ≤
      prfadv)
  (henc :
    MLKEM.EasyCryptMLKEM768.encapsPRFAdvantage ≤
      prfadv) :
  MLKEM.mlkem768Scheme.deltaCorrect
    ProbCompRuntime.probComp
    (failprob + hsadv + 2 * prfadv)

Under the upper-bound hypotheses of `mlkem_spec_correctness`, the local ML-KEM-768
scheme is `(failprob + hsadv + 2 * prfadv)`-correct.

Theorem6.1.5

Group: Module-Lattice Key Encapsulation Mechanism (ML-KEM, FIPS 203). (4)

Group member previews

Preview

Definition 6.1.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 1used by 0XL∃∀N

\todo

LeanLean anchor pending

uses Definition 6.1.1 · github #216