EffSalt.lean🔗

Tier 2 · definitions used by the computational proof 1 headline theorem depend on it 6 of 44 lines trusted trust banner B3, trusted in part source ↗

Read the definitions shown. Only the declarations that the headline statements use are shown, with the namespace, section, open and variable commands needed to read them. The collapsed runs are theorems, which Lean checks, and definitions that no headline statement uses.

The effective 32-byte HKDF salt (DEV-LS25)

Trusted in part. The theorems of Computational/Theorems/ use the general-length normaliser effectiveHkdfSalt and fit32 (Lemma 1's one-key first-message Auth game, Computational/Specifications/Pqxdh/Security/Auth/Game.lean, effectiveHkdfSaltBytes): read them. effectiveHkdfSalt32 is checked by Lean. See Computational/docs/TRUSTED_BASE.md.

In MessageKeys::derive_keys, HKDF-Extract computes HMAC-SHA256(salt, ikm) with None mapped to 32 zero bytes. Because HMAC zero-pads keys of length at most 64 to the 64-byte block, any salt of at most 32 bytes acts solely through its 32-byte zero-padded form (None, Some([]), and Some(0^32) coincide); PRF assumptions on salts are stated over this effective 32-byte salt.

@[expose] public section

namespace CryptoGames

def fit32L32–45 ↗#

Pad with zeros (or truncate) a list to 32 entries.

def fit32 {α : Type} [OfNat α 0] (s : List α) : List.Vector α 32 :=
  ⟨s.take 32 ++ List.replicate (32 - s.length) 0, byα:Typeinst✝:OfNat α 0s:List α⊢ (List.take 32 s ++ List.replicate (32 - s.length) 0).length = 32 simpα:Typeinst✝:OfNat α 0s:List α⊢ min 32 s.length + (32 - s.length) = 32; omegaAll goals completed! 🐙⟩

def effectiveHkdfSaltL36–38 ↗#

Effective 32-byte HKDF salt of an optional salt (none ↦ 0^32, some s ↦ fit32 s).

def effectiveHkdfSalt {α : Type} [OfNat α 0] (salt? : Option (List α)) : List.Vector α 32 :=
  (salt?.map fit32).getD (List.Vector.replicate 32 0)

1 declaration not shown (lines 40–42): theorems, which Lean checks, or definitions that no headline statement uses

CryptoGames.effectiveHkdfSalt32

end CryptoGames