LibsignalSim.lean🔗

Tier 2 · definitions used by the computational proof 1 headline theorem depend on it 88 of 162 lines trusted trust banner B3, trusted in part 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 (10)

Shared types and error terms for the libsignal-to-Double-Ratchet refinement

Trusted in part. The theorems of Computational/Theorems/ use every definition in this file except Fig8Comp, tagBytes and toWire, which are checked by Lean; the ones they use are part of what you must read to trust the result. See Computational/docs/TRUSTED_BASE.md. epoch0Term, GhostChain, configEpoch0Distinguisher, epoch0Distinguisher, and the refinement theorems are in Computational/Proofs/SpecLemmas/Session/ACD19/Ratchet/LibsignalSim.lean, checked by Lean.

A simulator sim playing the secure-messaging game of ACD19 (Alwen, Coretti, Dodis, The Double Ratchet, ePrint 2018/1037) against the Fig. 8 Double Ratchet instance lFig8 (messages LibsignalMsgPublicPart × Plain ℓ, healing constant Δ_SM = 3; DEV-LS32) reproduces the restricted libsignal session game configR1OnCurve on libsignalSessionScheme (LibsignalBinary/Specifications/CryptoGames/SM/LibsignalGame.lean; DEV-LS1 to DEV-LS7, with SPQR fields per DEV-LS24) up to the spurious-step error terms defined here.

The per-test regularity units rootKdfSpuriousStepUnit and rootKdfForgedEpochStartUnit are named, non-standard trust assumptions (HKDF/HMAC-SHA256 as a statistical extractor under a worst-case public salt on correlated clamped-X25519 inputs), justified only in the random-oracle model.

@[expose] public section

open OracleComp OracleSpec ENNReal

namespace CryptoGames

namespace Ratchet

namespace LibsignalSim

open HMAC HKDF CBC LibsignalAead SM SM.Construction CKA LibsignalSession LibsignalInst

1 declaration not shown (lines 45–48): theorems, which Lean checks, or definitions that no headline statement uses

CryptoGames.Ratchet.LibsignalSim.tagBytes

abbrev Fig8StL50–54 ↗#

Party state of the Fig. 8 instance lFig8.

abbrev Fig8St (Pt : Type) :=
  PartyState (CKA.DDH.State (BitVec 256) Pt) Pt Ratchet.RootKey
    (FSAEAD.RatchetSenderState (BitVec 256))
    (FSAEAD.RatchetReceiverState (BitVec 256) (BitVec 256))

abbrev Fig8CL56–57 ↗#

Ciphertext (header, (counter, wireCtWithSalt)) of lFig8.

abbrev Fig8C (Pt : Type) := Header Pt × (ℕ × LibsignalCiphertextWithSalt32)

1 declaration not shown (lines 59–60): theorems, which Lean checks, or definitions that no headline statement uses

CryptoGames.Ratchet.LibsignalSim.Fig8Comp

variable {Pt : Type} [DecidableEq Pt] [Zero Pt]

1 declaration not shown (lines 64–65): theorems, which Lean checks, or definitions that no headline statement uses

CryptoGames.Ratchet.LibsignalSim.toWire

Spurious-step error terms

def evictedKeySpuriousStepPrgL69–76 ↗#

Spurious DH step of P on an evicted honest ratchet key T_old = dh y base, viewed as a PRG in P's sending secret x: the eager step σ = (rootKdf rk (encPt (dh x curCkaMsg))).1 followed by the receiving half-step rootKdf σ (encPt (dh x T_old)).

def evictedKeySpuriousStepPrg (F : ShaState → List (BitVec 8) → ShaState) (encPt : Pt → List (BitVec 8))
    (Dh : DHFun (BitVec 256) Pt) (rk : Ratchet.RootKey) (curCkaMsg : Pt) (y : BitVec 256) :
    PRGScheme (BitVec 256) (Ratchet.RootKey × BitVec 256) :=
  ⟨fun x =>
    rootKdf F (rootKdf F rk (encPt (Dh.dh x curCkaMsg))).1 (encPt (Dh.dh x (Dh.dh y Dh.base)))⟩

def wireMacVerifiesTestL78–86 ↗#

Fixed test checking whether wire (ser, tag) verifies at chain counter c (with salt and identity keys ids) on the chain initialized from rk.2.

def wireMacVerifiesTest (F : ShaState → List (BitVec 8) → ShaState) (c : ℕ) (salt : Salt) (ids : SerializedIdentityKeys)
    (ser : List (BitVec 8)) (tag : BitVec 64) :
    PRGScheme.PRGAdversary (Ratchet.RootKey × BitVec 256) :=
  fun rk =>
    let ck := (List.range c).foldl (fun k _ => (hmacPRF F).tag k chainKeySeed) rk.2
    let mk := deriveMessageKeys F salt (chainHmac F ck messageKeySeed)
    return ((hmacScheme F).tag mk.2 (ids.toList ++ ser) == tag)

def rootKdfSpuriousStepUnitL88–105 ↗#

Worst-case root-KDF regularity unit for a spurious DH step on an evicted honest epoch: the supremum over public root key rk, current CKA message curCkaMsg, honest ratchet secret y, and fixed MAC test wireMacVerifiesTest F c salt ids ser tag (c < 2 ^ 32, ser.length < 2 ^ 32, as in macForgeryProb; DEV-LS23) of the PRG advantage of evictedKeySpuriousStepPrg in x plus the ideal acceptance probability of that test.

Smallness of this unit is a non-standard trust assumption justified only in the random-oracle model (not implied by HMAC PRF security, rootPRNG, or DDH): HKDF-SHA256 must extract under a worst-case public salt rk from the x-correlated clamped-X25519 secrets dh x curCkaMsg and dh x (dh y base) across a key-dependent second step. The 2 ^ 32 caps prevent the unbounded supremum over c and ser from reaching 1.

noncomputable def rootKdfSpuriousStepUnit (F : ShaState → List (BitVec 8) → ShaState)
    (encPt : Pt → List (BitVec 8)) (Dh : DHFun (BitVec 256) Pt) : ℝ≥0∞ :=
  ⨆ (rk : Ratchet.RootKey) (curCkaMsg : Pt) (y : BitVec 256) (c : ℕ) (_ : c < 2 ^ 32)
    (salt : Salt) (ids : SerializedIdentityKeys) (ser : List (BitVec 8)) (_ : ser.length < 2 ^ 32)
    (tag : BitVec 64),
    ((evictedKeySpuriousStepPrg F encPt Dh rk curCkaMsg y).prgAdvantage (wireMacVerifiesTest F c salt ids ser tag) +
      𝒟[PRGScheme.prgIdealExperiment (wireMacVerifiesTest F c salt ids ser tag)] {true})

def spuriousStepTermL107–117 ↗#

Spurious-step error bound (q * qep) * rootKdfSpuriousStepUnit F encPt Dh over at most q * qep (wire, eager key) pairs.

DEV-LS11 (libsignal): spurious DH steps on honest messages of evicted epochs. ACD19 Fig. 8 accepts honest messages from any old epoch, whereas libsignal evicts old chains and runs a fresh DH step on the old ratchet key whose MAC check fails with high probability. sim returns rejected; this term bounds the probability that libsignal accepts instead over c < 2 ^ 32 and ser.length < 2 ^ 32 (DEV-LS23).

noncomputable def spuriousStepTerm (F : ShaState → List (BitVec 8) → ShaState)
    (encPt : Pt → List (BitVec 8)) (Dh : DHFun (BitVec 256) Pt) (q qep : ℕ) : ℝ≥0∞ :=
  (q * qep : ℕ) * rootKdfSpuriousStepUnit F encPt Dh

def pointSpuriousStepPrgL119–124 ↗#

Point-generalized spurious DH step of P on an on-curve ratchet point T : Pt, viewed as a PRG in P's sending secret x (evictedKeySpuriousStepPrg is the case T = Dh.dh y Dh.base).

def pointSpuriousStepPrg (F : ShaState → List (BitVec 8) → ShaState) (encPt : Pt → List (BitVec 8))
    (Dh : DHFun (BitVec 256) Pt) (rk : Ratchet.RootKey) (curCkaMsg T : Pt) :
    PRGScheme (BitVec 256) (Ratchet.RootKey × BitVec 256) :=
  ⟨fun x => rootKdf F (rootKdf F rk (encPt (Dh.dh x curCkaMsg))).1 (encPt (Dh.dh x T))⟩

def rootKdfForgedEpochStartUnitL126–138 ↗#

Worst-case root-KDF regularity unit for a forged epoch start: as in rootKdfSpuriousStepUnit, taking the supremum over public root key rk, non-zero points curCkaMsg, T : {P : Pt // P ≠ 0} (calculate_agreement rejects 0), and wireMacVerifiesTest with c < 2 ^ 32 and ser.length < 2 ^ 32 of the PRG advantage of pointSpuriousStepPrg plus the ideal test probability. Smallness is a random-oracle-only statistical-extractor assumption on HKDF-SHA256 for adversary-chosen T ≠ 0.

noncomputable def rootKdfForgedEpochStartUnit (F : ShaState → List (BitVec 8) → ShaState)
    (encPt : Pt → List (BitVec 8)) (Dh : DHFun (BitVec 256) Pt) : ℝ≥0∞ :=
  ⨆ (rk : Ratchet.RootKey) (curCkaMsg : {P : Pt // P ≠ 0})
    (T : {P : Pt // P ≠ 0}) (c : ℕ) (_ : c < 2 ^ 32) (salt : Salt) (ids : SerializedIdentityKeys)
    (ser : List (BitVec 8)) (_ : ser.length < 2 ^ 32) (tag : BitVec 64),
    ((pointSpuriousStepPrg F encPt Dh rk curCkaMsg.1 T.1).prgAdvantage (wireMacVerifiesTest F c salt ids ser tag) +
      𝒟[PRGScheme.prgIdealExperiment (wireMacVerifiesTest F c salt ids ser tag)] {true})

def forgedEpochStartSpuriousStepTermL140–151 ↗#

Point-generalized spurious-step error bound q * rootKdfForgedEpochStartUnit F encPt Dh over at most q (wire, eager key) pairs.

DEV-LS12 (libsignal): libsignal accepts a forged epoch start inside the window. ACD19 Def. 7 (E) and Fig. 8 reject t > t_P + 1, whereas after an eager step (DEV-LS1) libsignal holds P's next sending key and accepts an unseen ratchet key at t_P + 2. sim rejects it; the session bound charges 2 * forgedEpochStartSpuriousStepTerm for an unknown ratchet key inside a window (between an accepted epoch start and P's next send) plus one extra fig8ShortBound copy (via Thm1.challSim) while Bob's signed pre-key chain is unknown.

noncomputable def forgedEpochStartSpuriousStepTerm (F : ShaState → List (BitVec 8) → ShaState)
    (encPt : Pt → List (BitVec 8)) (Dh : DHFun (BitVec 256) Pt) (q : ℕ) : ℝ≥0∞ :=
  (q : ℝ≥0∞) * rootKdfForgedEpochStartUnit F encPt Dh

Root-KDF PRG view

def rootKdfAsPrgL155–163 ↗#

Single root-KDF step on fixed input ikm, viewed as a PRG in the root key.

def rootKdfAsPrg (F : ShaState → List (BitVec 8) → ShaState) (ikm : List (BitVec 8)) :
    PRGScheme Ratchet.RootKey (Ratchet.RootKey × BitVec 256) :=
  ⟨fun σ => rootKdf F σ ikm⟩

end LibsignalSim

end Ratchet

end CryptoGames