Theory Unpredictable_Function

(* Title: Unpredictable_Function.thy
  Author: Andreas Lochbihler, ETH Zurich 
  Author: S. Reza Sefidgar, ETH Zurich *)

subsection ‹Unpredictable function›

theory Unpredictable_Function imports
  Guessing_Many_One
begin

locale upf =
  fixes key_gen :: "'key spmf"
  and hash :: "'key ⇒ 'x ⇒ 'hash"
begin

type_synonym ('x', 'hash') adversary = "(unit, 'x' + ('x' × 'hash'), 'hash' + unit) gpv"

definition oracle_hash :: "'key ⇒ ('x, 'hash, 'x set) callee"
where
  "oracle_hash k = (λL y. do {
    let t = hash k y;
    let L = insert y L;
    return_spmf (t, L)
  })"

definition oracle_flag :: "'key ⇒ ('x × 'hash, unit, bool × 'x set) callee"
where
  "oracle_flag = (λkey (flg, L) (y, t).
    return_spmf ((), (flg ∨ (t = (hash key y) ∧ y ∉ L), L)))"

abbreviation "oracle" :: "'key ⇒ ('x + 'x × 'hash, 'hash + unit, bool × 'x set) callee"
where "oracle key ≡ †(oracle_hash key) ⊕⇩O oracle_flag key"

definition game :: "('x, 'hash) adversary ⇒ bool spmf"
where
  "game 𝒜 = do {
    key ← key_gen;
    (_, (flag', L')) ← exec_gpv (oracle key) 𝒜 (False, {});
    return_spmf flag'
  }"

definition advantage :: "('x, 'hash) adversary ⇒ real"
where "advantage 𝒜 = spmf (game 𝒜) True"

type_synonym ('x', 'hash') adversary1 = "('x' × 'hash', 'x', 'hash') gpv"

definition game1 :: "('x, 'hash) adversary1 ⇒ bool spmf"
where
  "game1 𝒜 = do {
    key ← key_gen;
    ((m, h), L) ← exec_gpv (oracle_hash key) 𝒜 {};
    return_spmf (h = hash key m ∧ m ∉ L)
  }"

definition advantage1 :: "('x, 'hash) adversary1 ⇒ real"
  where "advantage1 𝒜 = spmf (game1 𝒜) True"

lemma advantage_advantage1:
  assumes bound: "interaction_bounded_by (Not ∘ isl) 𝒜 q"
  shows "advantage 𝒜 ≤ advantage1 (guessing_many_one.reduction q (λ_ :: unit. 𝒜) ()) * q"
proof -
  let ?init = "map_spmf (λkey. (key, (), {})) key_gen"
  let ?oracle = "λkey . oracle_hash key"
  let ?eval = "λkey (_ :: unit) L (x, h). return_spmf (h = hash key x ∧ x ∉ L)"

  interpret guessing_many_one ?init ?oracle ?eval .

  have [simp]: "oracle_flag key = eval_oracle key ()" for key
    by(simp add: oracle_flag_def eval_oracle_def fun_eq_iff)
  have "game 𝒜 = game_multi (λ_. 𝒜)"
    by(auto simp add: game_multi_def game_def bind_map_spmf intro!: bind_spmf_cong[OF refl])
  hence "advantage 𝒜 = advantage_multi (λ_. 𝒜)" by(simp add: advantage_def advantage_multi_def)
  also have "… ≤ advantage_single (reduction q (λ_. 𝒜)) * q" using bound
    by(rule many_single_reduction)(auto simp add: oracle_hash_def)
  also have "advantage_single (reduction q (λ_. 𝒜)) = advantage1 (reduction q (λ_. 𝒜) ())" for 𝒜
    unfolding advantage1_def advantage_single_def
    by(auto simp add: game1_def game_single_def bind_map_spmf o_def intro!: bind_spmf_cong[OF refl] arg_cong2[where f=spmf])
  finally show ?thesis .
qed

end

end