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