Theory ETP

subsection ‹ ETP definitions ›

text ‹ We define Extended Trapdoor Permutations (ETPs) following \<^cite>‹"DBLP:books/sp/17/Lindell17"› and \<^cite>‹"DBLP:books/cu/Goldreich2004"›. 
In particular we consider the property of Hard Core Predicates (HCPs). ›

theory ETP imports
  CryptHOL.CryptHOL
begin

type_synonym ('index,'range) dist2 = "(bool × 'index × bool × bool) ⇒ bool spmf"

type_synonym ('index,'range) advP2 = "'index ⇒ bool ⇒ bool ⇒ ('index,'range) dist2 ⇒ 'range ⇒ bool spmf"

locale etp =
  fixes I :: "('index × 'trap) spmf" ― ‹samples index and trapdoor›
    and domain :: "'index ⇒ 'range set" 
    and range :: "'index ⇒ 'range set"
    and F :: "'index ⇒ ('range ⇒ 'range)" ― ‹permutation›
    and F⇩i⇩n⇩v :: "'index ⇒ 'trap ⇒ 'range ⇒ 'range" ― ‹must be efficiently computable›
    and B :: "'index ⇒ 'range ⇒ bool" ― ‹hard core predicate›
  assumes dom_eq_ran: "y ∈ set_spmf I ⟶ domain (fst y) = range (fst y)"
    and finite_range: "y ∈ set_spmf I ⟶ finite (range (fst y))" 
    and non_empty_range: "y ∈ set_spmf I ⟶ range (fst y) ≠ {}" 
    and bij_betw: "y ∈ set_spmf I ⟶ bij_betw (F (fst y)) (domain (fst y)) (range (fst y))"
    and lossless_I: "lossless_spmf I"
    and F_f_inv: "y ∈ set_spmf I ⟶ x ∈ range (fst y) ⟶ F⇩i⇩n⇩v (fst y) (snd y) (F (fst y) x) = x"
begin

definition S :: "'index ⇒ 'range spmf"
  where "S α = spmf_of_set (range α)"

lemma lossless_S: "y ∈ set_spmf I ⟶  lossless_spmf (S (fst y))"
  by(simp add: lossless_spmf_def S_def finite_range non_empty_range)

lemma set_spmf_S [simp]: "y ∈ set_spmf I ⟶ set_spmf (S (fst y)) = range (fst y)" 
  by (simp add: S_def finite_range)

lemma f_inj_on: "y ∈ set_spmf I ⟶ inj_on (F (fst y)) (range (fst y))" 
  by(metis bij_betw_def bij_betw dom_eq_ran bij_betw_def bij_betw dom_eq_ran) 

lemma range_f: "y ∈ set_spmf I ⟶  x ∈ range (fst y) ⟶ F (fst y) x ∈ range (fst y)" 
  by (metis bij_betw bij_betw dom_eq_ran bij_betwE)   

lemma f_inv_f [simp]: "y ∈ set_spmf I ⟶ x ∈ range (fst y) ⟶ F⇩i⇩n⇩v (fst y) (snd y) (F (fst y) x) = x"
  by (metis bij_betw bij_betw_inv_into_left dom_eq_ran F_f_inv)

lemma f_inv_f' [simp]: "y ∈ set_spmf I ⟶ x ∈ range (fst y) ⟶ Hilbert_Choice.inv_into (range (fst y)) (F (fst y)) (F (fst y) x) = x" 
  by (metis bij_betw bij_betw_inv_into_left bij_betw dom_eq_ran)

lemma B_F_inv_rewrite: "(B α (F⇩i⇩n⇩v α τ y⇩σ') = (B α (F⇩i⇩n⇩v α τ y⇩σ') = m1)) = m1" 
  by auto

lemma uni_set_samp: 
  assumes "y ∈ set_spmf I"
  shows "map_spmf (λ x. F (fst y) x) (S (fst y)) = (S (fst y))" 
(is "?lhs = ?rhs")
proof-
  have rhs: "?rhs = spmf_of_set (range (fst y))" 
    unfolding S_def by(simp)
  also have "map_spmf (λ x. F (fst y) x) (spmf_of_set (range (fst y))) = spmf_of_set ((λ x. F (fst y) x) ` (range (fst y)))"
    using f_inj_on assms 
    by (metis map_spmf_of_set_inj_on) 
  also have "(λ x. F (fst y) x) ` (range (fst y)) = range (fst y)"
    apply(rule endo_inj_surj) 
    using bij_betw
      by (auto simp add: bij_betw_def dom_eq_ran f_inj_on bij_betw finite_range assms)  
  finally show ?thesis by(simp add: rhs)
qed

text‹We define the security property of the hard core predicate (HCP) using a game.›

definition HCP_game :: "('index,'range) advP2 ⇒  bool ⇒ bool ⇒ ('index,'range) dist2 ⇒ bool spmf"
  where "HCP_game A = (λ σ b⇩σ D. do {
    (α, τ) ← I;
    x ← S α;
    b' ← A α σ b⇩σ D x;
    let b = B α (F⇩i⇩n⇩v α τ x);
    return_spmf (b = b')})"

definition "HCP_adv A σ b⇩σ D = ¦((spmf (HCP_game A σ b⇩σ D) True) - 1/2)¦" 

end

end