Theory Pseudo_Random_Function

(* Title: Pseudo_Random_Function.thy
  Author: Andreas Lochbihler, ETH Zurich *)

theory Pseudo_Random_Function imports
  CryptHOL.Computational_Model
begin

subsection ‹Pseudo-random function›

locale random_function =
  fixes p :: "'a spmf"
begin

type_synonym ('b,'a') dict = "'b ⇀ 'a'"

definition random_oracle :: "('b, 'a) dict ⇒ 'b ⇒ ('a × ('b, 'a) dict) spmf"
where
  "random_oracle σ x =
  (case σ x of Some y ⇒ return_spmf (y, σ)
   | None ⇒ p ⤜ (λy. return_spmf (y, σ(x ↦ y))))"

definition forgetful_random_oracle :: "unit ⇒ 'b ⇒ ('a × unit) spmf"
where
  "forgetful_random_oracle σ x = p ⤜ (λy. return_spmf (y, ()))"

lemma weight_random_oracle [simp]:
  "weight_spmf p = 1 ⟹ weight_spmf (random_oracle σ x) = 1"
by(simp add: random_oracle_def weight_bind_spmf o_def split: option.split)

lemma lossless_random_oracle [simp]:
  "lossless_spmf p ⟹ lossless_spmf (random_oracle σ x)"
by(simp add: lossless_spmf_def)

sublocale finite: callee_invariant_on random_oracle "λσ. finite (dom σ)" ℐ_full
by(unfold_locales)(auto simp add: random_oracle_def split: option.splits)

lemma card_dom_random_oracle:
  assumes "interaction_any_bounded_by 𝒜 q"
  and "(y, σ') ∈ set_spmf (exec_gpv random_oracle 𝒜 σ)"
  and fin: "finite (dom σ)"
  shows "card (dom σ') ≤ q + card (dom σ)"
by(rule finite.interaction_bounded_by'_exec_gpv_count[OF assms(1-2)])
  (auto simp add: random_oracle_def fin card_insert_if simp del: fun_upd_apply split: option.split_asm)

end

subsection ‹Pseudo-random function›

locale "prf" =
  fixes key_gen :: "'key spmf"
  and "prf" :: "'key ⇒ 'domain ⇒ 'range"
  and rand :: "'range spmf"
begin

sublocale random_function "rand" .

definition prf_oracle :: "'key ⇒ unit ⇒ 'domain ⇒ ('range × unit) spmf"
where "prf_oracle key σ x = return_spmf (prf key x, ())"

type_synonym ('domain', 'range') adversary = "(bool, 'domain', 'range') gpv"

definition game_0 :: "('domain, 'range) adversary ⇒ bool spmf"
where
  "game_0 𝒜 = do {
     key ← key_gen;
     (b, _) ← exec_gpv (prf_oracle key) 𝒜 ();
     return_spmf b
   }"

definition game_1 :: "('domain, 'range) adversary ⇒ bool spmf"
where
  "game_1 𝒜 = do {
     (b, _) ← exec_gpv random_oracle 𝒜 Map.empty;
     return_spmf b
   }"

definition advantage :: "('domain, 'range) adversary ⇒ real"
where "advantage 𝒜 = ¦spmf (game_0 𝒜) True - spmf (game_1 𝒜) True¦"

lemma advantage_nonneg: "advantage 𝒜 ≥ 0"
by(simp add: advantage_def)

abbreviation lossless :: "('domain, 'range) adversary ⇒ bool"
where "lossless ≡ lossless_gpv ℐ_full"

abbreviation (input) ibounded_by :: "('domain, 'range) adversary ⇒ enat ⇒ bool"
where "ibounded_by ≡ interaction_any_bounded_by"

end

end