Adaptive oracle adversaries

An adaptive oracle adversary is a finite interaction tree: at each node it returns a value, flips coins from a probability mass function, or asks a query d : D and continues with the answer r : R. The query bound OracleAdv.IsQueryBound A q states that every path of A asks at most q queries. An adversary runs against a stateful oracle O : S → D → PMF (R × S), which returns the answer and the next oracle state.

Main definitions

• OracleAdv D R α — adaptive adversary with queries in D, answers in R, output in α
• OracleAdv.IsQueryBound A q — every path of A asks at most q queries
• OracleAdv.run O A s — joint distribution of the output and the final oracle state when A runs against O from state s

Main results

• OracleAdv.IsQueryBound.mono — query bounds are monotone
• OracleAdv.run_map_state — an oracle state map that commutes with one oracle call commutes with a whole run
• OracleAdv.run_map_fst_of_isQueryBound_zero — an adversary without queries has an output distribution independent of the oracle
• OracleAdv.run_flag_apply_false_of_true — an oracle whose flag is sticky keeps it set through a run
• OracleAdv.run_apply_flag_false_eq — two oracles that agree on every unflagged transition give runs that agree on every unflagged outcome (identical until bad)

inductive CatCrypt.Crypto.OracleAdv (D R α : Type) : Type 1

An adaptive oracle adversary with queries in D, answers in R and output in α: return a value (ret), sample b from a probability mass function and continue (rand), or query the oracle at d and continue with the answer (query).

• ret {D R α : Type} : α → OracleAdv D R α

  Return the output.

• rand {D R α β : Type} (p : PMF β) (k : β → OracleAdv D R α) : OracleAdv D R α

  Sample from p and continue with the sample.

• query {D R α : Type} (d : D) (k : R → OracleAdv D R α) : OracleAdv D R α

  Query the oracle at d and continue with the answer.

def CatCrypt.Crypto.OracleAdv.IsQueryBound {D R α : Type} : OracleAdv D R α → ℕ → Prop

IsQueryBound A q: every path of A asks at most q oracle queries.

Equations

• (CatCrypt.Crypto.OracleAdv.ret a).IsQueryBound x✝ = True
• (CatCrypt.Crypto.OracleAdv.rand p k).IsQueryBound x✝ = ∀ (b : β), (k b).IsQueryBound x✝
• (CatCrypt.Crypto.OracleAdv.query d k).IsQueryBound 0 = False
• (CatCrypt.Crypto.OracleAdv.query d k).IsQueryBound n.succ = ∀ (r : R), (k r).IsQueryBound n

theorem CatCrypt.Crypto.OracleAdv.IsQueryBound.mono {D R α : Type} {A : OracleAdv D R α} {m n : ℕ} (h : A.IsQueryBound m) (hmn : m ≤ n) : A.IsQueryBound n

noncomputable def CatCrypt.Crypto.OracleAdv.run {D R α S : Type} (O : S → D → PMF (R × S)) : OracleAdv D R α → S → PMF (α × S)

The joint distribution of the output and the final oracle state when A runs against the stateful oracle O from state s.

Equations

• CatCrypt.Crypto.OracleAdv.run O (CatCrypt.Crypto.OracleAdv.ret a) x✝ = PMF.pure (a, x✝)
• CatCrypt.Crypto.OracleAdv.run O (CatCrypt.Crypto.OracleAdv.rand p k) x✝ = p.bind fun (b : β) => CatCrypt.Crypto.OracleAdv.run O (k b) x✝
• CatCrypt.Crypto.OracleAdv.run O (CatCrypt.Crypto.OracleAdv.query d k) x✝ = (O x✝ d).bind fun (x : R × S) => CatCrypt.Crypto.OracleAdv.run O (k x.1) x.2

@[simp]

theorem CatCrypt.Crypto.OracleAdv.run_ret {D R α S : Type} (O : S → D → PMF (R × S)) (a : α) (s : S) : run O (ret a) s = PMF.pure (a, s)

@[simp]

theorem CatCrypt.Crypto.OracleAdv.run_rand {D R α S : Type} (O : S → D → PMF (R × S)) {β : Type} (p : PMF β) (k : β → OracleAdv D R α) (s : S) : run O (rand p k) s = p.bind fun (b : β) => run O (k b) s

@[simp]

theorem CatCrypt.Crypto.OracleAdv.run_query {D R α S : Type} (O : S → D → PMF (R × S)) (d : D) (k : R → OracleAdv D R α) (s : S) : run O (query d k) s = (O s d).bind fun (x : R × S) => run O (k x.1) x.2

theorem CatCrypt.Crypto.OracleAdv.run_map_state {D R α S S' : Type} (O : S → D → PMF (R × S)) (O' : S' → D → PMF (R × S')) (f : S → S') (hO : ∀ (s : S) (d : D), PMF.map (Prod.map id f) (O s d) = O' (f s) d) (A : OracleAdv D R α) (s : S) : PMF.map (Prod.map id f) (run O A s) = run O' A (f s)

A map f of oracle states that commutes with every oracle call commutes with every run.

theorem CatCrypt.Crypto.OracleAdv.run_map_fst_of_isQueryBound_zero {D R α S S' : Type} (O : S → D → PMF (R × S)) (O' : S' → D → PMF (R × S')) {A : OracleAdv D R α} (hA : A.IsQueryBound 0) (s : S) (s' : S') : PMF.map Prod.fst (run O A s) = PMF.map Prod.fst (run O' A s')

Without queries, the output distribution does not depend on the oracle or its initial state.

Flagged oracle state

theorem CatCrypt.Crypto.OracleAdv.run_flag_apply_false_of_true {D R α σ : Type} (O : σ × Bool → D → PMF (R × σ × Bool)) (hO : ∀ (t : σ) (d : D) (r : R) (t' : σ), (O (t, true) d) (r, t', false) = 0) (A : OracleAdv D R α) (t : σ) (a : α) (t' : σ) : (run O A (t, true)) (a, t', false) = 0

If an oracle never clears its flag, a run started with the flag set assigns probability zero to every outcome with the flag cleared.

theorem CatCrypt.Crypto.OracleAdv.run_apply_flag_false_eq {D R α σ : Type} (O₁ O₂ : σ × Bool → D → PMF (R × σ × Bool)) (h₁ : ∀ (t : σ) (d : D) (r : R) (t' : σ), (O₁ (t, true) d) (r, t', false) = 0) (h₂ : ∀ (t : σ) (d : D) (r : R) (t' : σ), (O₂ (t, true) d) (r, t', false) = 0) (hagree : ∀ (s : σ × Bool) (d : D) (r : R) (t' : σ), (O₁ s d) (r, t', false) = (O₂ s d) (r, t', false)) (A : OracleAdv D R α) (s : σ × Bool) (a : α) (t' : σ) : (run O₁ A s) (a, t', false) = (run O₂ A s) (a, t', false)

Identical until bad. Two oracles on flagged states whose flags are sticky and which agree on every transition into an unflagged state give runs that agree on every unflagged outcome.