Game hops that are identical until bad

Two games that run one program against stateful handlers that agree until a bad state, followed by the same final step, have advantage at most the probability of reaching a bad state (OracleComp.IdenticalUntilBad.advantage_le, [BS23], Theorem 4.7). This is the two-sided difference lemma OracleComp.IdenticalUntilBad.abs_sub_le in the form that composes with Game.advantage_triangle.

When a WordOracleComp Unit program interacts with a secret-dependent stateless deterministic oracle o₁ τ whose replies agree with a secret-independent clean oracle o₂ unless a per-query bad predicate isBad τ req holds (with secret-dependent continuation next τ), Game.runStatelessOracle_bind_le and Game.advantage_runStatelessOracle_bind_le bound the resulting μ.bind acceptance-probability difference and Game.advantage by Q * δ (respectively Q / q when each query hits a bad secret with probability at most q⁻¹).

Main definitions

• Cslib.Crypto.Game.runStatelessOracle: run a WordOracleComp Unit α against a stateless deterministic word oracle o : List Bool → List Bool and feed its output to next : α → Game.
• Cslib.Crypto.Game.finderPhase2Oracle, Cslib.Crypto.Game.runFinderOracle: stateful witness finder oracle handler that answers with o₂ while recording some (extract req) whenever isBad req holds.

Main results

• Cslib.OracleComp.IdenticalUntilBad.advantage_le: the advantage of an identical-until-bad hop.
• Cslib.Crypto.Game.runStatelessOracle_pure, Cslib.Crypto.Game.runStatelessOracle_query_inl, Cslib.Crypto.Game.runStatelessOracle_query_inr, Cslib.Crypto.Game.bind_runStatelessOracle_comm, Cslib.Crypto.Game.advantage_runStatelessOracle_le_of_support: structural and mixture laws for runStatelessOracle.
• Cslib.Crypto.Game.runStatelessOracle_bind_le, Cslib.Crypto.Game.advantage_runStatelessOracle_bind_le: stateless-oracle until-bad bounds with a secret-dependent continuation and a secret-independent clean oracle.
• Cslib.Crypto.Game.runStatelessOracle_le_runFinderOracle: stateless-oracle until-bad bound into a witness-finding game (runFinderOracle).
• Cslib.Crypto.Game.advantage_uniform_bind_of_eq_of_ne: single-exceptional-point advantage bound 1 / q for two ZMod q-indexed game families.

References

• D. Boneh, V. Shoup, A Graduate Course in Applied Cryptography, Version 0.6, Theorem 4.7.

theorem Cslib.OracleComp.IdenticalUntilBad.advantage_le {ι σ α : Type} {spec : ι → Type} {first second : (q : ι) → StateT σ PMF (spec q)} {bad : σ → Prop} (h : IdenticalUntilBad first second bad) (program : OracleComp spec α) (s : σ) (next : α × σ → Crypto.Game) : ↑(Crypto.Game.advantage (((interpret first program).run s).bind next) (((interpret second program).run s).bind next)) ≤ (((interpret first program).run s).toOuterMeasure {x : α × σ | bad x.2}).toReal

The difference lemma ([BS23], Theorem 4.7): games that run a program against handlers agreeing until a bad state, followed by the same final step, have advantage at most the probability of reaching a bad state.

noncomputable def Cslib.Crypto.Game.runStatelessOracle {α : Type} (o : List Bool → List Bool) (prog : Probability.WordOracleComp Unit α) (next : α → Game) : Game

Run a WordOracleComp Unit α against a stateless deterministic oracle o : List Bool → List Bool and feed its output to next : α → Game.

@[simp]

theorem Cslib.Crypto.Game.runStatelessOracle_pure {α : Type} (o : List Bool → List Bool) (a : α) (next : α → Game) : runStatelessOracle o (pure a) next = next a

theorem Cslib.Crypto.Game.runStatelessOracle_query_inl {α : Type} (o : List Bool → List Bool) (m : ℕ) (k : probOracleSpec (fun (x : Unit × List Bool) => List Bool) (Sum.inl m) → OracleComp (probOracleSpec fun (x : Unit × List Bool) => List Bool) α) (next : α → Game) : runStatelessOracle o (OracleComp.query (Sum.inl m) >>= k) next = (Probability.PMF.uniformOfFintype (Fin (m + 1))).bind fun (x : Fin (m + 1)) => runStatelessOracle o (k x) next

theorem Cslib.Crypto.Game.runStatelessOracle_query_inr {α : Type} (o : List Bool → List Bool) (req : Unit × List Bool) (k : probOracleSpec (fun (x : Unit × List Bool) => List Bool) (Sum.inr req) → OracleComp (probOracleSpec fun (x : Unit × List Bool) => List Bool) α) (next : α → Game) : runStatelessOracle o (OracleComp.query (Sum.inr req) >>= k) next = runStatelessOracle o (k (o req.2)) next

theorem Cslib.Crypto.Game.runStatelessOracle_bind_le {T α : Type} (μ : PMF T) (o₁ : T → List Bool → List Bool) (o₂ : List Bool → List Bool) (isBad : T → List Bool → Bool) (next : T → α → Game) {Q : ℕ} {δ : ENNReal} {prog : Probability.WordOracleComp Unit α} (hq : ProbOracleComp.IsQueryBounded prog Q) (hagree : ∀ (τ : T) (req : List Bool), isBad τ req = false → o₁ τ req = o₂ req) (hbad : ∀ (req : List Bool), (∑' (τ : T), μ τ * if isBad τ req = true then 1 else 0) ≤ δ) (b : Bool) : (μ.bind fun (τ : T) => runStatelessOracle (o₁ τ) prog (next τ)) b ≤ (μ.bind fun (τ : T) => runStatelessOracle o₂ prog (next τ)) b + ↑Q * δ ∧ (μ.bind fun (τ : T) => runStatelessOracle o₂ prog (next τ)) b ≤ (μ.bind fun (τ : T) => runStatelessOracle (o₁ τ) prog (next τ)) b + ↑Q * δ

Stateless oracle until-bad bound: if prog makes at most Q oracle queries, o₁ τ req agrees with o₂ req whenever isBad τ req = false, and for every req the μ-probability of isBad τ req = true is at most δ, then replacing o₁ τ by o₂ (with continuation next τ) changes the probability of each outcome b : Bool by at most Q * δ.

theorem Cslib.Crypto.Game.advantage_runStatelessOracle_bind_le {T α : Type} (μ : PMF T) (o₁ : T → List Bool → List Bool) (o₂ : List Bool → List Bool) (isBad : T → List Bool → Bool) (next : T → α → Game) {Q q : ℕ} [NeZero q] {prog : Probability.WordOracleComp Unit α} (hq : ProbOracleComp.IsQueryBounded prog Q) (hagree : ∀ (τ : T) (req : List Bool), isBad τ req = false → o₁ τ req = o₂ req) (hbad : ∀ (req : List Bool), (∑' (τ : T), μ τ * if isBad τ req = true then 1 else 0) ≤ (↑q)⁻¹) : advantage (μ.bind fun (τ : T) => runStatelessOracle (o₁ τ) prog (next τ)) (μ.bind fun (τ : T) => runStatelessOracle o₂ prog (next τ)) ≤ ↑Q / ↑q

Game.advantage corollary of runStatelessOracle_bind_le when δ = (q : ℝ≥0∞)⁻¹.

theorem Cslib.Crypto.Game.bind_runStatelessOracle_comm {α β : Type} (μ : PMF β) (o : List Bool → List Bool) (prog : Probability.WordOracleComp Unit α) (next : β → α → Game) : (μ.bind fun (b : β) => runStatelessOracle o prog (next b)) = runStatelessOracle o prog fun (a : α) => μ.bind fun (b : β) => next b a

An independent outer PMF.bind commutes with runStatelessOracle.

theorem Cslib.Crypto.Game.advantage_runStatelessOracle_le_of_support {α : Type} (o : List Bool → List Bool) (prog : Probability.WordOracleComp Unit α) (next₁ next₂ : α → Game) {ε : NNReal} (h : ∀ out ∈ ((OracleComp.interpret (ProbOracleComp.handler (fun (m : ℕ) => StateT.lift (ProbComp.unifFin m)) fun (req : Unit × List Bool) (s : Unit) => pure (o req.2, s)) prog).run ()).eval.support, (next₁ out.1).advantage (next₂ out.1) ≤ ε) : (runStatelessOracle o prog next₁).advantage (runStatelessOracle o prog next₂) ≤ ε

Support-restricted continuation bound for runStatelessOracle.

theorem Cslib.Crypto.Game.advantage_uniform_bind_of_eq_of_ne {q : ℕ} [NeZero q] (x₀ : ZMod q) (g₁ g₂ : ZMod q → Game) (heq : ∀ (x : ZMod q), x ≠ x₀ → g₁ x = g₂ x) : advantage ((Probability.PMF.uniformOfFintype (ZMod q)).bind g₁) ((Probability.PMF.uniformOfFintype (ZMod q)).bind g₂) ≤ 1 / ↑q

Two ZMod q-indexed game families that agree outside a single point x₀ have Game.advantage at most 1 / q under PMF.uniformOfFintype (ZMod q).

def Cslib.Crypto.Game.finderPhase2Oracle (o₂ : List Bool → List Bool) (isBad : List Bool → Bool) (extract : List Bool → List Bool) (request : Unit × List Bool) : StateT (Option (List Bool)) ProbComp (List Bool)

Stateful oracle handler that replies with o₂ request.2 and updates its Option (List Bool) state to some (extract request.2) whenever isBad request.2 holds.

noncomputable def Cslib.Crypto.Game.runFinderOracle {α : Type} (o₂ : List Bool → List Bool) (isBad : List Bool → Bool) (extract : List Bool → List Bool) (prog : Probability.WordOracleComp Unit α) (s : Option (List Bool)) (isGood : List Bool → Bool) : Game

Run prog against finderPhase2Oracle starting from s : Option (List Bool) and test whether the final state satisfies isGood.

@[simp]

theorem Cslib.Crypto.Game.runFinderOracle_pure {α : Type} (o₂ : List Bool → List Bool) (isBad : List Bool → Bool) (extract : List Bool → List Bool) (a : α) (s : Option (List Bool)) (isGood : List Bool → Bool) : runFinderOracle o₂ isBad extract (pure a) s isGood = PMF.pure (s.elim false isGood)

theorem Cslib.Crypto.Game.runFinderOracle_query_inl {α : Type} (o₂ : List Bool → List Bool) (isBad : List Bool → Bool) (extract : List Bool → List Bool) (m : ℕ) (k : probOracleSpec (fun (x : Unit × List Bool) => List Bool) (Sum.inl m) → OracleComp (probOracleSpec fun (x : Unit × List Bool) => List Bool) α) (s : Option (List Bool)) (isGood : List Bool → Bool) : runFinderOracle o₂ isBad extract (OracleComp.query (Sum.inl m) >>= k) s isGood = (Probability.PMF.uniformOfFintype (Fin (m + 1))).bind fun (x : Fin (m + 1)) => runFinderOracle o₂ isBad extract (k x) s isGood

theorem Cslib.Crypto.Game.runFinderOracle_query_inr {α : Type} (o₂ : List Bool → List Bool) (isBad : List Bool → Bool) (extract : List Bool → List Bool) (req : Unit × List Bool) (k : probOracleSpec (fun (x : Unit × List Bool) => List Bool) (Sum.inr req) → OracleComp (probOracleSpec fun (x : Unit × List Bool) => List Bool) α) (s : Option (List Bool)) (isGood : List Bool → Bool) : runFinderOracle o₂ isBad extract (OracleComp.query (Sum.inr req) >>= k) s isGood = runFinderOracle o₂ isBad extract (k (o₂ req.2)) (if isBad req.2 = true then some (extract req.2) else s) isGood

theorem Cslib.Crypto.Game.runFinderOracle_true_of_good {α : Type} (o₂ : List Bool → List Bool) (isBad : List Bool → Bool) (extract : List Bool → List Bool) (isGood : List Bool → Bool) (hbad_good : ∀ (req : List Bool), isBad req = true → isGood (extract req) = true) (prog : Probability.WordOracleComp Unit α) (s : Option (List Bool)) : s.elim false isGood = true → (runFinderOracle o₂ isBad extract prog s isGood) true = 1

Once s satisfies s.elim false isGood = true, runFinderOracle succeeds with probability 1.

theorem Cslib.Crypto.Game.runStatelessOracle_le_runFinderOracle {α : Type} (o₁ o₂ : List Bool → List Bool) (isBad : List Bool → Bool) (extract : List Bool → List Bool) (isGood : List Bool → Bool) (hagree : ∀ (req : List Bool), isBad req = false → o₁ req = o₂ req) (hbad_good : ∀ (req : List Bool), isBad req = true → isGood (extract req) = true) (prog : Probability.WordOracleComp Unit α) (next : α → Game) (b : Bool) : (runStatelessOracle o₁ prog next) b ≤ (runStatelessOracle o₂ prog next) b + (runFinderOracle o₂ isBad extract prog none isGood) true ∧ (runStatelessOracle o₂ prog next) b ≤ (runStatelessOracle o₁ prog next) b + (runFinderOracle o₂ isBad extract prog none isGood) true

Finder-oracle until-bad bound: if o₁ req = o₂ req whenever isBad req = false and every query with isBad req = true satisfies isGood (extract req) = true, then the difference between runStatelessOracle o₁ prog next and runStatelessOracle o₂ prog next is bounded by the probability that runFinderOracle o₂ isBad extract prog none isGood outputs true.