Theory IND_CPA_PK_Single

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

theory IND_CPA_PK_Single imports
  CryptHOL.Computational_Model
begin

subsection ‹The IND-CPA game (public key, single instance)›

locale ind_cpa = 
  fixes key_gen :: "('pub_key × 'priv_key) spmf" ― ‹probabilistic›
  and aencrypt :: "'pub_key ⇒ 'plain ⇒ 'cipher spmf"  ― ‹probabilistic›
  and adecrypt :: "'priv_key ⇒ 'cipher ⇒ 'plain option" ― ‹deterministic, but not used›
  and valid_plains :: "'plain ⇒ 'plain ⇒ bool" ― ‹checks whether a pair of plaintexts is valid, i.e., they both have the right format›
begin

text ‹
  We cannot incorporate the predicate @{term valid_plain} in the type @{typ "'plain"} of plaintexts,
  because the single @{typ "'plain"} must contain plaintexts for all values of the security parameter,
  as HOL does not have dependent types.  Consequently, the oracle has to ensure that the received
  plaintexts are valid.
›

type_synonym ('pub_key', 'plain', 'cipher', 'state) adversary = 
  "('pub_key' ⇒ (('plain' × 'plain') × 'state) spmf)
   × ('cipher' ⇒ 'state ⇒ bool spmf)"

primrec ind_cpa :: "('pub_key, 'plain, 'cipher, 'state) adversary ⇒ bool spmf"
where
  "ind_cpa (𝒜1, 𝒜2) = TRY do {
     (pk, sk) ← key_gen;
     ((m0, m1), σ) ← 𝒜1 pk;
     _ :: unit ← assert_spmf (valid_plains m0 m1);
     b ← coin_spmf;
     cipher ← aencrypt pk (if b then m0 else m1);
     b' ← 𝒜2 cipher σ;
     return_spmf (b = b')
  } ELSE coin_spmf"

declare ind_cpa.simps [simp del]

definition advantage :: "('pub_key, 'plain, 'cipher, 'state) adversary ⇒ real"
where "advantage 𝒜 = ¦spmf (ind_cpa 𝒜) True - 1/2¦"

definition lossless :: "('pub_key, 'plain, 'cipher, 'state) adversary ⇒ bool"
where
  "lossless 𝒜 ⟷
   ((∀pk. lossless_spmf (fst 𝒜 pk)) ∧
        (∀cipher σ. lossless_spmf (snd 𝒜 cipher σ)))"

lemma lossless_ind_cpa:
  "⟦ lossless 𝒜; lossless_spmf (key_gen) ⟧ ⟹ lossless_spmf (ind_cpa 𝒜)"
by(auto simp add: lossless_def ind_cpa_def split_def Let_def)

end

end