RootKdfDefs.lean🔗

Tier 2 · definitions used by the computational proof 2 headline theorems depend on it 32 of 79 lines trusted trust banner B2, trusted: definitions used by the statement 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.

Declarations on this page (8)

libsignal's root KDF as a PRF-PRNG

Trusted: definitions used by the statement. The theorems of Computational/Theorems/ use every definition in this file: read them. The theorems here are checked by Lean. See Computational/docs/TRUSTED_BASE.md.

Models the HKDF-SHA256 step of libsignal v0.105.4 RootKey::create_chain (rust/protocol/src/ratchet/keys.rs:199–218, info "WhisperRatchet", 64-byte output split into 32-byte root and chain keys) as rootKdf, packages it as the ACD19 PRF-PRNG rootPRNG (a named assumption of the session theorem, DEV-LS30), and defines its single-step PRG/PRF components expandPRG and extractPRF.

@[expose] public section

open OracleComp OracleSpec ENNReal

namespace CryptoGames

namespace Ratchet

open HMAC HKDF CBC MACScheme

abbrev RootKeyL38–39 ↗#

256-bit root key as its 32 LE bytes (RootKey.key : [u8; 32], keys.rs:185–188).

abbrev RootKey := BitVec 256

def whisperRatchetInfoL41–43 ↗#

HKDF info "WhisperRatchet" (14 ASCII bytes, keys.rs:207).

def whisperRatchetInfo : List (BitVec 8) :=
  "WhisperRatchet".toList.map fun c => BitVec.ofNat 8 c.toNat

def rootSaltL45–47 ↗#

HKDF salt Some(&self.key) (keys.rs:206).

def rootSalt (rk : RootKey) : Salt :=
  some ⟨keyToBytes32 rk, byrk:RootKey⊢ (keyToBytes32 rk).length = 32 simp [keyToBytes32]All goals completed! 🐙⟩

def rootExpandL49–53 ↗#

HKDF-Expand(prk, "WhisperRatchet", 64) split into (rootKey, chainKey) (keys.rs:205–209).

def rootExpand (F : ShaState → List (BitVec 8) → ShaState) (prk : List (BitVec 8)) :
    RootKey × ChainKey :=
  let okm := hkdfExpand F prk whisperRatchetInfo 64
  (bytesToKey32 (okm.take 32), bytesToKey32 ((okm.drop 32).take 32))

def rootKdfL55–60 ↗#

RootKey::create_chain KDF step (keys.rs:204–217): HKDF(salt = rk, ikm, "WhisperRatchet", 64) split into (okm[0..32], okm[32..64]).

def rootKdf (F : ShaState → List (BitVec 8) → ShaState) (rk : RootKey) (ikm : List (BitVec 8)) :
    RootKey × ChainKey :=
  let okm := hkdf F (rootSalt rk) ikm whisperRatchetInfo 64
  (bytesToKey32 (okm.take 32), bytesToKey32 ((okm.drop 32).take 32))

def rootPRNGL62–66 ↗#

Root KDF packaged as an ACD19 PRFPRNG (init = id, up σ I = rootKdf F σ (enc I)).

def rootPRNG (F : ShaState → List (BitVec 8) → ShaState) {Pt : Type} (enc : Pt → List (BitVec 8)) :
    PRFPRNG RootKey RootKey Pt ChainKey where
  init := id
  up σ I := rootKdf F σ (enc I)

def expandPRGL68–71 ↗#

rootExpand as a PRG from a uniform 256-bit PRK to RootKey × ChainKey.

def expandPRG (F : ShaState → List (BitVec 8) → ShaState) :
    PRGScheme (BitVec 256) (RootKey × ChainKey) :=
  ⟨fun prk => rootExpand F (keyToBytes32 prk)⟩

def extractPRFL73–80 ↗#

HKDF-Extract keyed by the root key in the salt slot as a PRF RootKey → Pt → BitVec 256.

def extractPRF (F : ShaState → List (BitVec 8) → ShaState) {Pt : Type}
    (enc : Pt → List (BitVec 8)) : MACScheme RootKey Pt (BitVec 256) :=
  ⟨fun σ I => bytesToKey32 (hkdfExtract F (rootSalt σ) (enc I))⟩

end Ratchet

end CryptoGames