ChainDefs.lean🔗

Tier 2 · definitions used by the computational proof 2 headline theorems depend on it 13 of 69 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.

libsignal's symmetric ratchet: the chain step and HMAC as a PRF on chain keys

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 libsignal v0.105.4 ChainKey (rust/protocol/src/ratchet/keys.rs:140–183): one-byte domain-separated HMAC-SHA256 (chainHmac, messageKeySeed = 0x01, chainKeySeed = 0x02) and its PRF view hmacPRF.

@[expose] public section

open OracleComp OracleSpec ENNReal

namespace CryptoGames

namespace Ratchet

open HMAC HKDF CBC LibsignalAead MACScheme AEADScheme

abbrev ChainKeyL36–37 ↗#

256-bit chain key as its 32 LE bytes (ChainKey.key : [u8; 32]).

abbrev ChainKey := BitVec 256

def chainHmacL39–42 ↗#

ChainKey::calculate_base_material: HMAC-SHA256(ck, [b]).

def chainHmac (F : ShaState → List (BitVec 8) → ShaState) (ck : ChainKey) (b : BitVec 8) :
    List (BitVec 8) :=
  hmacWith F (keyToBytes32 ck) [b]

def messageKeySeedL44–45 ↗#

ChainKey::MESSAGE_KEY_SEED (keys.rs:148).

def messageKeySeed : BitVec 8 := 0x01

def chainKeySeedL47–48 ↗#

ChainKey::CHAIN_KEY_SEED (keys.rs:149).

def chainKeySeed : BitVec 8 := 0x02

def hmacPRFL50–52 ↗#

HMAC-SHA256 on one-byte inputs as a 256-bit PRF (32 LE bytes).

def hmacPRF (F : ShaState → List (BitVec 8) → ShaState) : MACScheme ChainKey (BitVec 8) ChainKey :=
  ⟨fun ck b => bytesToKey32 (chainHmac F ck b)⟩

end Ratchet

end CryptoGames