CreateChainDefs.lean🔗

Tier 2 · definitions used by the computational proof and symbolic proof 6 headline theorems depend on it 16 of 55 lines trusted 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.

RootKey::create_chain with the X25519 agreement, over abstract SHA-256 and X25519

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 X25519 key-agreement half of libsignal v0.105.4 RootKey::create_chain (rust/protocol/src/ratchet/keys.rs:199–218): RFC 7748 scalar clamping (clampScalar), abstract X25519 evaluation (X25519Fn), all-zero shared-secret rejection, and HKDF root derivation via rootKdf.

@[expose] public section

namespace CryptoGames

namespace Ratchet

open HMAC HKDF

abbrev X25519FnL34–36 ↗#

Abstract X25519 function mapping 32 clamped scalar bytes and 32 u-coordinate bytes to 32 u-coordinate bytes (all LE).

abbrev X25519Fn := List.Vector (BitVec 8) 32 → List.Vector (BitVec 8) 32 → List.Vector (BitVec 8) 32

def clampScalarL38–40 ↗#

curve25519_dalek::scalar::clamp_integer (v5.0.0): k[0] &= 0xf8; k[31] &= 0x7f; k[31] |= 0x40.

def clampScalar (k : List.Vector (BitVec 8) 32) : List.Vector (BitVec 8) 32 :=
  ((k.set 0 (k.get 0 &&& 0xf8#8)).set 31 ((k.get 31 &&& 0x7f#8) ||| 0x40#8))

def keyToBytesVec32L42–44 ↗#

32 LE bytes of a 256-bit key as a List.Vector.

def keyToBytesVec32 (k : BitVec 256) : List.Vector (BitVec 8) 32 :=
  ⟨keyToBytes32 k, byk:BitVec 256⊢ (keyToBytes32 k).length = 32 simp [keyToBytes32]All goals completed! 🐙⟩

def createChainL46–52 ↗#

RootKey::create_chain over abstract SHA-256 F and X25519 X: computes ss = X (clampScalar priv) pub, returning none if ss is all zero and rootKdf F rk ss.toList otherwise.

def createChain (F : ShaState → List (BitVec 8) → ShaState) (X : X25519Fn) (rk : RootKey)
    (pub priv : List.Vector (BitVec 8) 32) : Option (RootKey × ChainKey) :=
  let ss := X (clampScalar priv) pub
  if ss.toList = List.replicate 32 0#8 then none else some (rootKdf F rk ss.toList)

end Ratchet

end CryptoGames