LibsignalSMInstance.lean
Declarations on this page (14)
The Fig. 8 instance with public message components, and the libsignal session as an SMSchemeR
Trusted in part. The theorems of Computational/ use only 26 definitions of this file, listed in Computational/ §3: read them. Everything else here is checked by Lean.
Instantiates ACD19 Fig. 8 on libsignal's primitives (lFig8 over lFS, lChainPRG, lAead, lAeadK, lAeadR, lIdeal, lPubOf, lWire, lHeader, lIds, dummyKey, Salt32, Libsignal, LibsignalMsgPublicPart, DEV-LS8, DEV-LS13, DEV-LS14), wraps the session model with given epoch-0 keys as an SMSchemeR (libsignal, DEV-LS26, DEV-LS27), and defines the game configuration (ratchetKeyAdmissible, configR1OnCurve, DEV-LS1, DEV-LS3, DEV-LS4, DEV-LS5, DEV-LS6, DEV-LS7), the DH realization predicate (X25519RealizesDh, DEV-LS29), and the salt-PRF / wire-OT-CCA reductions and forgery bound (lSaltPRF32, lSaltRed, lRandSaltBias, LibsignalWireOracleSpec, lWireRed, macForgeryProb, SaltSlotSt, slotKeyOf, isSlotChalSalt, slotSaltImpl, slotSaltImplNF, slotSaltRed, slotWireRed, DEV-LS23, DEV-LS25, DEV-LS31).
@[expose] public sectionopen OracleComp OracleSpec ENNRealnamespace CryptoGamesnamespace Ratchetnamespace LibsignalInstopen HMAC HKDF CBC LibsignalAead SM.Construction CKA LibsignalSession AEADScheme MACSchemeabbrev Salt32
The salt carried by the Fig. 8 instance: the 32-byte effective HKDF salt of the SPQR message key (effectiveHkdfSalt32: a missing salt is 0^32). HKDF-Extract keyed by an absent salt and by 0^32 computes the same function (msgKeys_effSalt), so the instance carries the key HKDF actually uses: a PRF over salts is then a PRF over {0,1}^256 (BBGS'23 Thm 11).
abbrev Salt32 := List.Vector (BitVec 8) 32
abbrev Libsignal
The ciphertext of the per-message AEAD: the wire (serialized message, 8-byte tag) and the salt attached to it (not on the wire).
abbrev LibsignalCiphertextWithSalt32 := (List (BitVec 8) × BitVec 64) × Salt32structure LibsignalMsgPublicPart
Public message components (previous_counter, SPQR wire message, effective HKDF salt, and address blob).
DEV-LS13 (libsignal): public message parts. libsignal sends previous_counter, the SPQR message, and unacknowledged addresses in the clear (MACed) and derives message keys with the SPQR salt; challenges in lFig8 must agree on LibsignalMsgPublicPart (EqualPubChalls).
structure LibsignalMsgPublicPart where
pn : BitVec 32
/-- SPQR wire message (`pq_ratchet`). -/
pqmsg : List (BitVec 8)
/-- Effective 32-byte HKDF salt of the message keys (ghost, not on the wire). -/
salt : Salt32
addrs : Option (List (BitVec 8))
deriving DecidableEq2 declarations not shown (lines 74–79): theorems, which Lean checks, or definitions that no headline statement uses
CryptoGames., CryptoGames.
def dummyKey
Placeholder public key (0xff^32, non-canonical u ≥ 2²⁵⁵ - 19 outside encT's image) used for Fig. 8's unused epoch-0 header (0, none).
def dummyKey : PublicKey := ⟨List.Vector.replicate 32 0xff⟩2 declarations not shown (lines 85–92): theorems, which Lean checks, or definitions that no headline statement uses
CryptoGames., CryptoGames.
abbrev lWire
The wire AEAD (libsignalWireAead) with libsignal's codec and plaintext length ℓ, no address check.
abbrev lWire (C : Crypto) (codec : SignalMessageProtoCodec) (ℓ : ℕ) :=
libsignalWireAead C.E C.D C.F ℓ (signalWireCodec codec) (fun _ => none) nonedef lAeadK
The per-message AEAD keyed by the message keys themselves (no salt check): lAead after deriveMessageKeys F (some salt) seed.
def lAeadK {Pt : Type} (C : Crypto) (codec : SignalMessageProtoCodec) (ℓ : ℕ) (encT : Pt → PublicKey)
(idOf : Party → IdentityKey) :
AEADScheme DerivedMessageKeys ((ℕ × Header Pt) × LibsignalMsgPublicPart) (Plain ℓ) LibsignalCiphertextWithSalt32 where
enc mk a m := ((lWire C codec ℓ).enc mk (lIds idOf a.1.2.1) (lHeader encT a.1.1 a.1.2 a.2) m, a.2.salt)
dec mk a c :=
match (lWire C codec ℓ).dec mk (lIds idOf a.1.2.1) c.1 with
| none => none
| some (h, m) => if h = lHeader encT a.1.1 a.1.2 a.2 then some (padOrTruncatePlain ℓ m) else none2 declarations not shown (lines 109–123): theorems, which Lean checks, or definitions that no headline statement uses
CryptoGames., CryptoGames.
def lChainPRG
The chain PRG: ck ↦ (HMAC(ck, 0x02), HMAC(ck, 0x01)) (next chain key, message-key seed). The SPQR salt enters only in lAead (unlike Ratchet.).
DEV-LS14 (libsignal): message keys from a chain step and a salted HKDF. ACD19 Fig. 6 uses one PRG G : W → W × K. libsignal's chain step yields the next chain key and a 32-byte seed, and the AEAD key is HKDF(salt, seed, "WhisperMessageKeys", 80) (AES key, MAC key, IV), computed per message inside lAead. The IV is derived, not random. Effect: none (one-time keys).
def lChainPRG (F : ShaState → List (BitVec 8) → ShaState) (_p : ℕ) :
PRGScheme (BitVec 256) (BitVec 256 × BitVec 256) :=
⟨fun ck => ((hmacPRF F).tag ck chainKeySeed, (hmacPRF F).tag ck messageKeySeed)⟩5 declarations not shown (lines 136–171): theorems, which Lean checks, or definitions that no headline statement uses
CryptoGames., CryptoGames., CryptoGames., CryptoGames., CryptoGames.
def ratchetKeyAdmissible
The wire's ratchet key is the encoding of a group element and a parseable wire has fewer than 2³² bytes (or the wire does not parse): the admissibility predicate of injections in the libsignal game.
DEV-LS5 (libsignal): only injections with on-curve ratchet keys and < 2³²-byte parseable wires. ACD19 Fig. 2 accepts any injected ciphertext. libsignal accepts any 32 bytes as a public key (twist points, mixed-order and non-canonical encodings), which the Fig. 8 instance cannot express, since its CKA messages are group elements. So the game refuses an injection whose ratchet key is not encT of a group element, or whose parseable wire has 2³² or more bytes (already excluded by shortCiphertext in the binary harness bhInjOK). Effect: restricts the adversary.
def ratchetKeyAdmissible {Pt : Type} (codec : SignalMessageProtoCodec) (decT : PublicKey → Option Pt) (encT : Pt → PublicKey)
[DecidableEq PublicKey] (w : List (BitVec 8)) : Bool :=
if w.length < 9 then true else
match (signalWireCodec codec).parse (w.take (w.length - 8)) with
| none => true
| some (h, _) =>
decide (w.length < 2 ^ 32) &&
match decT h.senderRatchetKey with
| some T => decide (encT T = h.senderRatchetKey)
| none => falsedef configR1OnCurve
The libsignal game: configR1 (ACD19 App. A's H1 with DEV-LS1–DEV-LS4 and DEV-LS6) with injections restricted to on-curve ratchet keys (DEV-LS5).
DEV-LS7 (formalization): rules inherited from the generic restricted game. The restricted game of SM/ keeps the generic game's own deviations from ACD19 Fig. 2 (the DEV-SM entries): corr-P also waits until no uncompromised record of the other party is in transit, the epoch cap qep, and tL only grows. The Fig. 8 side runs with epoch cap qep + 1, because a window reduction's hidden transmit can open one more epoch. Effect: restricts the adversary.
def configR1OnCurve {St Msg : Type} (onImage : List (BitVec 8) → Bool) : SM.ConfigR St Msg (List (BitVec 8)) :=
{ SM.configR1 with injOK := onImage }def lSaltPRF32
The salt PRF: seed ↦ 32-byte salt ↦ message keys, deriveMessageKeys F (some salt) seed (HKDF-Extract keyed by the seed in its message slot, then Expand). Its value at s is exactly the key lAead uses for a ciphertext carrying s.
DEV-LS25 (libsignal): one seed, several salts. In ACD19 Fig. 6 each message key is used once. libsignal takes the salt from the unauthenticated SPQR message before it checks the MAC, so an active adversary can make the receiver expand one seed under several salts. The proof treats seed ↦ salt ↦ keys as a PRF over 32-byte salts (the dual-PRF use of HMAC, BBGS'23 Thm 11 with S = {0,1}^256), bounds non-challenge-salt decryptions by macForgeryTerm before the wire reduction, and reduces the challenge salt (j = 0) to lWire. Effect: constants (a salt-PRF term per slot).
def lSaltPRF32 (F : ShaState → List (BitVec 8) → ShaState) : MACScheme (BitVec 256) Salt32 DerivedMessageKeys :=
⟨fun seed salt => deriveMessageKeys F (some salt) (keyToBytes32 seed)⟩2 declarations not shown (lines 219–255): theorems, which Lean checks, or definitions that no headline statement uses
CryptoGames., CryptoGames.
abbrev LibsignalWireOracleSpec
The oracle interface of the wire AEAD's game for the instance (header SignalHeader).
abbrev LibsignalWireOracleSpec (ℓ : ℕ) :=
unifSpec + WireAEAD.wireSpec SerializedIdentityKeys SignalHeader (Plain ℓ) (List (BitVec 8)) (BitVec 64)1 declaration not shown (lines 261–309): theorems, which Lean checks, or definitions that no headline statement uses
CryptoGames.
def macForgeryProb
Worst-case probability over identity keys, < 2³²-byte serialized messages, and 8-byte tags that a fixed wire (ser, tag) verifies under uniform DerivedMessageKeys (bounded in length to avoid Borel–Cantelli vacuity; reflects pointwise key-regularity of F in hmacWith F).
DEV-LS23 (libsignal): the 8-byte MAC tag and the forgery term. libsignal truncates the HMAC tag to 8 bytes (≥ 2⁻⁶⁴ forgery probability), so macForgeryProb enters fsShortBound as a bounded-length non-uniform supremum over concrete tests of F (DEV-LS31).
noncomputable def macForgeryProb (F : ShaState → List (BitVec 8) → ShaState) : ℝ≥0∞ :=
⨆ (ids : SerializedIdentityKeys) (ser : List (BitVec 8)) (_ : ser.length < 2 ^ 32)
(tag : BitVec 64),
𝒟[(do let mk ← ($ᵗ DerivedMessageKeys : ProbComp DerivedMessageKeys)
return ((hmacScheme F).tag mk.2 (ids.toList ++ ser) == tag) : ProbComp Bool)] {true}def vec32
A byte list as a 32-byte vector (zero-padded / truncated; identity on 32-byte lists).
def vec32 (bs : List (BitVec 8)) : List.Vector (BitVec 8) 32 :=
⟨(bs ++ List.replicate 32 0).take 32, bs:List (BitVec 8)⊢ (List.take 32 (bs ++ List.replicate 32 0)).length = 32 All goals completed! 🐙⟩7 declarations not shown (lines 328–421): theorems, which Lean checks, or definitions that no headline statement uses
CryptoGames., CryptoGames., CryptoGames., CryptoGames., CryptoGames., CryptoGames., CryptoGames., CryptoGames., CryptoGames.
def X25519RealizesDh
The byte-level X25519 of the model realizes the abstract DH function Dh (CKA. for the list lifts of C., C.), and encT is the public key of encPt.
DEV-LS29 (formalization): an abstract DH group. ACD19 §4.1.2's CKA is over a prime-order group with DDH. The CKA and PRF-PRNG terms of the theorem are over an abstract Dh : DHFun (BitVec 256) Pt, tied to the model's byte-level X25519 by this hypothesis; clamping and x-only points are absorbed into the DDH assumption for the X25519 function as used. Effect: none (nothing here is a proof about real Curve25519).
end LibsignalInstend Ratchetend CryptoGames