Secure Messaging

6.3.Β On-Off KEMπŸ”—

Definition6.3.1
Group: Online-Offline Key Encapsulation Mechanism (On-Off KEM). (2)
Group member previews
Preview
Definition 6.3.2
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 0
Used by 5
Reverse dependency previews
Preview
Definition 6.3.4
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
βœ“Lβˆƒβˆ€N

\todo

structure OnOffStructure (kem : KEMScheme m K PK SK C) where /-- Offline encapsulation state space. -/ St : Type /-- Offline ciphertext space. -/ Cβ‚€ : Type /-- Online ciphertext space. -/ C₁ : Type /-- The ciphertext space splits as `ct = (ct0, ct1)`. -/ split : C ≃ Cβ‚€ Γ— C₁ /-- Offline encapsulation `Enc.Off`: key-independent, returns a state and `ct0`. -/ encapsOff : m (St Γ— Cβ‚€) /-- Online encapsulation `Enc.On`: from the state and `pk`, returns `ct1` and the shared key. -/ encapsOn : St β†’ PK β†’ m (C₁ Γ— K) /-- For every public key, `kem.encaps` is equal to first running `encapsOff`, then running `encapsOn st pk`. -/ factor : βˆ€ pk, kem.encaps pk = (do let (st, c0) ← encapsOff let (c1, k) ← encapsOn st pk pure (split.symm (c0, c1), k))

github #40

Lean code for Definition6.3.1●1 definition
  • structure(7 fields)defined in SecureMessaging/KEM/OnOffKEM/Defs.lean
    complete
    structure KEMScheme.OnOffStructure.{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.OnOffStructure.{u}
  {m : Type β†’ Type u} [Monad m]
  {K PK SK C : Type}
  (kem : KEMScheme m K PK SK C) :
  Type (max 1 u)
    An online-offline (on/off) KEM witness for a KEM `kem`
decomposing `kem.encaps` into an offline and an online phase.

- `St`: state produced by the offline encapsulation algorithm;
- `Cβ‚€`, `C₁`: the offline and online ciphertext spaces;
- `split`: identifies the ciphertext space `C` with `Cβ‚€ Γ— C₁`, i.e. `ct = (ct0, ct1)`;
- `encapsOff`: the key-independent offline phase, producing a state and `ct0`;
- `encapsOn st pk`: the online phase, producing `ct1` and the shared key;
- `factor`: `kem.encaps` runs `encapsOff` then `encapsOn`, reassembled via `split`.

    Fields

    St : Type
    Offline encapsulation state space. 
    Cβ‚€ : Type
    Offline ciphertext space. 
    C₁ : Type
    Online ciphertext space. 
    split : C ≃ self.Cβ‚€ Γ— self.C₁
    The ciphertext space splits as `ct = (ct0, ct1)`. 
    encapsOff : m (self.St Γ— self.Cβ‚€)
    Offline encapsulation `Enc.Off`: key-independent, returns a state and `ct0`. 
    encapsOn : self.St β†’ PK β†’ m (self.C₁ Γ— K)
    Online encapsulation `Enc.On`: from the state and `pk`, returns `ct1` and the shared key. 
    factor : βˆ€ (pk : PK),
  kem.encaps pk = do
    let __discr ← self.encapsOff
    match __discr with
      | (st, c0) => do
        let __discr ← self.encapsOn st pk
        match __discr with
          | (c1, k) => pure (self.split.symm (c0, c1), k)
    For every public key, `kem.encaps` is equal to first running `encapsOff`,
then running `encapsOn st pk`.
Definition6.3.2
Group: Online-Offline Key Encapsulation Mechanism (On-Off KEM). (2)
Group member previews
Preview
Definition 6.3.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 0
Used by 2
Reverse dependency previews
Preview
Definition 6.1.1
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
βœ“Lβˆƒβˆ€N

IND-CPA PKE (\KeyGen,\Enc,\Dec) underlying ML-KEM (NIST (2024), Β§5).

\textsf{Notation and public parameters}

\begin{array}{ll} \Rq = \mathbb{Z}_q[X]/(X^{256}+1) & \text{polynomial ring over } \mathbb{Z}_q \text{ with } q=3329 \\ \Tq & \text{NTT-domain ring, isomorphic to } \Rq \\ \NTT:\Rq\to\Tq,\ \NTT^{-1}:\Tq\to\Rq & \text{forward and inverse Number-Theoretic Transforms} \\ \hat{x}=\NTT(x)\in\Tq & \text{NTT-domain value} \\ \langle \hat{u},\hat{v}\rangle \in \Tq & \text{vector product for }\hat{u}, \hat{v} \in \Tq^k \\ \end{array}

\KeyGen(d\in\{0,1\}^{256})

\begin{array}{l} (\rho, \sigma) \gets G(d) \pcomment{\text{seed expansion}} \\ s \gets \SampleVec_1(\sigma,0) \pcomment{\text{small secret vector}} \\ e \gets \SampleVec_1(\sigma,k) \pcomment{\text{small error vector}} \\ \hat{A} \gets \XOF(\rho) \pcomment{\text{public matrix from seed }\rho} \\ \hat{s}, \hat{e} \gets \NTT(s), \NTT(e) \\ \hat{t} \gets \hat{A}\,\hat{s} + \hat{e} \\ \Return (\ek = (\hat{t},\rho),\ \dk = \hat{s}) \end{array}

KeyGen specification in VCVio

def keygenFromSeed (ring : NTTRingOps) (encoding : Encoding params) (prims : Primitives params encoding) (d : Seed32) : PublicKey params encoding Γ— SecretKey params encoding := let (rho, sigma) := prims.gKeygen d let aHat := prims.publicMatrix rho let s := prims.sampleVecEta1 sigma 0 let e := prims.sampleVecEta1 sigma params.k let sHat := ring.nttVec s let eHat := ring.nttVec e let tHat := ring.matVecMul aHat sHat + eHat ({ tHatEncoded := encoding.byteEncode12Vec tHat, rho := rho }, { sHatEncoded := encoding.byteEncode12Vec sHat })
\Enc(\ek=(\hat{t},\rho)\in\Tq^k\times\{0,1\}^{256},\ m\in\{0,1\}^{256};\ \coins\in\{0,1\}^{256})

\begin{array}{l} y \gets \SampleVec_1(\coins,0) \pcomment{\text{small ephemeral vector}} \\ e_1 \gets \SampleVec_2(\coins,k) \pcomment{\text{small error vector}} \\ e_2 \gets \SamplePoly_2(\coins,2k) \pcomment{\text{small error polynomial}} \\ \hat{A} \gets \XOF(\rho) \pcomment{\text{public matrix from seed }\rho} \\ \hat{y} \gets \NTT(y) \\ u \gets \NTT^{-1}(\hat{A}^{\top}\hat{y}) + e_1 \pcomment{\text{first ciphertext component}} \\ \mu \gets \Embed(m) \pcomment{\text{embed message in }\Rq} \\ v \gets \NTT^{-1}(\langle \hat{t}, \hat{y}\rangle) + e_2 + \mu \pcomment{\text{second ciphertext component}} \\ \ct_0 \gets \Compress(u) \pcomment{\text{compress first component}} \\ \ct_1 \gets \Compress(v) \pcomment{\text{compress second component}} \\ \Return \ct=(\ct_0,\ct_1) \end{array}

Enc specification in VCVio

def encrypt (ring : NTTRingOps) (encoding : Encoding params) (prims : Primitives params encoding) (ek : PublicKey params encoding) (msg : Message) (coins : Coins) : Ciphertext params encoding := let tHat := encoding.byteDecode12Vec ek.tHatEncoded let aHat := prims.publicMatrix ek.rho let y := prims.sampleVecEta1 coins 0 let e1 := prims.sampleVecEta2 coins params.k let e2 := prims.prfEta2 coins (2 * params.k) let yHat := ring.nttVec y let u := ring.invNTTVec (ring.matTransposeVecMul aHat yHat) + e1 let mu := encoding.decompress1 (encoding.byteDecode1 msg) let v := ring.invNTT (ring.dot tHat yHat) + e2 + mu { uEncoded := encoding.byteEncodeDUVec (encoding.compressDU u) vEncoded := encoding.byteEncodeDV (encoding.compressDV v) }
\Dec(\dk=\hat{s}\in\Tq^k,\ \ct=(\ct_0,\ct_1))

\begin{array}{l} u' \gets \Decompress(\ctzero) \pcomment{\text{recover the }u\text{ component}} \\ v' \gets \Decompress(\ctone) \pcomment{\text{recover the }v\text{ component}} \\ w \gets v' - \NTT^{-1}(\langle \hat{s}, \NTT(u')\rangle) \pcomment{\text{recover the }\Rq\text{ representative of }m} \\ \Return \Recover(w) \pcomment{\text{decode }\Rq\text{ representative back to }\{0,1\}^{256}} \end{array}

Dec specification in VCVio

def decrypt (ring : NTTRingOps) (encoding : Encoding params) (_prims : Primitives params encoding) (dk : SecretKey params encoding) (c : Ciphertext params encoding) : Message := let (u', v') := encoding.decodeCiphertext c.uEncoded c.vEncoded let sHat := encoding.byteDecode12Vec dk.sHatEncoded let w := v' - ring.invNTT (ring.dot sHat (ring.nttVec u')) encoding.byteEncode1 (encoding.compress1 w)
Lean code for Definition6.3.2●14 definitions
  • defdefined in LatticeCrypto/MLKEM/KPKE.lean
    complete
    def MLKEM.KPKE.keygenFromSeed {params : Params} (ring : NTTRingOps)
  (encoding : Encoding params) (prims : Primitives params encoding)
  (d : Seed32) : PublicKey params encoding Γ— SecretKey params encoding
    def MLKEM.KPKE.keygenFromSeed
  {params : Params} (ring : NTTRingOps)
  (encoding : Encoding params)
  (prims : Primitives params encoding)
  (d : Seed32) :
  PublicKey params encoding Γ—
    SecretKey params encoding
    K-PKE key generation from an explicit 32-byte seed.

This expands the input seed into the public matrix seed `rho` and sampling seed `sigma`,
samples the secret and error vectors, moves them into the NTT domain, and forms the public
key relation `tHat = Ahat * sHat + eHat` before serializing the public and secret outputs.
  • defdefined in LatticeCrypto/MLKEM/KPKE.lean
    complete
    def MLKEM.KPKE.encrypt {params : Params} (ring : NTTRingOps)
  (encoding : Encoding params) (prims : Primitives params encoding)
  (ek : PublicKey params encoding) (msg : Message) (coins : Coins) :
  Ciphertext params encoding
    def MLKEM.KPKE.encrypt {params : Params}
  (ring : NTTRingOps)
  (encoding : Encoding params)
  (prims : Primitives params encoding)
  (ek : PublicKey params encoding)
  (msg : Message) (coins : Coins) :
  Ciphertext params encoding
    K-PKE encryption with explicit coins.

This decodes the public key, deterministically derives the ephemeral secret and noise terms from
`coins`, computes the ML-KEM ciphertext components `(u, v)`, and then compresses and serializes
them into the abstract ciphertext representation.
  • defdefined in LatticeCrypto/MLKEM/KPKE.lean
    complete
    def MLKEM.KPKE.decrypt {params : Params} (ring : NTTRingOps)
  (encoding : Encoding params) (_prims : Primitives params encoding)
  (dk : SecretKey params encoding) (c : Ciphertext params encoding) :
  Message
    def MLKEM.KPKE.decrypt {params : Params}
  (ring : NTTRingOps)
  (encoding : Encoding params)
  (_prims : Primitives params encoding)
  (dk : SecretKey params encoding)
  (c : Ciphertext params encoding) :
  Message
    K-PKE decryption.

This decodes the ciphertext into its semantic `(u, v)` components, subtracts the secret-key
contribution from `v`, and re-encodes the resulting message representative as the recovered
32-byte plaintext.
  • abbrevdefined in LatticeCrypto/MLKEM/Arithmetic.lean
    complete
    abbrev MLKEM.NTTRingOps : Type
    abbrev MLKEM.NTTRingOps : Type
    Optional transform-domain acceleration specialized to ML-KEM carriers.
  • abbrevdefined in LatticeCrypto/MLKEM/Primitives.lean
    complete
    abbrev MLKEM.Primitives.gKeygen {params : Params} {encoding : Encoding params}
  (self : Primitives params encoding) : Seed32 β†’ Seed32 Γ— Seed32
    abbrev MLKEM.Primitives.gKeygen {params : Params}
  {encoding : Encoding params}
  (self : Primitives params encoding) :
  Seed32 β†’ Seed32 Γ— Seed32
    `G(d || k)` from K-PKE key generation, modeled as a pair of 32-byte seeds.
  • abbrevdefined in LatticeCrypto/MLKEM/Primitives.lean
    complete
    abbrev MLKEM.Primitives.prfEta2 {params : Params} {encoding : Encoding params}
  (self : Primitives params encoding) : Seed32 β†’ β„• β†’ Rq
    abbrev MLKEM.Primitives.prfEta2 {params : Params}
  {encoding : Encoding params}
  (self : Primitives params encoding) :
  Seed32 β†’ β„• β†’ Rq
    `PRF_Ξ·β‚‚` followed by CBD sampling, specialized to output one polynomial.
  • defdefined in LatticeCrypto/MLKEM/Primitives.lean
    complete
    def MLKEM.Primitives.publicMatrix {params : Params}
  {encoding : Encoding params} (prims : Primitives params encoding)
  (rho : Seed32) : TqMatrix params.k params.k
    def MLKEM.Primitives.publicMatrix
  {params : Params}
  {encoding : Encoding params}
  (prims : Primitives params encoding)
  (rho : Seed32) :
  TqMatrix params.k params.k
    Reconstruct the public matrix `Γ‚` from the public seed `ρ`.
  • defdefined in LatticeCrypto/MLKEM/Primitives.lean
    complete
    def MLKEM.Primitives.sampleVecEta1 {params : Params}
  {encoding : Encoding params} (prims : Primitives params encoding)
  (seed : Seed32) (offset : β„•) : RqVec params.k
    def MLKEM.Primitives.sampleVecEta1
  {params : Params}
  {encoding : Encoding params}
  (prims : Primitives params encoding)
  (seed : Seed32) (offset : β„•) :
  RqVec params.k
    Sample a length-`k` noise vector using `PRF_η₁` and an explicit counter offset.
  • defdefined in LatticeCrypto/MLKEM/Primitives.lean
    complete
    def MLKEM.Primitives.sampleVecEta2 {params : Params}
  {encoding : Encoding params} (prims : Primitives params encoding)
  (seed : Seed32) (offset : β„•) : RqVec params.k
    def MLKEM.Primitives.sampleVecEta2
  {params : Params}
  {encoding : Encoding params}
  (prims : Primitives params encoding)
  (seed : Seed32) (offset : β„•) :
  RqVec params.k
    Sample a length-`k` noise vector using `PRF_Ξ·β‚‚` and an explicit counter offset.
  • defdefined in LatticeCrypto/MLKEM/Concrete/CBD.lean
    complete
    def MLKEM.Concrete.samplePolyCBD (eta : β„•) (bytes : ByteArray) : Rq
    def MLKEM.Concrete.samplePolyCBD (eta : β„•)
  (bytes : ByteArray) : Rq
    FIPS 203 Algorithm 8: sample a polynomial from the centered binomial distribution CBD_Ξ·.
Input: `64 * eta` bytes. Output: a polynomial in `R_q`.
  • defdefined in LatticeCrypto/MLKEM/Concrete/Encoding.lean
    complete
    def MLKEM.Concrete.compress (d : β„•) (x : Coeff) : Coeff
    def MLKEM.Concrete.compress (d : β„•)
  (x : Coeff) : Coeff
    FIPS 203 Section 4.2.1: `Compress_d(x) = ⌈(2^d / q) Β· xβŒ‹ mod 2^d`.
  • defdefined in LatticeCrypto/MLKEM/Concrete/Encoding.lean
    complete
    def MLKEM.Concrete.decompress (d : β„•) (y : Coeff) : Coeff
    def MLKEM.Concrete.decompress (d : β„•)
  (y : Coeff) : Coeff
    FIPS 203 Section 4.2.1: `Decompress_d(y) = ⌈(q / 2^d) Β· yβŒ‹`.
  • defdefined in LatticeCrypto/MLKEM/Concrete/Encoding.lean
    complete
    def MLKEM.Concrete.byteEncode (d : β„•) (f : Rq) : ByteArray
    def MLKEM.Concrete.byteEncode (d : β„•)
  (f : Rq) : ByteArray
    FIPS 203 Algorithm 4: encode 256 `d`-bit coefficients into `32d` bytes.
  • defdefined in LatticeCrypto/MLKEM/Concrete/Encoding.lean
    complete
    def MLKEM.Concrete.byteDecode (d : β„•) (bytes : ByteArray) : Rq
    def MLKEM.Concrete.byteDecode (d : β„•)
  (bytes : ByteArray) : Rq
    FIPS 203 Algorithm 5: decode `32d` bytes into 256 coefficients.
Definition6.3.3
groupuses 1used by 1βœ“Lβˆƒβˆ€N

Let \Enc,\Dec be the encryption and decryption algorithms of Definition 6.3.2. Following (Auerbach et al. (2025), Β§2, Β§4.1), we define a KEM as follows. The scheme is parameterised by a seed \rho\in\{0,1\}^{256} that generates the public matrix. It is fixed and shared by all key pairs.

\KeyGen()

\begin{array}{l} \sigma \sample \{0,1\}^{256} \pcomment{\text{fresh key-noise seed; }\rho\text{ is fixed}} \\ s \gets \SampleVec_1(\sigma,0) \pcomment{\text{small secret vector}} \\ e \gets \SampleVec_1(\sigma,k) \pcomment{\text{small error vector}} \\ \hat{A} \gets \XOF(\rho) \pcomment{\text{reconstruct public matrix from fixed seed }\rho} \\ \hat{s}, \hat{e} \gets \NTT(s), \NTT(e) \\ \hat{t} \gets \hat{A}\,\hat{s} + \hat{e} \\ \Return (\ek = \hat{t},\ \dk = \hat{s}) \end{array}

def keygen : ProbComp (encoding.EncodedTHat Γ— encoding.EncodedTHat) := do let sigma ← $α΅— Seed32 pure (keygenFromSigma params encoding ring prims rho sigma)
\Encaps(\ek=\hat{t}\in\Tq^k)

\begin{array}{l} \coins \sample \{0,1\}^{256} \\ m \sample \{0,1\}^{256} \pcomment{\text{sample a random message}} \\ \ct \gets \Enc((\hat{t},\rho),\ m;\ \coins) \\ \Return (\ct,\ m) \pcomment{\text{the message }m\text{ is the shared key}} \end{array}

def encaps (ek : encoding.EncodedTHat) : ProbComp ((encoding.EncodedU Γ— encoding.EncodedV) Γ— Message) := do let coins ← $α΅— Coins let msg ← $α΅— Message let ct := KPKE.encrypt ring encoding prims ({ tHatEncoded := ek, rho := rho } : KPKE.PublicKey params encoding) msg coins pure ((ct.uEncoded, ct.vEncoded), msg)
\Decaps(\dk=\hat{s}\in\Tq^k,\ \ct)

\begin{array}{l} m \gets \Dec(\hat{s}, \ct) \\ \Return \mathsf{some}(m) \pcomment{\text{the decrypted message }m\text{ is the shared key}} \end{array}

def decaps (dk : encoding.EncodedTHat) (c : encoding.EncodedU Γ— encoding.EncodedV) : ProbComp (Option Message) := pure (some (KPKE.decrypt ring encoding prims ({ sHatEncoded := dk } : KPKE.SecretKey params encoding) ({ uEncoded := c.1, vEncoded := c.2 } : KPKE.Ciphertext params encoding)))

KEM scheme wiring KeyGen, Encaps, and Decaps

def scheme : KEMScheme ProbComp Message encoding.EncodedTHat encoding.EncodedTHat (encoding.EncodedU Γ— encoding.EncodedV) where keygen := keygen params encoding ring prims rho encaps := encaps params encoding ring prims rho decaps := decaps params encoding ring prims

uses Definition 6.3.2

Lean code for Definition6.3.3●4 definitions
  • defdefined in SecureMessaging/KEM/OnOffKEM/FromKPKE.lean
    complete
    def KPKEOnOff.keygen (params : Params) (encoding : Encoding params)
  (ring : NTTRingOps) (prims : Primitives params encoding)
  (rho : Seed32) :
  ProbComp (encoding.EncodedTHat Γ— encoding.EncodedTHat)
    def KPKEOnOff.keygen (params : Params)
  (encoding : Encoding params)
  (ring : NTTRingOps)
  (prims : Primitives params encoding)
  (rho : Seed32) :
  ProbComp
    (encoding.EncodedTHat Γ—
      encoding.EncodedTHat)
    Key generation against the fixed public matrix `Γ‚ = publicMatrix ρ`.
Mirrors `MLKEM.KPKE.keygenFromSeed` with `ρ` fixed as a public parameter.
  • defdefined in SecureMessaging/KEM/OnOffKEM/FromKPKE.lean
    complete
    def KPKEOnOff.encaps (params : Params) (encoding : Encoding params)
  (ring : NTTRingOps) (prims : Primitives params encoding)
  (rho : Seed32) (ek : encoding.EncodedTHat) :
  ProbComp ((encoding.EncodedU Γ— encoding.EncodedV) Γ— Message)
    def KPKEOnOff.encaps (params : Params)
  (encoding : Encoding params)
  (ring : NTTRingOps)
  (prims : Primitives params encoding)
  (rho : Seed32)
  (ek : encoding.EncodedTHat) :
  ProbComp
    ((encoding.EncodedU Γ—
        encoding.EncodedV) Γ—
      Message)
    Encapsulation: encrypt a uniformly random message (the shared key) under
`MLKEM.KPKE.encrypt` with the fixed public seed `ρ`.
  • defdefined in SecureMessaging/KEM/OnOffKEM/FromKPKE.lean
    complete
    def KPKEOnOff.decaps (params : Params) (encoding : Encoding params)
  (ring : NTTRingOps) (prims : Primitives params encoding)
  (dk : encoding.EncodedTHat)
  (c : encoding.EncodedU Γ— encoding.EncodedV) :
  ProbComp (Option Message)
    def KPKEOnOff.decaps (params : Params)
  (encoding : Encoding params)
  (ring : NTTRingOps)
  (prims : Primitives params encoding)
  (dk : encoding.EncodedTHat)
  (c :
    encoding.EncodedU Γ—
      encoding.EncodedV) :
  ProbComp (Option Message)
    Decapsulation: reassemble the K-PKE ciphertext and run the total
`MLKEM.KPKE.decrypt`. The result is always wrapped in `some`; a K-PKE decryption
error means recovering `m' β‰  m`, not returning `none`.
  • defdefined in SecureMessaging/KEM/OnOffKEM/FromKPKE.lean
    complete
    def KPKEOnOff.scheme (params : Params) (encoding : Encoding params)
  (ring : NTTRingOps) (prims : Primitives params encoding)
  (rho : Seed32) :
  KEMScheme ProbComp Message encoding.EncodedTHat encoding.EncodedTHat
    (encoding.EncodedU Γ— encoding.EncodedV)
    def KPKEOnOff.scheme (params : Params)
  (encoding : Encoding params)
  (ring : NTTRingOps)
  (prims : Primitives params encoding)
  (rho : Seed32) :
  KEMScheme ProbComp Message
    encoding.EncodedTHat
    encoding.EncodedTHat
    (encoding.EncodedU Γ—
      encoding.EncodedV)
    The K-PKE KEM (IND-CPA, no FO transform) with ciphertext space
`C = Cβ‚€ Γ— C₁ = EncodedU Γ— EncodedV`.
Definition6.3.4
group
Statement uses 2
Statement dependency previews
Preview
Definition 6.3.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1βœ“Lβˆƒβˆ€N

Online-offline structure for the KEM specified in Definition 6.3.3 (Auerbach et al. (2025), Def. 2.1). The ciphertext space splits as \C=\C_0\times\C_1 with \ct=(\ctzero,\ctone), and the offline state space is \St=\Tq^k\times\Rq with online state \stct=(\hat{y},e_2), where \hat{y} is in the NTT domain while e_2 remains in coefficient form for the final inverse transform.

\Encaps.\mathsf{Off}()

\begin{array}{l} \coins \sample \{0,1\}^{256} \\ y \gets \SampleVec_1(\coins,0) \pcomment{\text{small ephemeral vector}} \\ e_1 \gets \SampleVec_2(\coins,k) \pcomment{\text{small error vector}} \\ e_2 \gets \SamplePoly_2(\coins,2k) \pcomment{\text{small error polynomial}} \\ \hat{A} \gets \XOF(\rho) \pcomment{\text{reconstruct public matrix from fixed seed }\rho} \\ \hat{y} \gets \NTT(y) \\ u \gets \NTT^{-1}(\hat{A}^{\top}\hat{y}) + e_1 \\ \stct \gets (\hat{y},e_2) \\ \Return (\stct,\ \ctzero = \Compress(u)) \pcomment{\text{compress first component}} \end{array}

def encapsOff : ProbComp ((TqVec params.k Γ— Rq) Γ— encoding.EncodedU) := do let coins ← $α΅— Coins pure (encapsOffFromCoins params encoding ring prims rho coins)
\Encaps.\mathsf{On}(\stct\in\St,\ \ek=\hat{t}\in\Tq^k)

\begin{array}{l} (\hat{y},e_2) \gets \stct \\ m \sample \{0,1\}^{256} \\ \mu \gets \Embed(m) \pcomment{\text{embed message in }\Rq} \\ v \gets \NTT^{-1}(\langle \hat{t}, \hat{y}\rangle) + e_2 + \mu \\ \Return (\ctone = \Compress(v),\ m) \pcomment{\text{the message }m\text{ is the shared key}} \end{array}

def encapsOn (st : TqVec params.k Γ— Rq) (ek : encoding.EncodedTHat) : ProbComp (encoding.EncodedV Γ— Message) := do let msg ← $α΅— Message pure (encapsOnFromMessage params encoding ring st ek msg)
\textsf{Factorization}

\forall\,\ek\in\Tq^k:\quad \Encaps(\ek)\equiv \left[(\stct,\ctzero)\gets\Encaps.\mathsf{Off}();\ (\ctone,K)\gets\Encaps.\mathsf{On}(\stct,\ek);\ \bigl((\ctzero,\ctone),K\bigr)\right]

on-off structure and factorization proof

def onOff : (scheme params encoding ring prims rho).OnOffStructure where St := TqVec params.k Γ— Rq Cβ‚€ := encoding.EncodedU C₁ := encoding.EncodedV split := Equiv.refl (encoding.EncodedU Γ— encoding.EncodedV) encapsOff := encapsOff params encoding ring prims rho encapsOn := encapsOn params encoding ring factor ek := params:Paramsencoding:Encoding paramsring:NTTRingOpsprims:Primitives params encodingrho:Seed32ek:encoding.EncodedTHat⊒ (scheme params encoding ring prims rho).encaps ek = do let __discr ← encapsOff params encoding ring prims rho match __discr with | (st, c0) => do let __discr ← encapsOn params encoding ring st ek match __discr with | (c1, k) => pure ((Equiv.refl (encoding.EncodedU Γ— encoding.EncodedV)).symm (c0, c1), k) All goals completed! πŸ™

uses Definition 6.3.1 Β· Definition 6.3.3 Β· github #41

Lean code for Definition6.3.4●3 definitions
  • defdefined in SecureMessaging/KEM/OnOffKEM/FromKPKE.lean
    complete
    def KPKEOnOff.encapsOff (params : Params) (encoding : Encoding params)
  (ring : NTTRingOps) (prims : Primitives params encoding)
  (rho : Seed32) : ProbComp ((TqVec params.k Γ— Rq) Γ— encoding.EncodedU)
    def KPKEOnOff.encapsOff (params : Params)
  (encoding : Encoding params)
  (ring : NTTRingOps)
  (prims : Primitives params encoding)
  (rho : Seed32) :
  ProbComp
    ((TqVec params.k Γ— Rq) Γ—
      encoding.EncodedU)
    Offline encapsulation `Enc.Off`: sample fresh coins, derive the ephemeral
vector `y` and noise `e1`, `e2`, compute `u = invNTTVec (Γ‚α΅€ Ε·) + e1`, and output
its compressed encoding as `ct0` together with the minimal online state `(Ε·, e2)`.
Independent of the encapsulation key.
  • defdefined in SecureMessaging/KEM/OnOffKEM/FromKPKE.lean
    complete
    def KPKEOnOff.encapsOn (params : Params) (encoding : Encoding params)
  (ring : NTTRingOps) (st : TqVec params.k Γ— Rq)
  (ek : encoding.EncodedTHat) : ProbComp (encoding.EncodedV Γ— Message)
    def KPKEOnOff.encapsOn (params : Params)
  (encoding : Encoding params)
  (ring : NTTRingOps)
  (st : TqVec params.k Γ— Rq)
  (ek : encoding.EncodedTHat) :
  ProbComp (encoding.EncodedV Γ— Message)
    Online encapsulation `Enc.On`: from the minimal offline state `(Ε·, e2)` and
the encapsulation key `ek = tΜ‚`, sample the message `m` (the shared key), compute
`v = invNTT ⟨tΜ‚, ŷ⟩ + e2 + decompress₁ (decode₁ m)`, and output its compressed
encoding as `ct1`.
  • defdefined in SecureMessaging/KEM/OnOffKEM/FromKPKE.lean
    complete
    def KPKEOnOff.onOff (params : Params) (encoding : Encoding params)
  (ring : NTTRingOps) (prims : Primitives params encoding)
  (rho : Seed32) :
  (KPKEOnOff.scheme params encoding ring prims rho).OnOffStructure
    def KPKEOnOff.onOff (params : Params)
  (encoding : Encoding params)
  (ring : NTTRingOps)
  (prims : Primitives params encoding)
  (rho : Seed32) :
  (KPKEOnOff.scheme params encoding ring
      prims rho).OnOffStructure
    The online-offline structure for the K-PKE KEM: the ciphertext splits as
`ct = (ct0, ct1)`, and `factor` proves that the KEM's encapsulation
(`MLKEM.KPKE.encrypt`) equals the offline phase `encapsOff` followed by the
online phase `encapsOn`.
Definition6.3.5
Group: Online-Offline Key Encapsulation Mechanism (On-Off KEM). (2)
Group member previews
Preview
Definition 6.3.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 2
Statement dependency previews
Preview
Definition 6.3.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 3
Reverse dependency previews
Preview
Definition 9.4.1
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
βœ“Lβˆƒβˆ€N

On-Off KEM randomness leakage

structure OnOffRandLeak (kem : KEMScheme m K PK SK C) (onoff : kem.OnOffStructure) where /-- Randomness space for key generation. -/ KeygenRand : Type /-- Randomness space for offline encapsulation. -/ OffRand : Type /-- Randomness space for online encapsulation. -/ OnRand : Type /-- Key generation together with the randomness used to sample the key pair. -/ keygenRleak : m ((PK Γ— SK) Γ— KeygenRand) /-- Offline encapsulation together with its randomness. -/ encapsOffRleak : m ((onoff.St Γ— onoff.Cβ‚€) Γ— OffRand) /-- Online encapsulation together with its randomness. -/ encapsOnRleak : onoff.St β†’ PK β†’ m ((onoff.C₁ Γ— K) Γ— OnRand) /-- 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 offline encapsulation is the first component of `encapsOffRleak`. -/ encapsOff_fst : (do let out ← encapsOffRleak pure out.1) = onoff.encapsOff /-- First component: ordinary online encapsulation is the first component of `encapsOnRleak st pk`. -/ encapsOn_fst : βˆ€ st pk, (do let out ← encapsOnRleak st pk pure out.1) = onoff.encapsOn st pk

K-PKE On-Off randomness leakage

def onOffRandLeak : (scheme params encoding ring prims rho).OnOffRandLeak (onOff params encoding ring prims rho) where KeygenRand := Seed32 OffRand := Coins OnRand := Message keygenRleak := do let sigma ← $α΅— Seed32 pure (keygenFromSigma params encoding ring prims rho sigma, sigma) encapsOffRleak := do let coins ← $α΅— Coins pure (encapsOffFromCoins params encoding ring prims rho coins, coins) encapsOnRleak := fun st ek => do let msg ← $α΅— Message pure (encapsOnFromMessage params encoding ring st ek msg, msg) keygen_fst := params:Paramsencoding:Encoding paramsring:NTTRingOpsprims:Primitives params encodingrho:Seed32⊒ (do let out ← do let sigma ← $α΅— Seed32 pure (keygenFromSigma params encoding ring prims rho sigma, sigma) pure out.1) = (scheme params encoding ring prims rho).keygen All goals completed! πŸ™ encapsOff_fst := params:Paramsencoding:Encoding paramsring:NTTRingOpsprims:Primitives params encodingrho:Seed32⊒ (do let out ← do let coins ← $α΅— Coins pure (encapsOffFromCoins params encoding ring prims rho coins, coins) pure out.1) = (onOff params encoding ring prims rho).encapsOff All goals completed! πŸ™ encapsOn_fst := fun st _ek => params:Paramsencoding:Encoding paramsring:NTTRingOpsprims:Primitives params encodingrho:Seed32st:(onOff params encoding ring prims rho).St_ek:encoding.EncodedTHat⊒ (do let out ← do let msg ← $α΅— Message pure (encapsOnFromMessage params encoding ring st _ek msg, msg) pure out.1) = (onOff params encoding ring prims rho).encapsOn st _ek params:Paramsencoding:Encoding paramsring:NTTRingOpsprims:Primitives params encodingrho:Seed32_ek:encoding.EncodedTHatfst✝:TqVec params.ksnd✝:Rq⊒ (do let out ← do let msg ← $α΅— Message pure (encapsOnFromMessage params encoding ring (fst✝, snd✝) _ek msg, msg) pure out.1) = (onOff params encoding ring prims rho).encapsOn (fst✝, snd✝) _ek All goals completed! πŸ™

uses Definition 6.3.1 Β· Definition 6.3.4 Β· github #248

Lean code for Definition6.3.5●2 definitions
  • structure(9 fields)defined in SecureMessaging/KEM/OnOffKEM/Defs.lean
    complete
    structure KEMScheme.OnOffRandLeak.{u} {m : Type β†’ Type u} [Monad m]
  {K PK SK C : Type} (kem : KEMScheme m K PK SK C)
  (onoff : kem.OnOffStructure) : Type (max 1 u)
    structure KEMScheme.OnOffRandLeak.{u}
  {m : Type β†’ Type u} [Monad m]
  {K PK SK C : Type}
  (kem : KEMScheme m K PK SK C)
  (onoff : kem.OnOffStructure) :
  Type (max 1 u)
    Randomness-leaking versions of the randomized algorithms used by an
online-offline KEM construction.

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

    Fields

    KeygenRand : Type
    Randomness space for key generation. 
    OffRand : Type
    Randomness space for offline encapsulation. 
    OnRand : Type
    Randomness space for online encapsulation. 
    keygenRleak : m ((PK Γ— SK) Γ— self.KeygenRand)
    Key generation together with the randomness used to sample the key pair. 
    encapsOffRleak : m ((onoff.St Γ— onoff.Cβ‚€) Γ— self.OffRand)
    Offline encapsulation together with its randomness. 
    encapsOnRleak : onoff.St β†’ PK β†’ m ((onoff.C₁ Γ— K) Γ— self.OnRand)
    Online 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`. 
    encapsOff_fst : (do
    let out ← self.encapsOffRleak
    pure out.1) =
  onoff.encapsOff
    First component: ordinary offline encapsulation is the first component of
`encapsOffRleak`. 
    encapsOn_fst : βˆ€ (st : onoff.St) (pk : PK),
  (do
      let out ← self.encapsOnRleak st pk
      pure out.1) =
    onoff.encapsOn st pk
    First component: ordinary online encapsulation is the first component of
`encapsOnRleak st pk`.
  • defdefined in SecureMessaging/KEM/OnOffKEM/FromKPKE.lean
    complete
    def KPKEOnOff.onOffRandLeak (params : Params) (encoding : Encoding params)
  (ring : NTTRingOps) (prims : Primitives params encoding)
  (rho : Seed32) :
  (KPKEOnOff.scheme params encoding ring prims rho).OnOffRandLeak
    (KPKEOnOff.onOff params encoding ring prims rho)
    def KPKEOnOff.onOffRandLeak (params : Params)
  (encoding : Encoding params)
  (ring : NTTRingOps)
  (prims : Primitives params encoding)
  (rho : Seed32) :
  (KPKEOnOff.scheme params encoding ring
        prims rho).OnOffRandLeak
    (KPKEOnOff.onOff params encoding ring
      prims rho)
    Randomness-leakage package for `onOff`. Key generation leaks the seed
`Οƒ`; offline encapsulation leaks the encryption coins; online encapsulation
leaks the sampled message (shared key).