Theory Elgamal

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

section ‹Cryptographic constructions and their security›

theory Elgamal imports
  CryptHOL.Cyclic_Group_SPMF
  CryptHOL.Computational_Model
  Diffie_Hellman
  IND_CPA_PK_Single
  CryptHOL.Negligible
begin

subsection ‹Elgamal encryption scheme›

locale elgamal_base =
  fixes 𝒢 :: "'grp cyclic_group" (structure)
begin

type_synonym 'grp' pub_key = "'grp'"
type_synonym 'grp' priv_key = nat
type_synonym 'grp' plain = 'grp'
type_synonym 'grp' cipher = "'grp' × 'grp'"

definition key_gen :: "('grp pub_key × 'grp priv_key) spmf"
where 
  "key_gen = do {
     x ← sample_uniform (order 𝒢);
     return_spmf (❙g [^] x, x)
  }"

lemma key_gen_alt:
  "key_gen = map_spmf (λx. (❙g [^] x, x)) (sample_uniform (order 𝒢))"
by(simp add: map_spmf_conv_bind_spmf key_gen_def)

definition aencrypt :: "'grp pub_key ⇒ 'grp ⇒ 'grp cipher spmf"
where
  "aencrypt α msg = do {
    y ← sample_uniform (order 𝒢);
    return_spmf (❙g [^] y, (α [^] y) ⊗ msg)
  }"

lemma aencrypt_alt:
  "aencrypt α msg = map_spmf (λy. (❙g [^] y, (α [^] y) ⊗ msg)) (sample_uniform (order 𝒢))"
by(simp add: map_spmf_conv_bind_spmf aencrypt_def)

definition adecrypt :: "'grp priv_key ⇒ 'grp cipher ⇒ 'grp option"
where
  "adecrypt x = (λ(β, ζ). Some (ζ ⊗ (inv (β [^] x))))"

abbreviation valid_plains :: "'grp ⇒ 'grp ⇒ bool"
where "valid_plains msg1 msg2 ≡ msg1 ∈ carrier 𝒢 ∧ msg2 ∈ carrier 𝒢"

sublocale ind_cpa: ind_cpa key_gen aencrypt adecrypt valid_plains .
sublocale ddh: ddh 𝒢 .

fun elgamal_adversary :: "('grp pub_key, 'grp plain, 'grp cipher, 'state) ind_cpa.adversary ⇒ 'grp ddh.adversary"
where
  "elgamal_adversary (𝒜1, 𝒜2) α β γ = TRY do {
    b ← coin_spmf;
    ((msg1, msg2), σ) ← 𝒜1 α;
    ― ‹have to check that the attacker actually sends two elements from the group; otherwise flip a coin›
    _ :: unit ← assert_spmf (valid_plains msg1 msg2);
    guess ← 𝒜2 (β, γ ⊗ (if b then msg1 else msg2)) σ;
    return_spmf (guess = b)
  } ELSE coin_spmf"

end

locale elgamal = elgamal_base + cyclic_group 𝒢
begin 

theorem advantage_elgamal: "ind_cpa.advantage 𝒜 = ddh.advantage (elgamal_adversary 𝒜)"
  including monad_normalisation
proof -
  obtain 𝒜1 and 𝒜2 where "𝒜 = (𝒜1, 𝒜2)" by(cases 𝒜)
  note [simp] = this order_gt_0_iff_finite finite_carrier try_spmf_bind_out split_def o_def spmf_of_set bind_map_spmf weight_spmf_le_1 scale_bind_spmf bind_spmf_const
    and [cong] = bind_spmf_cong_simp
  have "ddh.ddh_1 (elgamal_adversary 𝒜) = TRY do {
       x ← sample_uniform (order 𝒢);
       y ← sample_uniform (order 𝒢);
       ((msg1, msg2), σ) ← 𝒜1 (❙g [^] x);
       _ :: unit ← assert_spmf (valid_plains msg1 msg2);
       b ← coin_spmf;
       z ← map_spmf (λz. ❙g [^] z ⊗ (if b then msg1 else msg2)) (sample_uniform (order 𝒢));
       guess ← 𝒜2 (❙g [^] y, z) σ;
       return_spmf (guess ⟷ b)
     } ELSE coin_spmf"
    by(simp add: ddh.ddh_1_def)
  also have "… = TRY do {
       x ← sample_uniform (order 𝒢);
       y ← sample_uniform (order 𝒢);
       ((msg1, msg2), σ) ← 𝒜1 (❙g [^] x);
       _ :: unit ← assert_spmf (valid_plains msg1 msg2);
       z ← map_spmf (λz. ❙g [^] z) (sample_uniform (order 𝒢));
       guess ← 𝒜2 (❙g [^] y, z) σ;
       map_spmf ((=) guess) coin_spmf
     } ELSE coin_spmf"
    by(simp add: sample_uniform_one_time_pad map_spmf_conv_bind_spmf[where p=coin_spmf])
  also have "… = coin_spmf"
    by(simp add: map_eq_const_coin_spmf try_bind_spmf_lossless2')
  also have "ddh.ddh_0 (elgamal_adversary 𝒜) = ind_cpa.ind_cpa 𝒜"
    by(simp add: ddh.ddh_0_def IND_CPA_PK_Single.ind_cpa.ind_cpa_def key_gen_def aencrypt_def nat_pow_pow eq_commute)
  ultimately show ?thesis by(simp add: ddh.advantage_def ind_cpa.advantage_def)
qed

end
  
locale elgamal_asymp = 
  fixes 𝒢 :: "security ⇒ 'grp cyclic_group"
  assumes elgamal: "⋀η. elgamal (𝒢 η)"
begin
  
sublocale elgamal "𝒢 η" for η by(simp add: elgamal)
    
theorem elgamal_secure:
  "negligible (λη. ind_cpa.advantage η (𝒜 η))" if "negligible (λη. ddh.advantage η (elgamal_adversary η (𝒜 η)))"
  by(simp add: advantage_elgamal that)

end

context elgamal_base begin

lemma lossless_key_gen [simp]: "lossless_spmf (key_gen) ⟷ 0 < order 𝒢"
by(simp add: key_gen_def Let_def)

lemma lossless_aencrypt [simp]:
  "lossless_spmf (aencrypt key plain) ⟷ 0 < order 𝒢"
by(simp add: aencrypt_def Let_def)

lemma lossless_elgamal_adversary:
  "⟦ ind_cpa.lossless 𝒜; 0 < order 𝒢 ⟧
  ⟹ ddh.lossless (elgamal_adversary 𝒜)"
by(cases 𝒜)(simp add: ddh.lossless_def ind_cpa.lossless_def Let_def split_def)

end

end