Theory PRF_UHF
subsection ‹Extending the input length of a PRF using a universal hash function›
text ‹ This example is taken from \<^cite>‹‹\S 4.2› in "Shoup2004IACR"›.›
theory PRF_UHF imports
CryptHOL.GPV_Bisim
Pseudo_Random_Function
begin
locale "hash" =
fixes seed_gen :: "'seed spmf"
and "hash" :: "'seed ⇒ 'domain ⇒ 'range"
begin
definition game_hash :: " 'domain ⇒ 'domain ⇒ bool spmf"
where
"game_hash w w' = do {
seed ← seed_gen;
return_spmf (hash seed w = hash seed w' ∧ w ≠ w')
}"
definition game_hash_set :: "'domain set ⇒ bool spmf"
where
"game_hash_set W = do {
seed ← seed_gen;
return_spmf (¬ inj_on (hash seed) W)
}"
definition ε_uh :: "real"
where "ε_uh = (SUP w w'. spmf (game_hash w w') True)"
lemma ε_uh_nonneg : "ε_uh ≥ 0"
by(auto 4 3 intro!: cSUP_upper2 bdd_aboveI2[where M=1] cSUP_least pmf_le_1 pmf_nonneg simp add: ε_uh_def)
lemma hash_ineq_card:
assumes "finite W"
shows "spmf (game_hash_set W) True ≤ ε_uh * card W * card W"
proof -
let ?M = "measure (measure_spmf seed_gen)"
have bound: "?M {x. hash x w = hash x w' ∧ w ≠ w'} ≤ ε_uh" for w w'
proof -
have "?M {x. hash x w = hash x w' ∧ w ≠ w'} = spmf (game_hash w w') True"
by(simp add: game_hash_def spmf_conv_measure_spmf map_spmf_conv_bind_spmf[symmetric] measure_map_spmf vimage_def)
also have "… ≤ ε_uh" unfolding ε_uh_def
by(auto intro!: cSUP_upper2 bdd_aboveI[where M=1] cSUP_least simp add: pmf_le_1)
finally show ?thesis .
qed
have "spmf (game_hash_set W) True = ?M {x. ∃xa∈W. ∃y∈W. hash x xa = hash x y ∧ xa ≠ y}"
by(auto simp add: game_hash_set_def inj_on_def map_spmf_conv_bind_spmf[symmetric] spmf_conv_measure_spmf measure_map_spmf vimage_def)
also have "{x. ∃xa∈W. ∃y∈W. hash x xa = hash x y ∧ xa ≠ y} = (⋃(w, w') ∈ W× W. {x. hash x w = hash x w' ∧ w ≠ w'})"
by(auto)
also have "?M … ≤ (∑(w, w')∈W × W. ?M {x. hash x w = hash x w' ∧ w ≠ w'})"
by(auto intro!: measure_spmf.finite_measure_subadditive_finite simp add: split_def assms)
also have "… ≤ (∑(w, w')∈W × W. ε_uh)" by(rule sum_mono)(clarsimp simp add: bound)
also have "… = ε_uh * card(W) * card(W)" by(simp add: card_cartesian_product)
finally show ?thesis .
qed
end
locale prf_hash =
fixes f :: "'key ⇒ 'α ⇒ 'γ"
and h :: "'seed ⇒ 'β ⇒ 'α"
and key_gen :: "'key spmf"
and seed_gen :: "'seed spmf"
and range_f :: "'γ set"
assumes lossless_seed_gen: "lossless_spmf seed_gen"
and range_f_finite: "finite range_f"
and range_f_nonempty: "range_f ≠ {}"
begin
definition rand :: "'γ spmf"
where "rand = spmf_of_set range_f"
lemma lossless_rand [simp]: "lossless_spmf rand"
by(simp add: rand_def range_f_finite range_f_nonempty)
definition key_seed_gen :: "('key * 'seed) spmf"
where
"key_seed_gen = do {
k ← key_gen;
s :: 'seed ← seed_gen;
return_spmf (k, s)
}"
interpretation "prf": "prf" key_gen f rand .
interpretation hash: hash "seed_gen" "h".
fun f' :: "'key × 'seed ⇒ 'β ⇒ 'γ"
where "f' (key, seed) x = f key (h seed x)"
interpretation "prf'": "prf" key_seed_gen f' rand .
definition reduction_oracle :: "'seed ⇒ unit ⇒ 'β ⇒ ('γ × unit, 'α, 'γ) gpv"
where "reduction_oracle seed x b = Pause (h seed b) (λx. Done (x, ()))"
definition prf'_reduction :: " ('β, 'γ) prf'.adversary ⇒ ('α, 'γ) prf.adversary"
where
"prf'_reduction 𝒜 = do {
seed ← lift_spmf seed_gen;
(b, σ) ← inline (reduction_oracle seed) 𝒜 ();
Done b
}"
theorem prf_prf'_advantage:
assumes "prf'.lossless 𝒜"
and bounded: "prf'.ibounded_by 𝒜 q"
shows "prf'.advantage 𝒜 ≤ prf.advantage (prf'_reduction 𝒜) + hash.ε_uh * q * q"
including lifting_syntax
proof -
let ?𝒜 = "prf'_reduction 𝒜"
{ define cr where "cr = (λ_ :: unit × unit. λ_ :: unit. True)"
have [transfer_rule]: "cr ((), ()) ()" by(simp add: cr_def)
have "prf.game_0 ?𝒜 = prf'.game_0 𝒜"
unfolding prf'.game_0_def prf.game_0_def prf'_reduction_def unfolding key_seed_gen_def
by(simp add: exec_gpv_bind split_def exec_gpv_inline reduction_oracle_def bind_map_spmf prf.prf_oracle_def prf'.prf_oracle_def[abs_def])
(transfer_prover) }
note hop1 = this[symmetric]
define semi_forgetful_RO where "semi_forgetful_RO = (λseed :: 'seed. λ(σ :: 'α ⇀ 'β × 'γ, b :: bool). λx.
case σ (h seed x) of Some (a, y) ⇒ return_spmf (y, (σ, a ≠ x ∨ b))
| None ⇒ bind_spmf rand (λy. return_spmf (y, (σ(h seed x ↦ (x, y)), b))))"
define game_semi_forgetful where "game_semi_forgetful = do {
seed :: 'seed ← seed_gen;
(b, rep) ← exec_gpv (semi_forgetful_RO seed) 𝒜 (Map.empty, False);
return_spmf (b, rep)
}"
have bad_semi_forgetful [simp]: "callee_invariant (semi_forgetful_RO seed) snd" for seed
by(unfold_locales)(auto simp add: semi_forgetful_RO_def split: option.split_asm)
have lossless_semi_forgetful [simp]: "lossless_spmf (semi_forgetful_RO seed s1 x)" for seed s1 x
by(simp add: semi_forgetful_RO_def split_def split: option.split)
{ define cr
where "cr = (λ(_ :: unit, σ) (σ' :: 'α ⇒ ('β × 'γ) option, _ :: bool). σ = map_option snd ∘ σ')"
define initial where "initial = (Map.empty :: 'α ⇒ ('β × 'γ) option, False)"
have [transfer_rule]: "cr ((), Map.empty) initial" by(simp add: cr_def initial_def fun_eq_iff)
have [transfer_rule]: "((=) ===> cr ===> (=) ===> rel_spmf (rel_prod (=) cr))
(λy p ya. do {y ← prf.random_oracle (snd p) (h y ya); return_spmf (fst y, (), snd y) })
semi_forgetful_RO"
by(auto simp add: semi_forgetful_RO_def cr_def prf.random_oracle_def rel_fun_def fun_eq_iff split: option.split intro!: rel_spmf_bind_reflI)
have "prf.game_1 ?𝒜 = map_spmf fst game_semi_forgetful"
unfolding prf.game_1_def prf'_reduction_def game_semi_forgetful_def
by(simp add: exec_gpv_bind exec_gpv_inline split_def bind_map_spmf map_spmf_bind_spmf o_def map_spmf_conv_bind_spmf reduction_oracle_def initial_def[symmetric])
(transfer_prover) }
note hop2 = this
define game_semi_forgetful_bad where "game_semi_forgetful_bad = do {
seed :: 'seed ← seed_gen;
x ← exec_gpv (semi_forgetful_RO seed) 𝒜 (Map.empty, False);
return_spmf (snd x)
}"
have game_semi_forgetful_bad : "map_spmf snd game_semi_forgetful = game_semi_forgetful_bad"
unfolding game_semi_forgetful_bad_def game_semi_forgetful_def
by(simp add: map_spmf_bind_spmf o_def)
have bad_random_oracle_A [simp]: "callee_invariant prf.random_oracle (λσ. ¬ inj_on (h seed) (dom σ))" for seed
by unfold_locales(auto simp add: prf.random_oracle_def split: option.split_asm)
define invar
where "invar = (λseed (σ1, b) (σ2 :: 'β ⇒ 'γ option). ¬ b ∧ dom σ1 = h seed ` dom σ2 ∧
(∀x ∈ dom σ2. σ1 (h seed x) = map_option (Pair x) (σ2 x)))"
have rel_spmf_oracle_adv:
"rel_spmf (λ(x, s1) (y, s2). snd s1 ≠ inj_on (h seed) (dom s2) ∧ (inj_on (h seed) (dom s2) ⟶ x = y ∧ invar seed s1 s2))
(exec_gpv (semi_forgetful_RO seed) 𝒜 (Map.empty, False))
(exec_gpv prf.random_oracle 𝒜 Map.empty)"
if seed: "seed ∈ set_spmf seed_gen" for seed
proof -
have invar_initial [simp]: "invar seed (Map.empty, False) Map.empty" by(simp add: invar_def)
have invarD_inj: "inj_on (h seed) (dom s2)" if "invar seed bs1 s2" for bs1 s2
using that by(auto intro!: inj_onI simp add: invar_def)(metis domI domIff option.map_sel prod.inject)
let ?R = "λ(a, s1) (b, s2 :: 'β ⇒ 'γ option).
snd s1 = (¬ inj_on (h seed) (dom s2)) ∧
(¬ ¬ inj_on (h seed) (dom s2) ⟶ a = b ∧ invar seed s1 s2)"
have step: "rel_spmf ?R (semi_forgetful_RO seed σ1b x) (prf.random_oracle s2 x)"
if X: "invar seed σ1b s2" for s2 σ1b x
proof -
obtain σ1 b where [simp]: "σ1b = (σ1, b)" by(cases σ1b)
from X have not_b: "¬ b"
and dom: "dom σ1 = h seed ` dom s2"
and eq: "∀x∈dom s2. σ1 (h seed x) = map_option (Pair x) (s2 x)"
by(simp_all add: invar_def)
from X have inj: "inj_on (h seed) (dom s2)" by(rule invarD_inj)
have not_in_image: "h seed x ∉ h seed ` (dom s2 - {x})" if "σ1 (h seed x) = None"
proof (rule notI)
assume "h seed x ∈ h seed ` (dom s2 - {x})"
then obtain y where "y ∈ dom s2" and hx_hy: "h seed x = h seed y" by (auto)
then have "σ1 (h seed y) = None" using that by (auto)
then have "h seed y ∉ h seed ` dom s2" using dom by (auto)
then have "y ∉ dom s2" by (auto)
then show False using ‹y ∈ dom s2› by(auto)
qed
show ?thesis
proof(cases "σ1 (h seed x)")
case σ1: None
hence s2: "s2 x = None" using dom by(auto)
have "insert (h seed x) (dom σ1) = insert (h seed x) (h seed ` dom s2)" by(simp add: dom)
then have invar_update: "invar seed (σ1(h seed x ↦ (x, bs)), False) (s2(x ↦ bs))" for bs
using inj not_b not_in_image σ1 dom
by(auto simp add: invar_def domIff eq) (metis domI domIff imageI)
with σ1 s2 show ?thesis using inj not_b not_in_image
by(auto simp add: semi_forgetful_RO_def prf.random_oracle_def intro: rel_spmf_bind_reflI)
next
case σ1: (Some "by")
show ?thesis
proof(cases "s2 x")
case s2: (Some z)
with eq σ1 have "by = (x, z)" by(auto simp add: domIff)
thus ?thesis using σ1 inj not_b s2 X
by(simp add: semi_forgetful_RO_def prf.random_oracle_def split_beta)
next
case s2: None
from σ1 dom obtain y where y: "y ∈ dom s2" and *: "h seed x = h seed y"
by(metis domIff imageE option.distinct(1))
from y obtain z where z: "s2 y = Some z" by auto
from eq z σ1 have "by": "by = (y, z)" by(auto simp add: * domIff)
from y s2 have xny: "x ≠ y" by auto
with y * have "h seed x ∈ h seed ` (dom s2 - {x})" by auto
then show ?thesis using σ1 s2 not_b "by" xny inj
by(simp add: semi_forgetful_RO_def prf.random_oracle_def split_beta)(rule rel_spmf_bindI2; simp)
qed
qed
qed
from invar_initial _ step show ?thesis
by(rule exec_gpv_oracle_bisim_bad_full[where ?bad1.0 = "snd" and ?bad2.0 = "λσ. ¬ inj_on (h seed) (dom σ)"])
(simp_all add: assms)
qed
define game_A where "game_A = do {
seed :: 'seed ← seed_gen;
(b, σ) ← exec_gpv prf.random_oracle 𝒜 Map.empty;
return_spmf (b, ¬ inj_on (h seed) (dom σ))
}"
let ?bad1 = "λx. snd (snd x)" and ?bad2 = "snd"
have hop3: "rel_spmf (λx xa. (?bad1 x ⟷ ?bad2 xa) ∧ (¬ ?bad2 xa ⟶ fst x ⟷ fst xa)) game_semi_forgetful game_A"
unfolding game_semi_forgetful_def game_A_def
by(clarsimp simp add: restrict_bind_spmf split_def map_spmf_bind_spmf restrict_return_spmf o_def intro!: rel_spmf_bind_reflI simp del: bind_return_spmf)
(rule rel_spmf_bindI[OF rel_spmf_oracle_adv]; auto)
have bad1_bad2: "spmf (map_spmf (snd ∘ snd) game_semi_forgetful) True = spmf (map_spmf snd game_A) True"
using fundamental_lemma_bad[OF hop3] by(simp add: measure_map_spmf spmf_conv_measure_spmf vimage_def)
have bound_bad1_event: "¦spmf (map_spmf fst game_semi_forgetful) True - spmf (map_spmf fst game_A) True¦ ≤ spmf (map_spmf (snd ∘ snd) game_semi_forgetful) True"
using fundamental_lemma[OF hop3] by(simp add: measure_map_spmf spmf_conv_measure_spmf vimage_def)
then have bound_bad2_event : "¦spmf (map_spmf fst game_semi_forgetful) True - spmf (map_spmf fst game_A) True¦ ≤ spmf (map_spmf snd game_A) True"
using bad1_bad2 by (simp)
define game_B where "game_B = do {
(b, σ) ← exec_gpv prf.random_oracle 𝒜 Map.empty;
hash.game_hash_set (dom σ)
}"
have game_A_game_B: "map_spmf snd game_A = game_B"
unfolding game_B_def game_A_def hash.game_hash_set_def including monad_normalisation
by(simp add: map_spmf_bind_spmf o_def split_def)
have game_B_bound : "spmf game_B True ≤ hash.ε_uh * q * q" unfolding game_B_def
proof(rule spmf_bind_leI, clarify)
fix b σ
assume *: "(b, σ) ∈ set_spmf (exec_gpv prf.random_oracle 𝒜 Map.empty)"
have "finite (dom σ)" by(rule prf.finite.exec_gpv_invariant[OF *]) simp_all
then have "spmf (hash.game_hash_set (dom σ)) True ≤ hash.ε_uh * (card (dom σ) * card (dom σ))"
using hash.hash_ineq_card[of "dom σ"] by simp
also have p1: "card (dom σ) ≤ q + card (dom (Map.empty :: 'β ⇒ 'γ option))"
by(rule prf.card_dom_random_oracle[OF bounded *]) simp
then have "card (dom σ) * card (dom σ) ≤ q * q" using mult_le_mono by auto
finally show "spmf (hash.game_hash_set (dom σ)) True ≤ hash.ε_uh * q * q"
by(simp add: hash.ε_uh_nonneg mult_left_mono)
qed(simp add: hash.ε_uh_nonneg)
have hop4: "prf'.game_1 𝒜 = map_spmf fst game_A"
by(simp add: game_A_def prf'.game_1_def map_spmf_bind_spmf o_def split_def bind_spmf_const lossless_seed_gen lossless_weight_spmfD)
have "prf'.advantage 𝒜 ≤ ¦spmf (prf.game_0 ?𝒜) True - spmf (prf'.game_1 𝒜) True¦"
using hop1 by(simp add: prf'.advantage_def)
also have "… ≤ prf.advantage ?𝒜 + ¦spmf (prf.game_1 ?𝒜) True - spmf (prf'.game_1 𝒜) True¦"
by(simp add: prf.advantage_def)
also have "¦spmf (prf.game_1 ?𝒜) True - spmf (prf'.game_1 𝒜) True¦ ≤
¦spmf (map_spmf fst game_semi_forgetful) True - spmf (prf'.game_1 𝒜) True¦"
using hop2 by simp
also have "… ≤ hash.ε_uh * q * q"
using game_A_game_B game_B_bound bound_bad2_event hop4 by(simp)
finally show ?thesis by(simp add: add_left_mono)
qed
end
end