MsgKeys.lean🔗

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

Declarations on this page (16)

Hybrid Message-Key Derivation and Trace Helpers

Hybrid HKDF message-key derivation (trMsgKeys), protocol constants, and trace-inspection helpers shared by PQXDH and TripleRatchet.

namespace DY.Libsignal.TripleRatchet

@[expose] public section MsgKeys

variable [BytesFunctor] [BytesLength] [BytesFunctor.Has Literal.SubF] [BytesFunctor.Has Concat.SubF]
  [BytesFunctor.Has KdfExtract.SubF]

open Literal Concat KdfExtract

def litL34 ↗#

def lit (s: String): Bytes := literalToBytes s.toUTF8

def litByteL36 ↗#

def litByte (b: UInt8): Bytes := literalToBytes ⟨#[b]⟩

def hmacL38–39 ↗#

HMAC-SHA256 (HKDF-Extract with salt = key, RFC 5869 §2.2).

def hmac (key msg: Bytes): Bytes := kdfExtract key msg

def hkdfBlock1L41–42 ↗#

First three 32-byte RFC 5869 HKDF-Expand output blocks T(1), T(2), T(3) for SHA-256.

def hkdfBlock1 (prk info: Bytes): Bytes := hmac prk (concat info (litByte 1))

def hkdfBlock2L43 ↗#

def hkdfBlock2 (prk info: Bytes): Bytes := hmac prk (concat (hkdfBlock1 prk info) (concat info (litByte 2)))

def hkdfBlock3L44 ↗#

def hkdfBlock3 (prk info: Bytes): Bytes := hmac prk (concat (hkdfBlock2 prk info) (concat info (litByte 3)))

def zeroSaltL46–47 ↗#

Default 32-byte all-zero HKDF salt (optional_salt = None, RFC 5869 §2.2).

def zeroSalt: Bytes := literalToBytes ⟨Array.replicate 32 0⟩

structure MessageKeysL49–54 ↗#

Output of MessageKeys::derive_keys.

structure MessageKeys where
  cipherKey: Bytes
  macKey: Bytes
  /-- Full 32-byte third HKDF block; concretization uses its first 16 bytes as the AES-CBC IV. -/
  iv: Bytes

def trMsgKeysL56–63 ↗#

Hybrid message-key derivation MessageKeys::derive_keys(seed, Some(pqSalt), counter): expands "WhisperMessageKeys" from hmac pqSalt seed. When pqSalt = zeroSalt, this matches the unsalted optional_salt = None path.

def trMsgKeys (pqSalt seed: Bytes): MessageKeys :=
  let prk := hmac pqSalt seed
  { cipherKey := hkdfBlock1 prk (lit "WhisperMessageKeys")
    macKey := hkdfBlock2 prk (lit "WhisperMessageKeys")
    iv := hkdfBlock3 prk (lit "WhisperMessageKeys") }

def messageVersionL65–66 ↗#

CIPHERTEXT_MESSAGE_CURRENT_VERSION (version 4).

def messageVersion: UInt8 := 4

structure SignalMsgL68–75 ↗#

Decoded SignalMessage fields together with the MAC-authenticated wire term and mac.

structure SignalMsg where
  wire: Bytes
  mac: Bytes
  version: UInt8
  ratchetKey: Bytes
  counter: UInt32
  ciphertext: Bytes

def maxForwardJumpsL77–78 ↗#

consts::MAX_FORWARD_JUMPS.

def maxForwardJumps: Nat := 25000

def u32MaxL80–81 ↗#

u32::MAX (index + 1 overflows and aborts in libsignal).

def u32Max: UInt32 := 0xFFFFFFFF

end MsgKeys

@[expose] public section TraceHelpers

def anyEventOnTraceL87–94 ↗#

Whether some EventT entry on tr satisfies p.

def anyEventOnTrace (EventT: Type) [ExecTraceTypes]
    [ExecTraceTypes.Has (ProtocolEvent.ExecEntryT EventT)]
    (tr: ExecTrace) (p: EventT → Bool) : Bool :=
  (List.range tr.length).any fun i =>
    match tr.getEventAt EventT i with
    | some ev => p ev
    | none => false

def guardTraceL96–98 ↗#

Trace guard that succeeds iff p tr holds, without appending to tr.

def guardTrace [ExecTraceTypes] (p: ExecTrace → Bool) : Traceful Unit :=
  Traceful.mk fun tr => (if p tr then some () else none, ⟨tr, byinst✝:ExecTraceTypesp:ExecTrace → Booltr:ExecTrace⊢ tr ≤ tr grindAll goals completed! 🐙⟩)

abbrev getStoredLocalStateAt?L100–105 ↗#

Stored LocalState StateT at trace index idx, if any.

abbrev getStoredLocalStateAt? (StateT: Type) [ExecTraceTypes]
    [ExecTraceTypes.Has (PersistentLocalState.State.ExecEntryT StateT)]
    (tr: ExecTrace) (idx: Nat) : Option (PersistentLocalState.LocalState StateT) :=
  ((tr.at? idx : Option (PersistentGlobalState.State.ExecEntryT
      (PersistentLocalState.LocalState StateT)))).map (·.st)

end TraceHelpers

end DY.Libsignal.TripleRatchet