Theory IND_CPA

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

theory IND_CPA imports
  CryptHOL.Generative_Probabilistic_Value
  CryptHOL.Computational_Model
  CryptHOL.Negligible
begin

subsection ‹The IND-CPA game for symmetric encryption schemes›

locale ind_cpa = 
  fixes key_gen :: "'key spmf" ― ‹probabilistic›
  and encrypt :: "'key ⇒ 'plain ⇒ 'cipher spmf"  ― ‹probabilistic›
  and decrypt :: "'key ⇒ 'cipher ⇒ 'plain option" ― ‹deterministic, but not used›
  and valid_plain :: "'plain ⇒ bool" ― ‹checks whether a plain text is valid, i.e., has 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 ('plain', 'cipher', 'state) adversary = 
  "(('plain' × 'plain') × 'state, 'plain', 'cipher') gpv
   × ('cipher' ⇒ 'state ⇒ (bool, 'plain', 'cipher') gpv)"

definition encrypt_oracle :: "'key ⇒ unit ⇒ 'plain ⇒ ('cipher × unit) spmf"
where
  "encrypt_oracle key σ plain = do {
     cipher ← encrypt key plain;
     return_spmf (cipher, ())
  }"

definition ind_cpa :: "('plain, 'cipher, 'state) adversary ⇒ bool spmf"
where
  "ind_cpa 𝒜 = do {
     let (𝒜1, 𝒜2) = 𝒜;
     key ← key_gen;
     b ← coin_spmf;
     (guess, _) ← exec_gpv (encrypt_oracle key) (do {
         ((m0, m1), σ) ← 𝒜1;
         if valid_plain m0 ∧ valid_plain m1 then do {
           cipher ← lift_spmf (encrypt key (if b then m0 else m1));
           𝒜2 cipher σ
         } else lift_spmf coin_spmf
       }) ();
     return_spmf (guess = b)
  }"

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

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

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

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

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

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

end

end