Secure Messaging

6.4.ย Incremental KEM๐Ÿ”—

Definition6.4.1
groupuses 0
Used by 7
Reverse dependency previews
Preview
Definition 6.4.2
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
โœ“Lโˆƒโˆ€N

\todo

incremental KEM interface

structure IncrementalStructure (kem : KEMScheme m K PK SK C) where /-- Public-key header type. -/ PKheader : Type /-- Public-key vector type. -/ PKvector : Type /-- First ciphertext component. -/ Cโ‚ : Type /-- Second ciphertext component. -/ Cโ‚‚ : Type /-- Encapsulation state carried from the first stage to the second. -/ St : Type /-- Consistency check of a vector part against a header. -/ validPK : PKheader โ†’ PKvector โ†’ Bool /-- There is a bijection between public keys and header/vector pairs that pass `validPK`. -/ splitPK : PK โ‰ƒ { parts : PKheader ร— PKvector // validPK parts.1 parts.2 = true } /-- The ciphertext splits as `ct = (ct1, ct2)`. -/ splitC : C โ‰ƒ Cโ‚ ร— Cโ‚‚ /-- First stage of encaps: from the header alone, returns the state, `ct1`, and the shared key. -/ encaps1 : PKheader โ†’ m (St ร— Cโ‚ ร— K) /-- Second stage of encaps: returns the second ciphertext component `ct2`. -/ encaps2 : St โ†’ PKheader โ†’ PKvector โ†’ m Cโ‚‚ /-- For every public key, `kem.encaps` is equal to first running `encaps1` on the derived header, then running `encaps2` on the resulting state. -/ factor : โˆ€ pk, kem.encaps pk = (do let (hdr, vec) := (splitPK pk).1 let (st, c1, k) โ† encaps1 hdr let c2 โ† encaps2 st hdr vec pure (splitC.symm (c1, c2), k))

github #224

Lean code for Definition6.4.1โ—1 definition
  • structure(11 fields)defined in SecureMessaging/KEM/IncrementalKEM/Defs.lean
    complete
    structure KEMScheme.IncrementalStructure.{u} {m : Type โ†’ Type u} [Monad m]
  {K PK SK C : Type} (kem : KEMScheme m K PK SK C) : Type (max 1 u)
    structure KEMScheme.IncrementalStructure.{u}
  {m : Type โ†’ Type u} [Monad m]
  {K PK SK C : Type}
  (kem : KEMScheme m K PK SK C) :
  Type (max 1 u)
    An incremental KEM witness for a KEM `kem`, decomposing `kem.encaps`
into two stages using the two parts of the public encapsulation key.

- `PKheader`: the encapsulation key header;
- `PKvector`: the encapsulation key vector;
- `Cโ‚`, `Cโ‚‚`: the first and second ciphertext spaces;
- `St`: the encapsulation secret state carried between the two stages;
- `validPK hdr vec`: consistency check of a pair `(hdr,vec)`;
- `splitPK`: identifies public keys with valid header/vector pairs;
- `splitC`: identifies the ciphertext space `C` with `Cโ‚ ร— Cโ‚‚`;
- `encaps1 hdr`: the first stage, producing the state, `ct1`, and the shared key;
- `encaps2 st hdr vec`: the second stage, producing `ct2`;
- `factor`: `kem.encaps` agrees with `encaps1` then `encaps2` on `splitPK`.

    Fields

    PKheader : Type
    Public-key header type. 
    PKvector : Type
    Public-key vector type. 
    Cโ‚ : Type
    First ciphertext component. 
    Cโ‚‚ : Type
    Second ciphertext component. 
    St : Type
    Encapsulation state carried from the first stage to the second. 
    validPK : self.PKheader โ†’ self.PKvector โ†’ Bool
    Consistency check of a vector part against a header. 
    splitPK : PK โ‰ƒ { parts // self.validPK parts.1 parts.2 = true }
    There is a bijection between public keys and header/vector pairs that pass `validPK`. 
    splitC : C โ‰ƒ self.Cโ‚ ร— self.Cโ‚‚
    The ciphertext splits as `ct = (ct1, ct2)`. 
    encaps1 : self.PKheader โ†’ m (self.St ร— self.Cโ‚ ร— K)
    First stage of encaps: from the header alone, returns the state, `ct1`, and the shared key. 
    encaps2 : self.St โ†’ self.PKheader โ†’ self.PKvector โ†’ m self.Cโ‚‚
    Second stage of encaps: returns the second ciphertext component `ct2`. 
    factor : โˆ€ (pk : PK),
  kem.encaps pk =
    match โ†‘(self.splitPK pk) with
    | (hdr, vec) => do
      let __discr โ† self.encaps1 hdr
      match __discr with
        | (st, c1, k) => do
          let c2 โ† self.encaps2 st hdr vec
          pure (self.splitC.symm (c1, c2), k)
    For every public key, `kem.encaps` is equal to first running `encaps1`
on the derived header, then running `encaps2` on the resulting state.
Definition6.4.2
group
Statement uses 2
Statement dependency previews
Preview
Definition 6.1.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 2
Reverse dependency previews
Preview
Theorem 6.4.3
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
โœ“Lโˆƒโˆ€N

\todo

public-key header (ฯ, H(ek))

def incrementalHeader {params : Params} {encoding : Encoding params} (prims : Primitives params encoding) (ek : EncapsulationKey params encoding) : Seed32 ร— PublicKeyHash := (ek.rho, encapsulationKeyHash encoding prims ek)

state carried between encapsulation stages

structure EncapsulationState (params : Params) where /-- NTT-domain form of the ephemeral vector `y`, used to compute the second ciphertext component. -/ yHat : TqVec params.k /-- Second encapsulation-noise polynomial, added to the second ciphertext component. -/ e2 : Rq /-- Sampled 32-byte ML-KEM message embedded in the second ciphertext component. -/ message : Message

first stage: derive state, u, and the shared secret

def incrementalEncaps1 {params : Params} {encoding : Encoding params} (ring : NTTRingOps) (prims : Primitives params encoding) (hdr : Seed32 ร— PublicKeyHash) (m : Message) : EncapsulationState params ร— encoding.EncodedU ร— SharedSecret := let (k, r) := prims.gEncaps m hdr.2 let aHat := prims.publicMatrix hdr.1 let y := prims.sampleVecEta1 r 0 let e1 := prims.sampleVecEta2 r params.k let e2 := prims.prfEta2 r (2 * params.k) let yHat := ring.nttVec y let u := ring.invNTTVec (ring.matTransposeVecMul aHat yHat) + e1 ({ yHat, e2, message := m }, encoding.byteEncodeDUVec (encoding.compressDU u), k)

second stage: derive v from the public-key vector

def incrementalEncaps2 {params : Params} {encoding : Encoding params} (ring : NTTRingOps) (st : EncapsulationState params) (vec : encoding.EncodedTHat) : encoding.EncodedV := let tHat := encoding.byteDecode12Vec vec let mu := encoding.decompress1 (encoding.byteDecode1 st.message) let v := ring.invNTT (ring.dot tHat st.yHat) + st.e2 + mu encoding.byteEncodeDV (encoding.compressDV v)

complete incremental ML-KEM construction

def mlkemIncremental (p : ParameterSet) (ring : NTTRingOps) (prims : Primitives (ParameterSet.params p) (Concrete.concreteEncoding (ParameterSet.params p))) : (mlkemScheme p ring prims).IncrementalStructure where PKheader := Seed32 ร— PublicKeyHash PKvector := (Concrete.concreteEncoding (ParameterSet.params p)).EncodedTHat Cโ‚ := (Concrete.concreteEncoding (ParameterSet.params p)).EncodedU Cโ‚‚ := (Concrete.concreteEncoding (ParameterSet.params p)).EncodedV St := EncapsulationState (ParameterSet.params p) validPK hdr vec := decide (encapsulationKeyHash (Concrete.concreteEncoding (ParameterSet.params p)) prims { tHatEncoded := vec, rho := hdr.1 } = hdr.2) splitPK := { toFun := fun ek => โŸจ(incrementalHeader prims ek, ek.tHatEncoded), p:ParameterSetring:NTTRingOpsprims:Primitives p.params (Concrete.concreteEncoding p.params)ek:EncapsulationKey p.params (Concrete.concreteEncoding p.params)โŠข decide (encapsulationKeyHash (Concrete.concreteEncoding p.params) prims { tHatEncoded := (incrementalHeader prims ek, ek.tHatEncoded).2, rho := (incrementalHeader prims ek, ek.tHatEncoded).1.1 } = (incrementalHeader prims ek, ek.tHatEncoded).1.2) = true All goals completed! ๐Ÿ™โŸฉ invFun := fun parts => { tHatEncoded := parts.1.2, rho := parts.1.1.1 } left_inv := fun _ => rfl right_inv := p:ParameterSetring:NTTRingOpsprims:Primitives p.params (Concrete.concreteEncoding p.params)โŠข Function.RightInverse (fun parts => { tHatEncoded := (โ†‘parts).2, rho := (โ†‘parts).1.1 }) fun ek => โŸจ(incrementalHeader prims ek, ek.tHatEncoded), โ‹ฏโŸฉ p:ParameterSetring:NTTRingOpsprims:Primitives p.params (Concrete.concreteEncoding p.params)vec:(Concrete.concreteEncoding p.params).EncodedTHatrho:Seed32h:PublicKeyHashhvalid:decide (encapsulationKeyHash (Concrete.concreteEncoding p.params) prims { tHatEncoded := ((rho, h), vec).2, rho := ((rho, h), vec).1.1 } = ((rho, h), vec).1.2) = trueโŠข (fun ek => โŸจ(incrementalHeader prims ek, ek.tHatEncoded), โ‹ฏโŸฉ) ((fun parts => { tHatEncoded := (โ†‘parts).2, rho := (โ†‘parts).1.1 }) โŸจ((rho, h), vec), hvalidโŸฉ) = โŸจ((rho, h), vec), hvalidโŸฉ p:ParameterSetring:NTTRingOpsprims:Primitives p.params (Concrete.concreteEncoding p.params)vec:(Concrete.concreteEncoding p.params).EncodedTHatrho:Seed32h:PublicKeyHashhvalid:decide (encapsulationKeyHash (Concrete.concreteEncoding p.params) prims { tHatEncoded := ((rho, h), vec).2, rho := ((rho, h), vec).1.1 } = ((rho, h), vec).1.2) = truehh:encapsulationKeyHash (Concrete.concreteEncoding p.params) prims { tHatEncoded := ((rho, h), vec).2, rho := ((rho, h), vec).1.1 } = ((rho, h), vec).1.2โŠข (fun ek => โŸจ(incrementalHeader prims ek, ek.tHatEncoded), โ‹ฏโŸฉ) ((fun parts => { tHatEncoded := (โ†‘parts).2, rho := (โ†‘parts).1.1 }) โŸจ((rho, h), vec), hvalidโŸฉ) = โŸจ((rho, h), vec), hvalidโŸฉ p:ParameterSetring:NTTRingOpsprims:Primitives p.params (Concrete.concreteEncoding p.params)vec:(Concrete.concreteEncoding p.params).EncodedTHatrho:Seed32h:PublicKeyHashhvalid:decide (encapsulationKeyHash (Concrete.concreteEncoding p.params) prims { tHatEncoded := ((rho, h), vec).2, rho := ((rho, h), vec).1.1 } = ((rho, h), vec).1.2) = truehh:encapsulationKeyHash (Concrete.concreteEncoding p.params) prims { tHatEncoded := ((rho, h), vec).2, rho := ((rho, h), vec).1.1 } = ((rho, h), vec).1.2โŠข โ†‘((fun ek => โŸจ(incrementalHeader prims ek, ek.tHatEncoded), โ‹ฏโŸฉ) ((fun parts => { tHatEncoded := (โ†‘parts).2, rho := (โ†‘parts).1.1 }) โŸจ((rho, h), vec), hvalidโŸฉ)) = โ†‘โŸจ((rho, h), vec), hvalidโŸฉ All goals completed! ๐Ÿ™ } splitC := { toFun := fun c => (c.uEncoded, c.vEncoded) invFun := fun uv => { uEncoded := uv.1, vEncoded := uv.2 } left_inv := fun _ => rfl right_inv := fun _ => rfl } encaps1 := fun hdr => do let m โ†$แต— Message return incrementalEncaps1 ring prims hdr m encaps2 := fun st _hdr vec => return (incrementalEncaps2 ring st vec) factor := p:ParameterSetring:NTTRingOpsprims:Primitives p.params (Concrete.concreteEncoding p.params)โŠข โˆ€ (pk : EncapsulationKey p.params (Concrete.concreteEncoding p.params)), (mlkemScheme p ring prims).encaps pk = match โ†‘({ toFun := fun ek => โŸจ(incrementalHeader prims ek, ek.tHatEncoded), โ‹ฏโŸฉ, invFun := fun parts => { tHatEncoded := (โ†‘parts).2, rho := (โ†‘parts).1.1 }, left_inv := โ‹ฏ, right_inv := โ‹ฏ } pk) with | (hdr, vec) => do let __discr โ† do let m โ† $แต— Message pure (incrementalEncaps1 ring prims hdr m) match __discr with | (st, c1, k) => do let c2 โ† pure (incrementalEncaps2 ring st vec) pure ({ toFun := fun c => (c.uEncoded, c.vEncoded), invFun := fun uv => { uEncoded := uv.1, vEncoded := uv.2 }, left_inv := โ‹ฏ, right_inv := โ‹ฏ }.symm (c1, c2), k) p:ParameterSetring:NTTRingOpsprims:Primitives p.params (Concrete.concreteEncoding p.params)ek:EncapsulationKey p.params (Concrete.concreteEncoding p.params)โŠข (mlkemScheme p ring prims).encaps ek = match โ†‘({ toFun := fun ek => โŸจ(incrementalHeader prims ek, ek.tHatEncoded), โ‹ฏโŸฉ, invFun := fun parts => { tHatEncoded := (โ†‘parts).2, rho := (โ†‘parts).1.1 }, left_inv := โ‹ฏ, right_inv := โ‹ฏ } ek) with | (hdr, vec) => do let __discr โ† do let m โ† $แต— Message pure (incrementalEncaps1 ring prims hdr m) match __discr with | (st, c1, k) => do let c2 โ† pure (incrementalEncaps2 ring st vec) pure ({ toFun := fun c => (c.uEncoded, c.vEncoded), invFun := fun uv => { uEncoded := uv.1, vEncoded := uv.2 }, left_inv := โ‹ฏ, right_inv := โ‹ฏ }.symm (c1, c2), k) p:ParameterSetring:NTTRingOpsprims:Primitives p.params (Concrete.concreteEncoding p.params)ek:EncapsulationKey p.params (Concrete.concreteEncoding p.params)โŠข (do let m โ† $แต— Message pure ((encapsInternal ring (Concrete.concreteEncoding p.params) prims ek m).2, (encapsInternal ring (Concrete.concreteEncoding p.params) prims ek m).1)) = do let x โ† $แต— Message pure ({ uEncoded := (incrementalEncaps1 ring prims (incrementalHeader prims ek) x).2.1, vEncoded := incrementalEncaps2 ring (incrementalEncaps1 ring prims (incrementalHeader prims ek) x).1 ek.tHatEncoded }, (incrementalEncaps1 ring prims (incrementalHeader prims ek) x).2.2) All goals completed! ๐Ÿ™

uses Definition 6.4.1 ยท Definition 6.1.1 ยท github #226

Lean code for Definition6.4.2โ—5 definitions
  • defdefined in SecureMessaging/KEM/IncrementalKEM/FromMLKEM.lean
    complete
    def MLKEM.incrementalHeader {params : MLKEM.Params}
  {encoding : MLKEM.Encoding params}
  (prims : MLKEM.Primitives params encoding)
  (ek : MLKEM.EncapsulationKey params encoding) :
  MLKEM.Seed32 ร— MLKEM.PublicKeyHash
    def MLKEM.incrementalHeader
  {params : MLKEM.Params}
  {encoding : MLKEM.Encoding params}
  (prims :
    MLKEM.Primitives params encoding)
  (ek :
    MLKEM.EncapsulationKey params
      encoding) :
  MLKEM.Seed32 ร— MLKEM.PublicKeyHash
    The incremental public-key header `(ฯ, H(ek))`. The first stage uses both values in
`G(m โ€– H(ek))` and matrix expansion.
  • structure(3 fields)defined in SecureMessaging/KEM/IncrementalKEM/FromMLKEM.lean
    complete
    structure MLKEM.EncapsulationState (params : MLKEM.Params) : Type
    structure MLKEM.EncapsulationState
  (params : MLKEM.Params) : Type
    Values computed during the first incremental encapsulation stage and needed by the
second: the NTT-domain ephemeral vector `yHat`, second noise polynomial `e2`, and ML-KEM
`message`. This semantic state retains derived values rather than the raw coins.

    Fields

    yHat : MLKEM.TqVec params.k
    NTT-domain form of the ephemeral vector `y`, used to compute the second ciphertext
component. 
    e2 : MLKEM.Rq
    Second encapsulation-noise polynomial, added to the second ciphertext component. 
    message : MLKEM.Message
    Sampled 32-byte ML-KEM message embedded in the second ciphertext component.
  • defdefined in SecureMessaging/KEM/IncrementalKEM/FromMLKEM.lean
    complete
    def MLKEM.incrementalEncaps1 {params : MLKEM.Params}
  {encoding : MLKEM.Encoding params} (ring : MLKEM.NTTRingOps)
  (prims : MLKEM.Primitives params encoding)
  (hdr : MLKEM.Seed32 ร— MLKEM.PublicKeyHash) (m : MLKEM.Message) :
  MLKEM.EncapsulationState params ร—
    encoding.EncodedU ร— MLKEM.SharedSecret
    def MLKEM.incrementalEncaps1
  {params : MLKEM.Params}
  {encoding : MLKEM.Encoding params}
  (ring : MLKEM.NTTRingOps)
  (prims :
    MLKEM.Primitives params encoding)
  (hdr :
    MLKEM.Seed32 ร— MLKEM.PublicKeyHash)
  (m : MLKEM.Message) :
  MLKEM.EncapsulationState params ร—
    encoding.EncodedU ร— MLKEM.SharedSecret
    Given `(ฯ, h)` and `m`, derives `(k, r) = G(m โ€– h)`, computes `yHat`, `e2`, and the
encoded `u` component, and returns them as the stage-2 state, first ciphertext component,
and shared secret.
  • defdefined in SecureMessaging/KEM/IncrementalKEM/FromMLKEM.lean
    complete
    def MLKEM.incrementalEncaps2 {params : MLKEM.Params}
  {encoding : MLKEM.Encoding params} (ring : MLKEM.NTTRingOps)
  (st : MLKEM.EncapsulationState params) (vec : encoding.EncodedTHat) :
  encoding.EncodedV
    def MLKEM.incrementalEncaps2
  {params : MLKEM.Params}
  {encoding : MLKEM.Encoding params}
  (ring : MLKEM.NTTRingOps)
  (st : MLKEM.EncapsulationState params)
  (vec : encoding.EncodedTHat) :
  encoding.EncodedV
    Given the derived stage-2 state and encoded `tฬ‚`, decodes `tHat`, combines it with the
retained `yHat`, `e2`, and `message`, and returns the encoded `v` component without
re-sampling or recomputing an NTT.
  • defdefined in SecureMessaging/KEM/IncrementalKEM/FromMLKEM.lean
    complete
    def MLKEM.mlkemIncremental (p : MLKEM.ParameterSet)
  (ring : MLKEM.NTTRingOps)
  (prims :
    MLKEM.Primitives p.params
      (MLKEM.Concrete.concreteEncoding p.params)) :
  (MLKEM.mlkemScheme p ring prims).IncrementalStructure
    def MLKEM.mlkemIncremental
  (p : MLKEM.ParameterSet)
  (ring : MLKEM.NTTRingOps)
  (prims :
    MLKEM.Primitives p.params
      (MLKEM.Concrete.concreteEncoding
        p.params)) :
  (MLKEM.mlkemScheme p ring
      prims).IncrementalStructure
    The incremental ML-KEM structure of ML-KEM Braid, Section 1.2.1. Stage 1 produces an
`EncapsulationState` containing `yHat`, `e2`, and `message`; stage 2 consumes that state
without retaining raw coins. `validPK` checks the header hash against the reconstructed
public key.
Theorem6.4.3
group
Statement uses 2
Statement dependency previews
Preview
Theorem 6.1.4
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0โœ“Lโˆƒโˆ€N

\todo

staged ML-KEM-768 correctness bound

theorem incrementalCorrectExp_failure_le_mlkem768_easycrypt {failprob hsadv prfadv : โ„โ‰ฅ0โˆž} (hcb : EasyCryptMLKEM768.correctnessBoundError โ‰ค failprob) (hhs : EasyCryptMLKEM768.smoothingAdvantage โ‰ค hsadv) (hkg : EasyCryptMLKEM768.keygenPRFAdvantage โ‰ค prfadv) (henc : EasyCryptMLKEM768.encapsPRFAdvantage โ‰ค prfadv) : Pr[= false | ProbCompRuntime.probComp.evalDist (mlkemIncremental .MLKEM768 Concrete.concreteNTTRingOps Concrete.mlkem768Primitives).CorrectExp] โ‰ค failprob + hsadv + 2 * prfadv

uses Definition 6.4.2 ยท Theorem 6.1.4 ยท github #226

Lean code for Theorem6.4.3โ—1 theorem
  • theoremdefined in SecureMessaging/KEM/MLKEM/Correctness/EasyCryptBoundary.lean
    complete
    theorem MLKEM.incrementalCorrectExp_failure_le_mlkem768_easycrypt
  {failprob hsadv prfadv : ENNReal}
  (hcb : MLKEM.EasyCryptMLKEM768.correctnessBoundError โ‰ค failprob)
  (hhs : MLKEM.EasyCryptMLKEM768.smoothingAdvantage โ‰ค hsadv)
  (hkg : MLKEM.EasyCryptMLKEM768.keygenPRFAdvantage โ‰ค prfadv)
  (henc : MLKEM.EasyCryptMLKEM768.encapsPRFAdvantage โ‰ค prfadv) :
  Pr[= false |
      ProbCompRuntime.probComp.evalDist
        (MLKEM.mlkemIncremental MLKEM.ParameterSet.MLKEM768
            MLKEM.Concrete.concreteNTTRingOps
            MLKEM.Concrete.mlkem768Primitives).CorrectExp] โ‰ค
    failprob + hsadv + 2 * prfadv
    theorem MLKEM.incrementalCorrectExp_failure_le_mlkem768_easycrypt
  {failprob hsadv prfadv : ENNReal}
  (hcb :
    MLKEM.EasyCryptMLKEM768.correctnessBoundError โ‰ค
      failprob)
  (hhs :
    MLKEM.EasyCryptMLKEM768.smoothingAdvantage โ‰ค
      hsadv)
  (hkg :
    MLKEM.EasyCryptMLKEM768.keygenPRFAdvantage โ‰ค
      prfadv)
  (henc :
    MLKEM.EasyCryptMLKEM768.encapsPRFAdvantage โ‰ค
      prfadv) :
  Pr[= false |
      ProbCompRuntime.probComp.evalDist
        (MLKEM.mlkemIncremental
            MLKEM.ParameterSet.MLKEM768
            MLKEM.Concrete.concreteNTTRingOps
            MLKEM.Concrete.mlkem768Primitives).CorrectExp] โ‰ค
    failprob + hsadv + 2 * prfadv
    The staged ML-KEM-768 correctness experiment returns `false` with probability at most
`failprob + hsadv + 2 * prfadv`.
Definition6.4.4
group
Statement uses 2
Statement dependency previews
Preview
Definition 6.4.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0โœ“Lโˆƒโˆ€N

incremental KEM randomness leakage

structure IncrementalRandLeak (kem : KEMScheme m K PK SK C) (inc : kem.IncrementalStructure) where /-- Randomness space for key generation. -/ KeygenRand : Type /-- Randomness space for the first encapsulation stage. -/ Encaps1Rand : Type /-- Randomness space for the second encapsulation stage. -/ Encaps2Rand : Type /-- Key generation together with the randomness used to sample the key pair. -/ keygenRleak : m ((PK ร— SK) ร— KeygenRand) /-- First-stage encapsulation together with its randomness. -/ encaps1Rleak : inc.PKheader โ†’ m ((inc.St ร— inc.Cโ‚ ร— K) ร— Encaps1Rand) /-- Second-stage encapsulation together with its randomness. -/ encaps2Rleak : inc.St โ†’ inc.PKheader โ†’ inc.PKvector โ†’ m (inc.Cโ‚‚ ร— Encaps2Rand) /-- First component: ordinary key generation is the first component of `keygenRleak`. -/ keygen_fst : (do let out โ† keygenRleak pure out.1) = kem.keygen /-- First component: ordinary first-stage encapsulation is the first component of `encaps1Rleak hdr`. -/ encaps1_fst : โˆ€ hdr, (do let out โ† encaps1Rleak hdr pure out.1) = inc.encaps1 hdr /-- First component: ordinary second-stage encapsulation is the first component of `encaps2Rleak st hdr vec`. -/ encaps2_fst : โˆ€ st hdr vec, (do let out โ† encaps2Rleak st hdr vec pure out.1) = inc.encaps2 st hdr vec

ML-KEM incremental randomness leakage

def mlkemIncrementalRandLeak (p : ParameterSet) (ring : NTTRingOps) (prims : Primitives (ParameterSet.params p) (Concrete.concreteEncoding (ParameterSet.params p))) : (mlkemScheme p ring prims).IncrementalRandLeak (mlkemIncremental p ring prims) where KeygenRand := Seed32 ร— Seed32 Encaps1Rand := Message Encaps2Rand := Unit keygenRleak := do let d โ† $แต— Seed32 let z โ† $แต— Seed32 return (keygenInternal ring (Concrete.concreteEncoding (ParameterSet.params p)) prims d z, (d, z)) encaps1Rleak := fun hdr => do let m โ† $แต— Message return (incrementalEncaps1 ring prims hdr m, m) encaps2Rleak := fun st _hdr vec => return (incrementalEncaps2 ring st vec, ()) keygen_fst := p: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 All goals completed! ๐Ÿ™ encaps1_fst := fun _hdr => p:ParameterSetring:NTTRingOpsprims:Primitives p.params (Concrete.concreteEncoding p.params)_hdr:(mlkemIncremental p ring prims).PKheaderโŠข (do let out โ† do let m โ† $แต— Message pure (incrementalEncaps1 ring prims _hdr m, m) pure out.1) = (mlkemIncremental p ring prims).encaps1 _hdr All goals completed! ๐Ÿ™ encaps2_fst := fun _st _hdr _vec => p:ParameterSetring:NTTRingOpsprims:Primitives p.params (Concrete.concreteEncoding p.params)_st:(mlkemIncremental p ring prims).St_hdr:(mlkemIncremental p ring prims).PKheader_vec:(mlkemIncremental p ring prims).PKvectorโŠข (do let out โ† pure (incrementalEncaps2 ring _st _vec, ()) pure out.1) = (mlkemIncremental p ring prims).encaps2 _st _hdr _vec All goals completed! ๐Ÿ™

uses Definition 6.4.1 ยท Definition 6.4.2 ยท github #246

Lean code for Definition6.4.4โ—2 definitions
  • structure(9 fields)defined in SecureMessaging/KEM/IncrementalKEM/Defs.lean
    complete
    structure KEMScheme.IncrementalRandLeak.{u} {m : Type โ†’ Type u} [Monad m]
  {K PK SK C : Type} (kem : KEMScheme m K PK SK C)
  (inc : kem.IncrementalStructure) : Type (max 1 u)
    structure KEMScheme.IncrementalRandLeak.{u}
  {m : Type โ†’ Type u} [Monad m]
  {K PK SK C : Type}
  (kem : KEMScheme m K PK SK C)
  (inc : kem.IncrementalStructure) :
  Type (max 1 u)
    Randomness-leaking versions of the randomized algorithms used by an
incremental KEM construction.

Fine-grained version of `KEMScheme.RandLeak` specifying the leak in each phase.

    Fields

    KeygenRand : Type
    Randomness space for key generation. 
    Encaps1Rand : Type
    Randomness space for the first encapsulation stage. 
    Encaps2Rand : Type
    Randomness space for the second encapsulation stage. 
    keygenRleak : m ((PK ร— SK) ร— self.KeygenRand)
    Key generation together with the randomness used to sample the key pair. 
    encaps1Rleak : inc.PKheader โ†’ m ((inc.St ร— inc.Cโ‚ ร— K) ร— self.Encaps1Rand)
    First-stage encapsulation together with its randomness. 
    encaps2Rleak : inc.St โ†’ inc.PKheader โ†’ inc.PKvector โ†’ m (inc.Cโ‚‚ ร— self.Encaps2Rand)
    Second-stage encapsulation together with its randomness. 
    keygen_fst : (do
    let out โ† self.keygenRleak
    pure out.1) =
  kem.keygen
    First component: ordinary key generation is the first component of
`keygenRleak`. 
    encaps1_fst : โˆ€ (hdr : inc.PKheader),
  (do
      let out โ† self.encaps1Rleak hdr
      pure out.1) =
    inc.encaps1 hdr
    First component: ordinary first-stage encapsulation is the first component of
`encaps1Rleak hdr`. 
    encaps2_fst : โˆ€ (st : inc.St) (hdr : inc.PKheader) (vec : inc.PKvector),
  (do
      let out โ† self.encaps2Rleak st hdr vec
      pure out.1) =
    inc.encaps2 st hdr vec
    First component: ordinary second-stage encapsulation is the first component of
`encaps2Rleak st hdr vec`.
  • defdefined in SecureMessaging/KEM/IncrementalKEM/FromMLKEM.lean
    complete
    def MLKEM.mlkemIncrementalRandLeak (p : MLKEM.ParameterSet)
  (ring : MLKEM.NTTRingOps)
  (prims :
    MLKEM.Primitives p.params
      (MLKEM.Concrete.concreteEncoding p.params)) :
  (MLKEM.mlkemScheme p ring prims).IncrementalRandLeak
    (MLKEM.mlkemIncremental p ring prims)
    def MLKEM.mlkemIncrementalRandLeak
  (p : MLKEM.ParameterSet)
  (ring : MLKEM.NTTRingOps)
  (prims :
    MLKEM.Primitives p.params
      (MLKEM.Concrete.concreteEncoding
        p.params)) :
  (MLKEM.mlkemScheme p ring
        prims).IncrementalRandLeak
    (MLKEM.mlkemIncremental p ring prims)
    Randomness-leakage package for `mlkemIncremental`. Key generation leaks the
FIPS 203 seeds `(d, z)`; first-stage encapsulation leaks the sampled `Message`;
second-stage encapsulation samples nothing, so its leak type is `Unit`.

References: