Theory IND_CPA_PK

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

theory IND_CPA_PK imports
  CryptHOL.Computational_Model
  CryptHOL.Negligible
begin

subsection ‹The IND-CPA game for public-key encryption with oracle access›

locale ind_cpa_pk = 
  fixes key_gen :: "('pubkey × 'privkey, 'call, 'ret) gpv" ― ‹probabilistic›
  and aencrypt :: "'pubkey ⇒ 'plain ⇒ ('cipher, 'call, 'ret) gpv"  ― ‹probabilistic w/ access to an oracle›
  and adecrypt :: "'privkey ⇒ 'cipher ⇒ ('plain, 'call, 'ret) gpv" ― ‹not used›
  and valid_plains :: "'plain ⇒ 'plain ⇒ bool" ― ‹checks whether a pair of plaintexts is valid, i.e., they 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 game has to ensure that the received
  plaintexts are valid.
›

type_synonym ('pubkey', 'plain', 'cipher', 'call', 'ret', 'state) adversary = 
  "('pubkey' ⇒ (('plain' × 'plain') × 'state, 'call', 'ret') gpv)
   × ('cipher' ⇒ 'state ⇒ (bool, 'call', 'ret') gpv)"

fun ind_cpa :: "('pubkey, 'plain, 'cipher, 'call, 'ret, 'state) adversary ⇒ (bool, 'call, 'ret) gpv"
where
  "ind_cpa (𝒜1, 𝒜2) = TRY do {
     (pk, sk) ← key_gen;
     b ← lift_spmf coin_spmf;
     ((m0, m1), σ) ← (𝒜1 pk);
     assert_gpv (valid_plains m0 m1);
     cipher ← aencrypt pk (if b then m0 else m1);
     guess ← 𝒜2 cipher σ; 
     Done (guess = b)
   } ELSE lift_spmf coin_spmf"

definition advantage :: "('σ ⇒ 'call ⇒ ('ret × 'σ) spmf) ⇒ 'σ ⇒ ('pubkey, 'plain, 'cipher, 'call, 'ret, 'state) adversary ⇒ real"
where "advantage oracle σ 𝒜 = ¦spmf (run_gpv oracle (ind_cpa 𝒜) σ) True - 1/2¦"

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

definition ibounded_by :: "('call ⇒ bool) ⇒ ('pubkey, 'plain, 'cipher, 'call, 'ret, 'state) adversary ⇒ enat ⇒ bool"
where 
  "ibounded_by consider = (λ(𝒜1, 𝒜2) q. 
  (∃q1 q2. (∀pk. interaction_bounded_by consider (𝒜1 pk) q1) ∧ (∀cipher σ. interaction_bounded_by consider (𝒜2 cipher σ) q2) ∧ q1 + q2 ≤ q))"

lemma ibounded_by'E [consumes 1, case_names ibounded_by', elim?]:
  assumes "ibounded_by consider (𝒜1, 𝒜2) q"
  obtains q1 q2
  where "q1 + q2 ≤ q"
  and "⋀pk. interaction_bounded_by consider (𝒜1 pk) q1"
  and "⋀cipher σ. interaction_bounded_by consider (𝒜2 cipher σ) q2"
using assms by(auto simp add: ibounded_by_def)

lemma ibounded_byI [intro?]:
  "⟦ ⋀pk. interaction_bounded_by consider (𝒜1 pk) q1; ⋀cipher σ. interaction_bounded_by consider (𝒜2 cipher σ) q2; q1 + q2 ≤ q ⟧
  ⟹ ibounded_by consider (𝒜1, 𝒜2) q"
by(auto simp add: ibounded_by_def)

definition lossless :: "('pubkey, 'plain, 'cipher, 'call, 'ret, 'state) adversary ⇒ bool"
where "lossless = (λ(𝒜1, 𝒜2). (∀pk. lossless_gpv ℐ_full (𝒜1 pk)) ∧ (∀cipher σ. lossless_gpv ℐ_full (𝒜2 cipher σ)))"

end

end