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.

Main results

• Cslib.OracleComp.IdenticalUntilBad.advantage_le: the advantage of an identical-until-bad hop.

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.