StatementPqReds.lean
End-to-end composition reduction bundles and per-session mixture bound
Trusted: definitions used by the statement. This file defines the multi-session composition ReductionDsl bundles and per-session mixture bound used by ModelSecure (Computational/) and CliPqxdhSecurityFor (Computational/). See Computational/.
A CompositionCostedReductions bundle reduces the multi-session game bhTargetGameSpec to one-key real-HKDF PQXDH key indistinguishability (kindRed) and to single-session ACD19 secure messaging (prefixRed k for session k), using operations from ReductionDsl. and coin-only randomness from ReductionDsl.. Composition bounds both uniform step cost (bhE2ECostBudget) and per-query-kind step cost (bhE2ECostBudgetByKind, separating online protocol queries from offline random-oracle queries via bhQueryKind). For each session k, bhPrefixFullBoundMixV1With combines the single-session bound uniformStartMixtureBound over the stage-1 identity/pre-key distribution with the PRF, PRG, forgery, collision, and scalar-guessing terms of the signed-pre-key hybrid hops.
@[expose] public sectionset_option autoImplicit falseopen OracleComp OracleSpec MeasureTheory ENNRealnamespace CryptoVerification.E2Eopen CryptoGames CryptoGames.LibsignalSM Ratchet LibsignalInst LibsignalSession
CryptoGames.LibsignalSessionApi HMAC HKDF CBC LibsignalAead SM SM.Construction CKA AEADScheme
MACScheme WireAEAD FSAEAD CryptoGames.Ratchet.LibsignalSim CryptoGames.FSAEAD.Thm5
CryptoVerification.LibsignalProtoCodec CryptoVerification.LibsignalSession
CryptoVerification.LibsignalSpqrV1def compositionLocalStart
Local startDR sid promotion step on BHE2EDrvState S ℓ against handshake oracle ki, used by the reference model game modelIface.
def compositionLocalStart {S : SignalPqxdh.Setup} {ℓ : ℕ}
(ki : QueryImpl (SignalPqxdh.keyIndSpec S) (StateT (SignalPqxdh.KeyIndState S) ProbComp))
(C : Crypto) (K : LibsignalSpqrV1.MlKem) (bMode? : Option Bool)
(σ : BHE2EDrvState S ℓ) (sid : SignalPqxdh.SessionId S) :
ProbComp (Option ℕ × BHE2EDrvState S ℓ) := do
match bhE2EGuard σ sid with
| none => return (none, σ)
| some (_, _, (u, j)) =>
let (kr1, st1) ← (ki (.testSession sid)).run σ.st
let (kr2, st2) ← (ki (.revealSpkSk u j)).run st1
let ac ← ($ᵗ BitVec 256 : ProbComp (BitVec 256))
return bhE2EFinishStartSpk C K bMode? { σ with st := st2 } sid kr1 kr2 acstructure CompositionCostedReductions
Multi-session composition ReductionDsl bundle: a one-stage reduction kindRed to one-key KeyInd and a family prefixRed k of two-stage reductions to single-session SM. with stage-1 context ReductionDsl..
structure CompositionCostedReductions (S : SignalPqxdh.Setup) {Pt : Type} (ℓ : ℕ)
(P : SignalPqxdh.Primitives) (C : Crypto) (K : LibsignalSpqrV1.MlKem) (qep : ℕ)
(decT : PublicKey → Option Pt) (encT : Pt → PublicKey) where
kindRed :
ReductionDsl.CostedReduction (ReductionDsl.atomicE2EOps ℓ P C K decT encT)
(ReductionDsl.e2eKeyIndTargetIface S ℓ Pt)
(bhTargetGameSpec S ℓ (BitVec 512)) (e2eTargetGameCodec S ℓ Pt)
.unit .unit .bool .bool
prefixRed : (k : ℕ) →
ReductionDsl.TwoStageCostedReduction (ReductionDsl.atomicE2EOps ℓ P C K decT encT)
(ReductionDsl.e2eSessionTargetIface ℓ Pt)
(bhTargetGameSpec S ℓ (BitVec 512)) (e2eTargetGameCodec S ℓ Pt)
.unit .unit .bool (ReductionDsl.prefixCtxT (ℓ := ℓ) (Pt := Pt)) .bool .bool
abbrev Composition
Family of CompositionCostedReductions indexed by handshake budget b and static loop bounds qStart, qDR, and qInst.
abbrev CompositionCostedReductionFamily (S : SignalPqxdh.Setup) {Pt : Type} (ℓ : ℕ)
(P : SignalPqxdh.Primitives) (C : Crypto) (K : LibsignalSpqrV1.MlKem) (qep : ℕ)
(decT : PublicKey → Option Pt) (encT : Pt → PublicKey) : Type :=
(b : SignalPqxdh.QueryBudget) → (qStart qDR qInst : ℕ) →
CompositionCostedReductions S ℓ P C K qep decT encT
def Composition
Boundedness predicate for R: enforces size, size-honesty, target-query (2 * qTot for kindRed, qTot for prefixRed k), and uniform step-cost bounds (GRedBounded, GRed2Bounded against bhE2ECostBudget), together with per-kind step-cost and query bounds (GRedCostByKind, GRed2CostByKind against bhE2ECostBudgetByKind under bhQueryKind and bhKindCounts). The per-kind conjuncts separate online protocol queries (kind 0) from offline .roQuery calls (kind 1) so offline hashes pay only random-oracle table lookup rather than online dispatch and session-table scans.
def CompositionCostedReductionsBounded {S : SignalPqxdh.Setup} {Pt : Type} {ℓ : ℕ}
(P : SignalPqxdh.Primitives) (C : Crypto) (K : LibsignalSpqrV1.MlKem) (qep : ℕ)
(decT : PublicKey → Option Pt) (encT : Pt → PublicKey)
(b : SignalPqxdh.QueryBudget) (qStart : ℕ) (qs : ℕ → ℕ)
(R : CompositionCostedReductions S ℓ P C K qep decT encT) : Prop :=
let qDR := ∑ k ∈ Finset.range qStart, qs k
let qInst := Finset.sup (Finset.range qStart) qs
let qTot := b.q_total + qStart + qDR
let B := bhE2ECostBudget S b qStart qDR qInst qep ℓ
let qKind := bhKindCounts b qStart qDR
let qSum := (List.ofFn qKind).sum
let Bk := bhE2ECostBudgetByKind S b qStart qDR qInst qep ℓ
(GRedBounded R.kindRed (fun _ => 1) (fun _ => 0) qTot (2 * qTot) B ∧
(∀ k < qStart,
GRed2Bounded (R.prefixRed k) (fun _ => 1) (fun _ => 0) qTot qTot B false)) ∧
(GRedCostByKind R.kindRed (fun _ => 1) (fun _ => 0) bhQueryKind qKind (2 * qSum) Bk ∧
(∀ k < qStart,
GRed2CostByKind (R.prefixRed k) (fun _ => 1) (fun _ => 0) bhQueryKind qKind qSum Bk))
def Composition
Uniform Composition compliance across all query budgets.
def CompositionCostedReductionFamilyBounded {S : SignalPqxdh.Setup} {Pt : Type} {ℓ : ℕ}
(P : SignalPqxdh.Primitives) (C : Crypto) (K : LibsignalSpqrV1.MlKem) (qep : ℕ)
(decT : PublicKey → Option Pt) (encT : Pt → PublicKey)
(reds : CompositionCostedReductionFamily S ℓ P C K qep decT encT) : Prop :=
∀ (b : SignalPqxdh.QueryBudget) (qStart : ℕ) (qs : ℕ → ℕ),
CompositionCostedReductionsBounded P C K qep decT encT b qStart qs
(reds b qStart (∑ k ∈ Finset.range qStart, qs k) (Finset.sup (Finset.range qStart) qs))1 declaration not shown (lines 122–157): theorems, which Lean checks, or definitions that no headline statement uses
CryptoVerification.
end CryptoVerification.E2E