9.5. ML-KEM Braid🔗

Definition9.5.1

Group: ML-KEM Braid ( ). (3)

Group member previews

Preview

Definition 9.5.7

Loading preview

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

uses 1

Used by 2

Reverse dependency previews

Preview

Definition 9.5.5

Loading preview

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

✓L∃∀N

GitHub#245

ratcheted authenticator interface

structure RatchetedAuthenticator
    (InitKey EpochKey AuthState Header Ciphertext Mac : Type) where
  /-- Initialize authenticator state from an initial key and epoch. -/
  init : InitKey → ℕ → AuthState
  /-- Ratchet the authenticator state with an epoch key at the given epoch. -/
  update : AuthState → ℕ → EpochKey → AuthState
  /-- MAC a header at the given epoch. -/
  macHeader : AuthState → ℕ → Header → Mac
  /-- Verify a MAC on a header at the given epoch. -/
  verifyHeader : AuthState → ℕ → Header → Mac → Bool
  /-- MAC a ciphertext at the given epoch. -/
  macCiphertext : AuthState → ℕ → Ciphertext → Mac
  /-- Verify a MAC on a ciphertext at the given epoch. -/
  verifyCiphertext : AuthState → ℕ → Ciphertext → Mac → Bool
  /-- Honestly produced header MACs verify successfully. -/
  verifyHeader_correct :
    ∀ (s : AuthState) (ep : ℕ) (h : Header),
      verifyHeader s ep h (macHeader s ep h) = true
  /-- Honestly produced ciphertext MACs verify successfully. -/
  verifyCiphertext_correct :
    ∀ (s : AuthState) (ep : ℕ) (c : Ciphertext),
      verifyCiphertext s ep c (macCiphertext s ep c) = true

Lean code for Definition9.5.1●1 definition

structure(8 fields)defined in SecureMessaging/SCKA/MLKEMBraid/Authenticator.lean

complete

structure RatchetedAuthenticator
  (InitKey EpochKey AuthState Header Ciphertext Mac : Type) : Type

structure RatchetedAuthenticator
  (InitKey EpochKey AuthState Header
    Ciphertext Mac : Type) :
  Type

Epoch-indexed MAC state with separate header and ciphertext authentication.

Fields

init : InitKey → ℕ → AuthState

Initialize authenticator state from an initial key and epoch.

update : AuthState → ℕ → EpochKey → AuthState

Ratchet the authenticator state with an epoch key at the given epoch.

macHeader : AuthState → ℕ → Header → Mac

MAC a header at the given epoch.

verifyHeader : AuthState → ℕ → Header → Mac → Bool

Verify a MAC on a header at the given epoch.

macCiphertext : AuthState → ℕ → Ciphertext → Mac

MAC a ciphertext at the given epoch.

verifyCiphertext : AuthState → ℕ → Ciphertext → Mac → Bool

Verify a MAC on a ciphertext at the given epoch.

verifyHeader_correct : ∀ (s : AuthState) (ep : ℕ) (h : Header), self.verifyHeader s ep h (self.macHeader s ep h) = true

Honestly produced header MACs verify successfully.

verifyCiphertext_correct : ∀ (s : AuthState) (ep : ℕ) (c : Ciphertext), self.verifyCiphertext s ep c (self.macCiphertext s ep c) = true

Honestly produced ciphertext MACs verify successfully.

Definition9.5.2

Group: ML-KEM Braid. (4)

Group member previews

Preview

Definition 9.5.3

Loading preview

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

Statement uses 2

Statement dependency previews

Preview

Definition 4.1.2

Loading preview

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

Used by 2

Reverse dependency previews

Preview

Definition 9.5.5

Loading preview

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

✓L∃∀N

incremental KEM, pure receive operations, epoch-key derivation, and streams

structure Parameters (m : Type → Type u) [Monad m] where
  /-- KEM shared secret. -/
  K : Type
  /-- Encapsulation key. -/
  PK : Type
  /-- Decapsulation key. -/
  SK : Type
  /-- Ciphertext. -/
  C : Type
  /-- The key-encapsulation mechanism. -/
  kem : KEMScheme m K PK SK C
  /-- The incremental KEM structure. -/
  inc : kem.IncrementalStructure
  /-- Pure decapsulation agreeing with `kem.decaps`. -/
  hDet : kem.DeterministicDecaps
  /-- Pure second-stage encapsulation agreeing with `inc.encaps2`. -/
  hEnc2 : inc.DeterministicEncaps2
  /-- Epoch key output by `KDF_OK`. -/
  EpochKey : Type
  /-- MAC tag. -/
  Mac : Type
  /-- Erasure-code symbol alphabet, shared by the four streams. -/
  Sym : Type
  /-- `KDF_OK(shared_secret, epoch)`. -/
  kdfOK : K → ℕ → EpochKey
  /-- Header stream, recovering `header ‖ mac`. -/
  ecpHdr : ErasureCodePayload (inc.PKheader × Mac) Sym
  /-- Encapsulation-key-vector stream. -/
  ecpEk : ErasureCodePayload inc.PKvector Sym
  /-- `ct₁` stream. -/
  ecpCt1 : ErasureCodePayload inc.C₁ Sym
  /-- `ct₂` stream, recovering `ct₂ ‖ mac`. -/
  ecpCt2 : ErasureCodePayload (inc.C₂ × Mac) Sym

Lean code for Definition9.5.2●1 definition

structure(16 fields)defined in SecureMessaging/SCKA/MLKEMBraid/Basic.lean

complete

structure MLKEMBraid.Parameters.{u} (m : Type → Type u) [Monad m] : Type (max 1 u)

structure MLKEMBraid.Parameters.{u}
  (m : Type → Type u) [Monad m] :
  Type (max 1 u)

Parameters for the transition system: an incremental KEM, pure implementations of the
KEM operations used by `receive`, epoch-key derivation, and four erasure-coded streams.

Fields

K : Type

KEM shared secret.

PK : Type

Encapsulation key.

SK : Type

Decapsulation key.

C : Type

Ciphertext.

kem : KEMScheme m self.K self.PK self.SK self.C

The key-encapsulation mechanism.

inc : self.kem.IncrementalStructure

The incremental KEM structure.

hDet : self.kem.DeterministicDecaps

Pure decapsulation agreeing with `kem.decaps`.

hEnc2 : self.inc.DeterministicEncaps2

Pure second-stage encapsulation agreeing with `inc.encaps2`.

EpochKey : Type

Epoch key output by `KDF_OK`.

Mac : Type

MAC tag.

Sym : Type

Erasure-code symbol alphabet, shared by the four streams.

kdfOK : self.K → ℕ → self.EpochKey

`KDF_OK(shared_secret, epoch)`.

ecpHdr : ErasureCodePayload (self.inc.PKheader × self.Mac) self.Sym

Header stream, recovering `header ‖ mac`.

ecpEk : ErasureCodePayload self.inc.PKvector self.Sym

Encapsulation-key-vector stream.

ecpCt1 : ErasureCodePayload self.inc.C₁ self.Sym

`ct₁` stream.

ecpCt2 : ErasureCodePayload (self.inc.C₂ × self.Mac) self.Sym

`ct₂` stream, recovering `ct₂ ‖ mac`.

Definition9.5.3

Group: ML-KEM Braid. (4)

Group member previews

Preview

Definition 9.5.2

Loading preview

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

uses 0used by 0✓L∃∀N

message types

inductive MessageType where
  /-- `None`: no payload. -/
  | none
  /-- `Hdr`: header-stream chunk. -/
  | hdr
  /-- `Ek`: encapsulation-key-vector chunk. -/
  | ek
  /-- `EkCt1Ack`: encapsulation-key chunk, and the sender has all of `ct₁`. -/
  | ekCt1Ack
  /-- `Ct1Ack`: the sender has all of `ct₁`, no payload. No transition sends or consumes
  it. -/
  | ct1Ack
  /-- `Ct1`: `ct₁`-stream chunk. -/
  | ct1
  /-- `Ct2`: `ct₂`-stream chunk. -/
  | ct2

protocol message

structure Message (Sym : Type) where
  /-- `epoch`: the epoch being negotiated. -/
  epoch : ℕ
  /-- `type`: which stream, acknowledgment, or empty message this is. -/
  type : MessageType
  /-- `data`: the indexed erasure-code chunk, if any. -/
  data : Option (ℕ × Sym)

Lean code for Definition9.5.3●2 definitions

inductive(7 constructors)defined in SecureMessaging/SCKA/MLKEMBraid/Basic.lean

complete

inductive MLKEMBraid.MessageType : Type

inductive MLKEMBraid.MessageType : Type

The message types.

Constructors

MLKEMBraid.MessageType.none : MLKEMBraid.MessageType

`None`: no payload.

MLKEMBraid.MessageType.hdr : MLKEMBraid.MessageType

`Hdr`: header-stream chunk.

MLKEMBraid.MessageType.ek : MLKEMBraid.MessageType

`Ek`: encapsulation-key-vector chunk.

MLKEMBraid.MessageType.ekCt1Ack : MLKEMBraid.MessageType

`EkCt1Ack`: encapsulation-key chunk, and the sender has all of `ct₁`.

MLKEMBraid.MessageType.ct1Ack : MLKEMBraid.MessageType

`Ct1Ack`: the sender has all of `ct₁`, no payload. No transition sends or consumes
it.

MLKEMBraid.MessageType.ct1 : MLKEMBraid.MessageType

`Ct1`: `ct₁`-stream chunk.

MLKEMBraid.MessageType.ct2 : MLKEMBraid.MessageType

`Ct2`: `ct₂`-stream chunk.

structure(3 fields)defined in SecureMessaging/SCKA/MLKEMBraid/Basic.lean

complete

structure MLKEMBraid.Message (Sym : Type) : Type

structure MLKEMBraid.Message (Sym : Type) : Type

A protocol message containing the negotiated epoch, message type, and optional chunk.

Fields

epoch : ℕ

`epoch`: the epoch being negotiated.

type : MLKEMBraid.MessageType

`type`: which stream, acknowledgment, or empty message this is.

data : Option (ℕ × Sym)

`data`: the indexed erasure-code chunk, if any.

Definition9.5.4

Group: ML-KEM Braid. (4)

Group member previews

Preview

Definition 9.5.2

Loading preview

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

uses 1used by 0✓L∃∀N

the eleven protocol states

inductive State (P : Parameters m) (AuthState : Type) where
  /-- "KeysUnsampled": no additional state. -/
  | keysUnsampled (epoch : ℕ) (auth : AuthState)
  /-- "KeysSampled": `sk`, `ek_vector`, `header_encoder`. -/
  | keysSampled (epoch : ℕ) (auth : AuthState) (sk : P.SK) (ekVector : P.inc.PKvector)
      (headerEncoder : EncoderState (P.inc.PKheader × P.Mac) P.Sym)
  /-- "HeaderSent": `sk`, `ct1_decoder`, `ek_encoder`. -/
  | headerSent (epoch : ℕ) (auth : AuthState) (sk : P.SK)
      (ct1Decoder : DecoderState P.inc.C₁ P.Sym)
      (ekEncoder : EncoderState P.inc.PKvector P.Sym)
  /-- "Ct1Received": `sk`, `ct1`, `ek_encoder`. -/
  | ct1Received (epoch : ℕ) (auth : AuthState) (sk : P.SK) (ct1 : P.inc.C₁)
      (ekEncoder : EncoderState P.inc.PKvector P.Sym)
  /-- "EkSentCt1Received": `sk`, `ct1`, `ct2_decoder`. -/
  | ekSentCt1Received (epoch : ℕ) (auth : AuthState) (sk : P.SK) (ct1 : P.inc.C₁)
      (ct2Decoder : DecoderState (P.inc.C₂ × P.Mac) P.Sym)
  /-- "NoHeaderReceived": `header_decoder`. -/
  | noHeaderReceived (epoch : ℕ) (auth : AuthState)
      (headerDecoder : DecoderState (P.inc.PKheader × P.Mac) P.Sym)
  /-- "HeaderReceived": `header`, `ek_decoder`. -/
  | headerReceived (epoch : ℕ) (auth : AuthState) (header : P.inc.PKheader)
      (ekDecoder : DecoderState P.inc.PKvector P.Sym)
  /-- "Ct1Sampled": `header`, `encaps_state`, `ct1`, `ct1_encoder`, `ek_decoder`. -/
  | ct1Sampled (epoch : ℕ) (auth : AuthState) (header : P.inc.PKheader)
      (encapsState : P.inc.St) (ct1 : P.inc.C₁)
      (ct1Encoder : EncoderState P.inc.C₁ P.Sym)
      (ekDecoder : DecoderState P.inc.PKvector P.Sym)
  /-- "EkReceivedCt1Sampled": `encaps_state`, `ct1`, `header`, `ek_vector`,
  `ct1_encoder`. -/
  | ekReceivedCt1Sampled (epoch : ℕ) (auth : AuthState)
      (encapsState : P.inc.St) (ct1 : P.inc.C₁) (header : P.inc.PKheader)
      (ekVector : P.inc.PKvector) (ct1Encoder : EncoderState P.inc.C₁ P.Sym)
  /-- "Ct1Acknowledged": `header`, `encaps_state`, `ct1`, `ek_decoder`. -/
  | ct1Acknowledged (epoch : ℕ) (auth : AuthState) (header : P.inc.PKheader)
      (encapsState : P.inc.St) (ct1 : P.inc.C₁)
      (ekDecoder : DecoderState P.inc.PKvector P.Sym)
  /-- "Ct2Sampled": `ct2_encoder`. -/
  | ct2Sampled (epoch : ℕ) (auth : AuthState)
      (ct2Encoder : EncoderState (P.inc.C₂ × P.Mac) P.Sym)

Lean code for Definition9.5.4●1 definition

inductive(11 constructors, 4 parameters)defined in SecureMessaging/SCKA/MLKEMBraid/Basic.lean

complete

inductive MLKEMBraid.State.{u} {m : Type → Type u} [Monad m]
  (P : MLKEMBraid.Parameters m) (AuthState : Type) : Type

inductive MLKEMBraid.State.{u} {m : Type → Type u}
  [Monad m] (P : MLKEMBraid.Parameters m)
  (AuthState : Type) : Type

The eleven protocol states, each with an epoch and authenticator state.

Constructors

MLKEMBraid.State.keysUnsampled.{u} {m : Type → Type u}
  [Monad m] {P : MLKEMBraid.Parameters m} {AuthState : Type}
  (epoch : ℕ) (auth : AuthState) :
  MLKEMBraid.State P AuthState

"KeysUnsampled": no additional state.

MLKEMBraid.State.keysSampled.{u} {m : Type → Type u}
  [Monad m] {P : MLKEMBraid.Parameters m} {AuthState : Type}
  (epoch : ℕ) (auth : AuthState) (sk : P.SK)
  (ekVector : P.inc.PKvector)
  (headerEncoder :
    ErasureCodePayload.Streaming.EncoderState
      (P.inc.PKheader × P.Mac) P.Sym) :
  MLKEMBraid.State P AuthState

"KeysSampled": `sk`, `ek_vector`, `header_encoder`.

MLKEMBraid.State.headerSent.{u} {m : Type → Type u}
  [Monad m] {P : MLKEMBraid.Parameters m} {AuthState : Type}
  (epoch : ℕ) (auth : AuthState) (sk : P.SK)
  (ct1Decoder :
    ErasureCodePayload.Streaming.DecoderState P.inc.C₁
      P.Sym)
  (ekEncoder :
    ErasureCodePayload.Streaming.EncoderState P.inc.PKvector
      P.Sym) :
  MLKEMBraid.State P AuthState

"HeaderSent": `sk`, `ct1_decoder`, `ek_encoder`.

MLKEMBraid.State.ct1Received.{u} {m : Type → Type u}
  [Monad m] {P : MLKEMBraid.Parameters m} {AuthState : Type}
  (epoch : ℕ) (auth : AuthState) (sk : P.SK)
  (ct1 : P.inc.C₁)
  (ekEncoder :
    ErasureCodePayload.Streaming.EncoderState P.inc.PKvector
      P.Sym) :
  MLKEMBraid.State P AuthState

"Ct1Received": `sk`, `ct1`, `ek_encoder`.

MLKEMBraid.State.ekSentCt1Received.{u} {m : Type → Type u}
  [Monad m] {P : MLKEMBraid.Parameters m} {AuthState : Type}
  (epoch : ℕ) (auth : AuthState) (sk : P.SK)
  (ct1 : P.inc.C₁)
  (ct2Decoder :
    ErasureCodePayload.Streaming.DecoderState
      (P.inc.C₂ × P.Mac) P.Sym) :
  MLKEMBraid.State P AuthState

"EkSentCt1Received": `sk`, `ct1`, `ct2_decoder`.

MLKEMBraid.State.noHeaderReceived.{u} {m : Type → Type u}
  [Monad m] {P : MLKEMBraid.Parameters m} {AuthState : Type}
  (epoch : ℕ) (auth : AuthState)
  (headerDecoder :
    ErasureCodePayload.Streaming.DecoderState
      (P.inc.PKheader × P.Mac) P.Sym) :
  MLKEMBraid.State P AuthState

"NoHeaderReceived": `header_decoder`.

MLKEMBraid.State.headerReceived.{u} {m : Type → Type u}
  [Monad m] {P : MLKEMBraid.Parameters m} {AuthState : Type}
  (epoch : ℕ) (auth : AuthState) (header : P.inc.PKheader)
  (ekDecoder :
    ErasureCodePayload.Streaming.DecoderState P.inc.PKvector
      P.Sym) :
  MLKEMBraid.State P AuthState

"HeaderReceived": `header`, `ek_decoder`.

MLKEMBraid.State.ct1Sampled.{u} {m : Type → Type u}
  [Monad m] {P : MLKEMBraid.Parameters m} {AuthState : Type}
  (epoch : ℕ) (auth : AuthState) (header : P.inc.PKheader)
  (encapsState : P.inc.St) (ct1 : P.inc.C₁)
  (ct1Encoder :
    ErasureCodePayload.Streaming.EncoderState P.inc.C₁
      P.Sym)
  (ekDecoder :
    ErasureCodePayload.Streaming.DecoderState P.inc.PKvector
      P.Sym) :
  MLKEMBraid.State P AuthState

"Ct1Sampled": `header`, `encaps_state`, `ct1`, `ct1_encoder`, `ek_decoder`.

MLKEMBraid.State.ekReceivedCt1Sampled.{u}
  {m : Type → Type u} [Monad m]
  {P : MLKEMBraid.Parameters m} {AuthState : Type}
  (epoch : ℕ) (auth : AuthState) (encapsState : P.inc.St)
  (ct1 : P.inc.C₁) (header : P.inc.PKheader)
  (ekVector : P.inc.PKvector)
  (ct1Encoder :
    ErasureCodePayload.Streaming.EncoderState P.inc.C₁
      P.Sym) :
  MLKEMBraid.State P AuthState

"EkReceivedCt1Sampled": `encaps_state`, `ct1`, `header`, `ek_vector`,
`ct1_encoder`.

MLKEMBraid.State.ct1Acknowledged.{u} {m : Type → Type u}
  [Monad m] {P : MLKEMBraid.Parameters m} {AuthState : Type}
  (epoch : ℕ) (auth : AuthState) (header : P.inc.PKheader)
  (encapsState : P.inc.St) (ct1 : P.inc.C₁)
  (ekDecoder :
    ErasureCodePayload.Streaming.DecoderState P.inc.PKvector
      P.Sym) :
  MLKEMBraid.State P AuthState

"Ct1Acknowledged": `header`, `encaps_state`, `ct1`, `ek_decoder`.

MLKEMBraid.State.ct2Sampled.{u} {m : Type → Type u}
  [Monad m] {P : MLKEMBraid.Parameters m} {AuthState : Type}
  (epoch : ℕ) (auth : AuthState)
  (ct2Encoder :
    ErasureCodePayload.Streaming.EncoderState
      (P.inc.C₂ × P.Mac) P.Sym) :
  MLKEMBraid.State P AuthState

"Ct2Sampled": `ct2_encoder`.

Definition9.5.5

Group: ML-KEM Braid. (4)

Group member previews

Preview

Definition 9.5.2

Loading preview

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

Statement uses 3

Statement dependency previews

Preview

Definition 4.1.3

Loading preview

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

used by 1✓L∃∀N

send transition

def send (P : Parameters m)
    (auth : RatchetedAuthenticator InitKey P.EpochKey AuthState
      P.inc.PKheader (P.inc.C₁ × P.inc.C₂) P.Mac)
    (st : State P AuthState) : m (SendResult P AuthState)

receive transition

def receive (P : Parameters m) [DecidableEq P.Sym]
    (auth : RatchetedAuthenticator InitKey P.EpochKey AuthState
      P.inc.PKheader (P.inc.C₁ × P.inc.C₂) P.Mac)
    (st : State P AuthState) (msg : Message P.Sym) :
    Except Failure (RecvResult P AuthState)

Lean code for Definition9.5.5●2 definitions

defdefined in SecureMessaging/SCKA/MLKEMBraid/Basic.lean

complete

def MLKEMBraid.send.{u} {m : Type → Type u} [Monad m]
  {InitKey AuthState : Type} (P : MLKEMBraid.Parameters m)
  (auth :
    RatchetedAuthenticator InitKey P.EpochKey AuthState P.inc.PKheader
      (P.inc.C₁ × P.inc.C₂) P.Mac)
  (st : MLKEMBraid.State P AuthState) :
  m (MLKEMBraid.SendResult P AuthState)

def MLKEMBraid.send.{u} {m : Type → Type u}
  [Monad m] {InitKey AuthState : Type}
  (P : MLKEMBraid.Parameters m)
  (auth :
    RatchetedAuthenticator InitKey
      P.EpochKey AuthState P.inc.PKheader
      (P.inc.C₁ × P.inc.C₂) P.Mac)
  (st : MLKEMBraid.State P AuthState) :
  m (MLKEMBraid.SendResult P AuthState)

The protocol send transition for each state.

defdefined in SecureMessaging/SCKA/MLKEMBraid/Basic.lean

complete

def MLKEMBraid.receive.{u} {m : Type → Type u} [Monad m]
  {InitKey AuthState : Type} (P : MLKEMBraid.Parameters m)
  [DecidableEq P.Sym]
  (auth :
    RatchetedAuthenticator InitKey P.EpochKey AuthState P.inc.PKheader
      (P.inc.C₁ × P.inc.C₂) P.Mac)
  (st : MLKEMBraid.State P AuthState) (msg : MLKEMBraid.Message P.Sym) :
  Except MLKEMBraid.Failure (MLKEMBraid.RecvResult P AuthState)

def MLKEMBraid.receive.{u} {m : Type → Type u}
  [Monad m] {InitKey AuthState : Type}
  (P : MLKEMBraid.Parameters m)
  [DecidableEq P.Sym]
  (auth :
    RatchetedAuthenticator InitKey
      P.EpochKey AuthState P.inc.PKheader
      (P.inc.C₁ × P.inc.C₂) P.Mac)
  (st : MLKEMBraid.State P AuthState)
  (msg : MLKEMBraid.Message P.Sym) :
  Except MLKEMBraid.Failure
    (MLKEMBraid.RecvResult P AuthState)

Receive a message. Ill-formed messages and messages that fail the current state's epoch
or type guards are ignored.

Definition9.5.6

Group: ML-KEM Braid. (4)

Group member previews

Preview

Definition 9.5.2

Loading preview

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

Statement uses 2

Statement dependency previews

Preview

Definition 4.1.3

Loading preview

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

used by 1✓L∃∀N

Alice's initial state

def initA (P : Parameters m)
    (auth : RatchetedAuthenticator InitKey P.EpochKey AuthState
      P.inc.PKheader (P.inc.C₁ × P.inc.C₂) P.Mac)
    (ik : InitKey) : State P AuthState

Bob's initial state

def initB (P : Parameters m)
    (auth : RatchetedAuthenticator InitKey P.EpochKey AuthState
      P.inc.PKheader (P.inc.C₁ × P.inc.C₂) P.Mac)
    (ik : InitKey) : State P AuthState

Lean code for Definition9.5.6●2 definitions

defdefined in SecureMessaging/SCKA/MLKEMBraid/Basic.lean

complete

def MLKEMBraid.initA.{u} {m : Type → Type u} [Monad m]
  {InitKey AuthState : Type} (P : MLKEMBraid.Parameters m)
  (auth :
    RatchetedAuthenticator InitKey P.EpochKey AuthState P.inc.PKheader
      (P.inc.C₁ × P.inc.C₂) P.Mac)
  (ik : InitKey) : MLKEMBraid.State P AuthState

def MLKEMBraid.initA.{u} {m : Type → Type u}
  [Monad m] {InitKey AuthState : Type}
  (P : MLKEMBraid.Parameters m)
  (auth :
    RatchetedAuthenticator InitKey
      P.EpochKey AuthState P.inc.PKheader
      (P.inc.C₁ × P.inc.C₂) P.Mac)
  (ik : InitKey) :
  MLKEMBraid.State P AuthState

Alice's initial state: epoch `1`, an initialized authenticator, and no sampled keys.

defdefined in SecureMessaging/SCKA/MLKEMBraid/Basic.lean

complete

def MLKEMBraid.initB.{u} {m : Type → Type u} [Monad m]
  {InitKey AuthState : Type} (P : MLKEMBraid.Parameters m)
  (auth :
    RatchetedAuthenticator InitKey P.EpochKey AuthState P.inc.PKheader
      (P.inc.C₁ × P.inc.C₂) P.Mac)
  (ik : InitKey) : MLKEMBraid.State P AuthState

def MLKEMBraid.initB.{u} {m : Type → Type u}
  [Monad m] {InitKey AuthState : Type}
  (P : MLKEMBraid.Parameters m)
  (auth :
    RatchetedAuthenticator InitKey
      P.EpochKey AuthState P.inc.PKheader
      (P.inc.C₁ × P.inc.C₂) P.Mac)
  (ik : InitKey) :
  MLKEMBraid.State P AuthState

Bob's initial state: epoch `1`, an initialized authenticator, and an empty header decoder.

Definition9.5.7

Group: ML-KEM Braid ( ). (3)

Group member previews

Preview

Definition 9.5.1

Loading preview

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

Statement uses 3

Statement dependency previews

Preview

Definition 9.1.1

Loading preview

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

Used by 2

Reverse dependency previews

Preview

Theorem 9.5.8

Loading preview

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

✓L∃∀N

GitHub#271

ML-KEM Braid as an SCKA scheme

def scheme (P : Parameters m) [DecidableEq P.Sym]
    (auth : RatchetedAuthenticator InitKey P.EpochKey AuthState
      P.inc.PKheader (P.inc.C₁ × P.inc.C₂) P.Mac)
    (irl : P.kem.IncrementalRandLeak P.inc) (sampleInitKey : m InitKey) :
    SCKAScheme m InitKey (State P AuthState) (State P AuthState)
      P.EpochKey (Message P.Sym) (SendRand irl.KeygenRand irl.Encaps1Rand)
    :=
  let sendSCKA (st : State P AuthState) := do
    let r ← send P auth st
    pure (some (r.outputKey, r.msg, r.sendingEpoch, r.state))
  let sendRleakSCKA (st : State P AuthState) := do
    let (r, rand) ← sendRleak P irl auth st
    pure (some (r.outputKey, r.msg, r.sendingEpoch, r.state, rand))
  { initKeyGen := sampleInitKey
    initA := fun ik => pure (initA P auth ik)
    initB := fun ik => pure (initB P auth ik)
    sendA := sendSCKA
    sendArleak := sendRleakSCKA
    recvA := recvSCKA P auth
    sendB := sendSCKA
    sendBrleak := sendRleakSCKA
    recvB := recvSCKA P auth }

Lean code for Definition9.5.7●1 definition

defdefined in SecureMessaging/SCKA/MLKEMBraid/Construction.lean

complete

def MLKEMBraid.scheme.{u} {m : Type → Type u} [Monad m]
  {InitKey AuthState : Type} (P : MLKEMBraid.Parameters m)
  [DecidableEq P.Sym]
  (auth :
    RatchetedAuthenticator InitKey P.EpochKey AuthState P.inc.PKheader
      (P.inc.C₁ × P.inc.C₂) P.Mac)
  (irl : P.kem.IncrementalRandLeak P.inc) (sampleInitKey : m InitKey) :
  SCKAScheme m InitKey (MLKEMBraid.State P AuthState)
    (MLKEMBraid.State P AuthState) P.EpochKey (MLKEMBraid.Message P.Sym)
    (MLKEMBraid.SendRand irl.KeygenRand irl.Encaps1Rand)

def MLKEMBraid.scheme.{u} {m : Type → Type u}
  [Monad m] {InitKey AuthState : Type}
  (P : MLKEMBraid.Parameters m)
  [DecidableEq P.Sym]
  (auth :
    RatchetedAuthenticator InitKey
      P.EpochKey AuthState P.inc.PKheader
      (P.inc.C₁ × P.inc.C₂) P.Mac)
  (irl : P.kem.IncrementalRandLeak P.inc)
  (sampleInitKey : m InitKey) :
  SCKAScheme m InitKey
    (MLKEMBraid.State P AuthState)
    (MLKEMBraid.State P AuthState)
    P.EpochKey (MLKEMBraid.Message P.Sym)
    (MLKEMBraid.SendRand irl.KeygenRand
      irl.Encaps1Rand)

ML-KEM Braid as an `SCKAScheme`. Both parties run the same algorithms and differ
only in their initial state.

Theorem9.5.8

Group: ML-KEM Braid ( ). (3)

Group member previews

Preview

Definition 9.5.1

Loading preview

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

Statement uses 5

Statement dependency previews

Preview

Definition 4.1.4

Loading preview

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

used by 0✓L∃∀N

GitHub#243

\todo

Correctness error bound

theorem correctness_error_le
    (P : Parameters ProbComp) [DecidableEq P.K]
    [DecidableEq P.EpochKey] [DecidableEq P.Sym]
    {InitKey AuthState : Type}
    (auth : RatchetedAuthenticator InitKey P.EpochKey AuthState
      P.inc.PKheader (P.inc.C₁ × P.inc.C₂) P.Mac)
    (irl : P.kem.IncrementalRandLeak P.inc)
    (sampleInitKey : ProbComp InitKey)
    (hHdrCorrect : P.ecpHdr.ec.Correct)
    (hEkCorrect : P.ecpEk.ec.Correct)
    (hCt1Correct : P.ecpCt1.ec.Correct)
    (hCt2Correct : P.ecpCt2.ec.Correct)
    (adv : SCKAScheme.SCKACorrectnessAdversary (Message P.Sym))
    (q : ℕ) (hq : SCKAScheme.SendQueryBound adv q) :
    1 - Pr[= true |
      SCKAScheme.correctnessExp (scheme P auth irl sampleInitKey) adv] ≤
      (q : ℝ≥0∞) * P.kem.correctnessError ProbCompRuntime.probComp

Lean code for Theorem9.5.8●2 theorems

theoremdefined in SecureMessaging/SCKA/MLKEMBraid/Correctness.lean

complete

theorem MLKEMBraid.correctness_error_le (P : MLKEMBraid.Parameters ProbComp)
  [DecidableEq P.K] [DecidableEq P.EpochKey] [DecidableEq P.Sym]
  {InitKey AuthState : Type}
  (auth :
    RatchetedAuthenticator InitKey P.EpochKey AuthState P.inc.PKheader
      (P.inc.C₁ × P.inc.C₂) P.Mac)
  (irl : P.kem.IncrementalRandLeak P.inc)
  (sampleInitKey : ProbComp InitKey) (hHdrCorrect : P.ecpHdr.ec.Correct)
  (hEkCorrect : P.ecpEk.ec.Correct) (hCt1Correct : P.ecpCt1.ec.Correct)
  (hCt2Correct : P.ecpCt2.ec.Correct)
  (adv : SCKAScheme.SCKACorrectnessAdversary (MLKEMBraid.Message P.Sym))
  (q : ℕ) (hq : SCKAScheme.SendQueryBound adv q) :
  1 -
      Pr[= true |
        (MLKEMBraid.scheme P auth irl sampleInitKey).correctnessExp
          adv] ≤
    ↑q * P.kem.correctnessError ProbCompRuntime.probComp

theorem MLKEMBraid.correctness_error_le
  (P : MLKEMBraid.Parameters ProbComp)
  [DecidableEq P.K]
  [DecidableEq P.EpochKey]
  [DecidableEq P.Sym]
  {InitKey AuthState : Type}
  (auth :
    RatchetedAuthenticator InitKey
      P.EpochKey AuthState P.inc.PKheader
      (P.inc.C₁ × P.inc.C₂) P.Mac)
  (irl : P.kem.IncrementalRandLeak P.inc)
  (sampleInitKey : ProbComp InitKey)
  (hHdrCorrect : P.ecpHdr.ec.Correct)
  (hEkCorrect : P.ecpEk.ec.Correct)
  (hCt1Correct : P.ecpCt1.ec.Correct)
  (hCt2Correct : P.ecpCt2.ec.Correct)
  (adv :
    SCKAScheme.SCKACorrectnessAdversary
      (MLKEMBraid.Message P.Sym))
  (q : ℕ)
  (hq : SCKAScheme.SendQueryBound adv q) :
  1 -
      Pr[= true |
        (MLKEMBraid.scheme P auth irl
              sampleInitKey).correctnessExp
          adv] ≤
    ↑q *
      P.kem.correctnessError
        ProbCompRuntime.probComp

With correct erasure codes, every adversary making at most `q` sends across both parties causes
a false correctness flag with probability at most `q` times the KEM correctness error.

theoremdefined in SecureMessaging/SCKA/MLKEMBraid/Correctness.lean

complete

theorem MLKEMBraid.mlkemBraidScheme_correctness_error_le
  (p : MLKEM.ParameterSet) (ring : MLKEM.NTTRingOps)
  (prims :
    MLKEM.Primitives p.params
      (MLKEM.Concrete.concreteEncoding p.params))
  {InitKey AuthState EpochKey Mac Sym : Type} [DecidableEq EpochKey]
  [DecidableEq Sym] (kdfOK : MLKEM.SharedSecret → ℕ → EpochKey)
  (ecpHdr :
    ErasureCodePayload
      ((MLKEM.mlkemIncremental p ring prims).PKheader × Mac) Sym)
  (ecpEk :
    ErasureCodePayload (MLKEM.mlkemIncremental p ring prims).PKvector
      Sym)
  (ecpCt1 :
    ErasureCodePayload (MLKEM.mlkemIncremental p ring prims).C₁ Sym)
  (ecpCt2 :
    ErasureCodePayload ((MLKEM.mlkemIncremental p ring prims).C₂ × Mac)
      Sym)
  (auth :
    RatchetedAuthenticator InitKey EpochKey AuthState
      (MLKEM.mlkemIncremental p ring prims).PKheader
      ((MLKEM.mlkemIncremental p ring prims).C₁ ×
        (MLKEM.mlkemIncremental p ring prims).C₂)
      Mac)
  (sampleInitKey : ProbComp InitKey) (hHdrCorrect : ecpHdr.ec.Correct)
  (hEkCorrect : ecpEk.ec.Correct) (hCt1Correct : ecpCt1.ec.Correct)
  (hCt2Correct : ecpCt2.ec.Correct)
  (adv : SCKAScheme.SCKACorrectnessAdversary (MLKEMBraid.Message Sym))
  (q : ℕ) (hq : SCKAScheme.SendQueryBound adv q) :
  1 -
      Pr[= true |
        (MLKEMBraid.mlkemBraidScheme p ring prims kdfOK ecpHdr ecpEk
              ecpCt1 ecpCt2 auth sampleInitKey).correctnessExp
          adv] ≤
    ↑q *
      (MLKEM.mlkemScheme p ring prims).correctnessError
        ProbCompRuntime.probComp

theorem MLKEMBraid.mlkemBraidScheme_correctness_error_le
  (p : MLKEM.ParameterSet)
  (ring : MLKEM.NTTRingOps)
  (prims :
    MLKEM.Primitives p.params
      (MLKEM.Concrete.concreteEncoding
        p.params))
  {InitKey AuthState EpochKey Mac Sym :
    Type}
  [DecidableEq EpochKey] [DecidableEq Sym]
  (kdfOK :
    MLKEM.SharedSecret → ℕ → EpochKey)
  (ecpHdr :
    ErasureCodePayload
      ((MLKEM.mlkemIncremental p ring
            prims).PKheader ×
        Mac)
      Sym)
  (ecpEk :
    ErasureCodePayload
      (MLKEM.mlkemIncremental p ring
          prims).PKvector
      Sym)
  (ecpCt1 :
    ErasureCodePayload
      (MLKEM.mlkemIncremental p ring
          prims).C₁
      Sym)
  (ecpCt2 :
    ErasureCodePayload
      ((MLKEM.mlkemIncremental p ring
            prims).C₂ ×
        Mac)
      Sym)
  (auth :
    RatchetedAuthenticator InitKey
      EpochKey AuthState
      (MLKEM.mlkemIncremental p ring
          prims).PKheader
      ((MLKEM.mlkemIncremental p ring
            prims).C₁ ×
        (MLKEM.mlkemIncremental p ring
            prims).C₂)
      Mac)
  (sampleInitKey : ProbComp InitKey)
  (hHdrCorrect : ecpHdr.ec.Correct)
  (hEkCorrect : ecpEk.ec.Correct)
  (hCt1Correct : ecpCt1.ec.Correct)
  (hCt2Correct : ecpCt2.ec.Correct)
  (adv :
    SCKAScheme.SCKACorrectnessAdversary
      (MLKEMBraid.Message Sym))
  (q : ℕ)
  (hq : SCKAScheme.SendQueryBound adv q) :
  1 -
      Pr[= true |
        (MLKEMBraid.mlkemBraidScheme p
              ring prims kdfOK ecpHdr
              ecpEk ecpCt1 ecpCt2 auth
              sampleInitKey).correctnessExp
          adv] ≤
    ↑q *
      (MLKEM.mlkemScheme p ring
            prims).correctnessError
        ProbCompRuntime.probComp

The bound of `correctness_error_le` for `mlkemBraidScheme`, using the correctness error of
`MLKEM.mlkemScheme p ring prims`.

Theorem9.5.9

Group: ML-KEM Braid ( ). (3)

Group member previews

Preview

Definition 9.5.1

Loading preview

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

Statement uses 3

Statement dependency previews

Preview

Definition 6.4.1

Loading preview

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

used by 0XL∃∀N

GitHub#244

\todo

LeanLean anchor pending

References:

Signal (2025)
Auerbach et al. (2025)