Identical until bad

Two stateful oracle handlers are identical until bad when, from a good state, they give the same probability to every answer that leads to a good state, and bad states are absorbing in both. Then the two interpretations of any program give the same probability to every outcome with a good final state (IdenticalUntilBad.run_apply). Consequently, an experiment that continues the run accepts with the first handler at most as often as with the second, plus the probability of reaching a bad state ([BS23], Theorem 4.7, the difference lemma), with no bound on the program's number of calls (IdenticalUntilBad.bind_apply_le). Both handlers reach a bad state with the same probability (IdenticalUntilBad.bad_eq), so the two acceptance probabilities differ by at most that probability (IdenticalUntilBad.abs_sub_le), and the bad event may be bounded in whichever run is easier.

The probability of reaching a bad state is bounded by summing over the calls: if each call q from a good state turns bad with probability at most cost q · budget s, and each call raises the budget by at most δ, then a program making at most n calls, whose calls cost at most k, reaches a bad state with probability at most k · (budget s + n · δ) (toOuterMeasure_bad_le). This is the union bound for a growing collision set, such as a random oracle that is programmed, at some calls only, at points that may already be defined.

Main definitions

• Cslib.OracleComp.IdenticalUntilBad: two handlers that agree until a bad state.

Main results

• Cslib.OracleComp.IdenticalUntilBad.run_apply: equal outcome probabilities at good states.
• Cslib.OracleComp.IdenticalUntilBad.bind_apply_le: the difference lemma.
• Cslib.OracleComp.IdenticalUntilBad.bad_eq, Cslib.OracleComp.IdenticalUntilBad.abs_sub_le: the bad event has the same probability under both handlers, and the two-sided difference lemma.
• Cslib.OracleComp.toOuterMeasure_bad_le: the accumulated probability of a bad state.

References

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

structure Cslib.OracleComp.IdenticalUntilBad {ι σ : Type} {spec : ι → Type} (first second : (q : ι) → StateT σ PMF (spec q)) (bad : σ → Prop) : Prop

Two stateful handlers agree until a bad state: from a good state they give equal probability to every answer with a good next state, and bad states are absorbing for both.

• agree (q : ι) (s : σ) : ¬bad s → ∀ (a : spec q) (s' : σ), ¬bad s' → (first q s) (a, s') = (second q s) (a, s')

  From a good state, answers with good next states are equally likely.

• absorb_first (q : ι) (s : σ) : bad s → ∀ x ∈ (first q s).support, bad x.2

  Bad states are absorbing for the first handler.

• absorb_second (q : ι) (s : σ) : bad s → ∀ x ∈ (second q s).support, bad x.2

  Bad states are absorbing for the second handler.

theorem Cslib.OracleComp.bad_of_mem_support_run {ι σ α : Type} {spec : ι → Type} {handler : (q : ι) → StateT σ PMF (spec q)} {bad : σ → Prop} (habsorb : ∀ (q : ι) (s : σ), bad s → ∀ x ∈ (handler q s).support, bad x.2) (program : OracleComp spec α) {s : σ} (hs : bad s) (x : α × σ) : x ∈ ((interpret handler program).run s).support → bad x.2

A handler for which bad states are absorbing keeps every run from a bad state bad.

theorem Cslib.OracleComp.IdenticalUntilBad.run_apply {ι σ α : Type} {spec : ι → Type} {first second : (q : ι) → StateT σ PMF (spec q)} {bad : σ → Prop} (h : IdenticalUntilBad first second bad) (program : OracleComp spec α) (s : σ) (a : α) (s' : σ) (hs' : ¬bad s') : ((interpret first program).run s) (a, s') = ((interpret second program).run s) (a, s')

Handlers that agree until a bad state give the same probability to every outcome whose final state is good.

theorem Cslib.OracleComp.IdenticalUntilBad.bind_apply_le {ι σ α : Type} {spec : ι → Type} {first second : (q : ι) → StateT σ PMF (spec q)} {bad : σ → Prop} (h : IdenticalUntilBad first second bad) (program : OracleComp spec α) (s : σ) {β : Type} (next : α × σ → PMF β) (b : β) : (((interpret first program).run s).bind next) b ≤ (((interpret second program).run s).bind next) b + ((interpret first program).run s).toOuterMeasure {x : α × σ | bad x.2}

The difference lemma ([BS23], Theorem 4.7): any experiment continuing the run of a program accepts with the first handler at most as often as with the second, plus the probability of reaching a bad state with the first.

theorem Cslib.OracleComp.IdenticalUntilBad.symm {ι σ : Type} {spec : ι → Type} {first second : (q : ι) → StateT σ PMF (spec q)} {bad : σ → Prop} (h : IdenticalUntilBad first second bad) : IdenticalUntilBad second first bad

Identical until bad is symmetric.

theorem Cslib.OracleComp.IdenticalUntilBad.bad_eq {ι σ α : Type} {spec : ι → Type} {first second : (q : ι) → StateT σ PMF (spec q)} {bad : σ → Prop} (h : IdenticalUntilBad first second bad) (program : OracleComp spec α) (s : σ) : ((interpret first program).run s).toOuterMeasure {x : α × σ | bad x.2} = ((interpret second program).run s).toOuterMeasure {x : α × σ | bad x.2}

Handlers that agree until a bad state reach a bad state with the same probability.

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

The difference lemma, two-sided ([BS23], Theorem 4.7): any experiment continuing the run of a program accepts with probabilities, under the two handlers, that differ by at most the probability of reaching a bad state, which is the same under both.

theorem Cslib.OracleComp.toOuterMeasure_bad_le {ι σ α : Type} {spec : ι → Type} {handler : (q : ι) → StateT σ PMF (spec q)} {bad : σ → Prop} (cost : ι → ℕ) (budget : σ → ENNReal) (δ : ENNReal) (hstep : ∀ (q : ι) (s : σ), ¬bad s → (handler q s).toOuterMeasure {x : spec q × σ | bad x.2} ≤ ↑(cost q) * budget s) (hgrow : ∀ (q : ι) (s : σ), ¬bad s → ∀ x ∈ (handler q s).support, ¬bad x.2 → budget x.2 ≤ budget s + δ) {program : OracleComp spec α} {n k : ℕ} (hn : program.IsQueryBounded n) (hk : IsCostBounded cost program k) {s : σ} (hs : ¬bad s) : ((interpret handler program).run s).toOuterMeasure {x : α × σ | bad x.2} ≤ ↑k * (budget s + ↑n * δ)

The accumulated probability of a bad state. Let each call q from a good state turn bad with probability at most cost q · budget s, and raise the budget by at most δ. Then a program making at most n calls, whose calls cost at most k, reaches a bad state from a good state with probability at most k · (budget s + n · δ).