Theory IND_CCA2_sym

(* Title: IND_CCA2_sym.thy
  Author: Andreas Lochbihler, ETH Zurich 
  Author: S. Reza Sefidgar, ETH Zurich *)

subsection ‹The IND-CCA2 security for symmetric encryption schemes›

theory IND_CCA2_sym imports
  CryptHOL.Computational_Model
begin

locale ind_cca =
  fixes key_gen :: "'key spmf"
  and encrypt :: "'key ⇒ 'message ⇒ 'cipher spmf"
  and decrypt :: "'key ⇒ 'cipher ⇒ 'message option"
  and msg_predicate :: "'message ⇒ bool"
begin

type_synonym ('message', 'cipher') adversary = 
  "(bool, 'message' × 'message' + 'cipher', 'cipher' option + 'message' option) gpv"

definition oracle_encrypt :: "'key ⇒ bool ⇒ ('message × 'message, 'cipher option, 'cipher set) callee"
where
  "oracle_encrypt k b L = (λ(msg1, msg0).
     (case msg_predicate msg1 ∧ msg_predicate msg0 of
        True ⇒ do {
         c ← encrypt k (if b then msg1 else msg0);
         return_spmf (Some c, {c} ∪ L)
        }
     | False ⇒ return_spmf (None, L)))"

lemma lossless_oracle_encrypt [simp]:
  assumes "lossless_spmf (encrypt k m1)" and "lossless_spmf (encrypt k m0)"
  shows "lossless_spmf (oracle_encrypt k b L (m1, m0))"
using assms by (simp add: oracle_encrypt_def split: bool.split)

definition oracle_decrypt :: "'key ⇒ ('cipher, 'message option, 'cipher set) callee"
where "oracle_decrypt k L c = return_spmf (if c ∈ L then None else decrypt k c, L)"

lemma lossless_oracle_decrypt [simp]: "lossless_spmf (oracle_decrypt k L c)"
by(simp add: oracle_decrypt_def)

definition game :: "('message, 'cipher) adversary ⇒ bool spmf"
where
  "game 𝒜 = do {
    key ← key_gen;
    b ← coin_spmf;
    (b', L') ← exec_gpv (oracle_encrypt key b ⊕⇩O oracle_decrypt key) 𝒜 {};
    return_spmf (b = b')
  }"

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

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

end

end