Theory Delta_Correct

theory Delta_Correct

imports "HOL-Probability.Probability"

begin 
section ‹$\delta$-Correctness of PKEs›
text ‹The following locale defines the $\delta$-correctness of a public key encryption (PKE) scheme
given by the algorithms ‹key_gen› ‹encrypt› and ‹decrypt›.
‹Msgs› is the set of all possible messages that can be encoded with the PKE.
Since some PKE have a small failure probability, the definition of correctness has to be 
adapted to cover the case of failures as well. 
The standard definition of such $\delta$-correctness is given in the function ‹expect_correct›.›
locale pke_delta_correct =
fixes key_gen :: "('pk × 'sk) pmf"
  and encrypt :: "'pk ⇒ 'plain ⇒ 'cipher pmf" 
  and decrypt :: "'sk ⇒ 'cipher ⇒ 'plain"
  and Msgs :: "'plain set"
begin

type_synonym ('pk', 'sk') cor_adversary = "('pk' ⇒ 'sk' ⇒ bool pmf)"

definition expect_correct where
"expect_correct = measure_pmf.expectation key_gen
  (λ(pk,sk). MAX m∈Msgs. pmf (bind_pmf (encrypt pk m)
  (λc. return_pmf (decrypt sk c ≠ m))) True)"

definition delta_correct where
"delta_correct delta = (expect_correct ≤ delta)"

text ‹‹game_correct› is the game played to guarantee correctness. If an adversary ‹Adv› has a 
non-negligible advantage in the correctness game, he might have enough information to break 
the PKE.
However, the definition of this correctness game is somewhat questionable, since the adversary 
‹Adv› is given the secret key as well, thus enabling him to break the encryption and the PKE.›

definition game_correct where
"game_correct Adv = do{
      (pk,sk) ← key_gen;
      m ← Adv pk sk;
      c ← encrypt pk m;
      let m' = decrypt sk c;
      return_pmf (m' ≠ m)
    }"


end

text ‹An auxiliary lemma to handle the maximum over a sum.›

lemma max_sum:
fixes A B and f :: "'a ⇒ 'b ⇒ 'c :: {ordered_comm_monoid_add, linorder}"
assumes "finite A " "A ≠ {}"
shows "(MAX x∈A. (∑y∈B. f x y)) ≤ (∑y∈B. (MAX x∈A. f x y))"
proof -
  obtain x where "x∈A" and "(∑y∈B. f x y) = (MAX x∈A. (∑y∈B. f x y))" using assms
  by (metis (no_types, lifting) Max_in finite_imageI imageE image_is_empty)
  moreover have "(∑y∈B. f x y) ≤ (∑y∈B. MAX x∈A. f x y)" 
    by (intro sum_mono) (simp add: assms(1) calculation(1))
  ultimately show ?thesis by metis
qed

end