9.2. ML-KEM Braid
Definition9.2.1
Group: ML-KEM Braid ( ). (3)
Associated Lean declarations
-
RatchetedAuthenticator[complete]
\todo
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
uses Definition 9.1.1 · github #245
Lean code for Definition9.2.1●1 definition
Associated Lean declarations
-
RatchetedAuthenticator[complete]
Associated Lean declarations
-
RatchetedAuthenticator[complete]
-
structuredefined in SecureMessaging/SCKA/MLKEMBraid/Authenticator.leancomplete
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.2.2
Group: ML-KEM Braid ( ). (3)
Statement uses 3
Used by 2
Lean status
- No associated Lean code or declarations.
\todo
LeanLean anchor pending
uses Definition 9.1.1 · Definition 6.4.1 · Definition 9.2.1 · github #271
Theorem9.2.3
Group: ML-KEM Braid ( ). (3)
Statement uses 3
Lean status
- No associated Lean code or declarations.
\todo
LeanLean anchor pending
uses Definition 9.2.2 · Definition 9.1.3 · Definition 6.4.1 · github #243
Theorem9.2.4
Group: ML-KEM Braid ( ). (3)
Statement uses 3
Lean status
- No associated Lean code or declarations.
\todo
LeanLean anchor pending
uses Definition 9.2.2 · Definition 9.1.4 · Definition 6.4.1 · github #244
References:
-
Signal (2025)