Theory Chaum_Pedersen_Sigma_Commit

subsection‹Chaum-Pedersen ‹Σ›-protocol›

text‹The Chaum-Pedersen ‹Σ›-protocol \<^cite>‹"DBLP:conf/crypto/ChaumP92"› considers a relation of equality of discrete logs.›

theory Chaum_Pedersen_Sigma_Commit imports
  Commitment_Schemes
  Sigma_Protocols
  Cyclic_Group_Ext
  Discrete_Log
  Number_Theory_Aux
  Uniform_Sampling 
begin 

locale chaum_ped_Σ_base = 
  fixes 𝒢 :: "'grp cyclic_group" (structure)
    and x :: nat
  assumes  prime_order: "prime (order 𝒢)"
begin

definition "g' = ❙g [^] x"

lemma or_gt_1: "order 𝒢 > 1" 
  using prime_order 
  using prime_gt_1_nat by blast

lemma or_gt_0 [simp]:"order 𝒢 > 0" 
  using or_gt_1 by simp

type_synonym witness = "nat"
type_synonym rand = nat 
type_synonym 'grp' msg = "'grp' × 'grp'"
type_synonym response = nat
type_synonym challenge = nat
type_synonym 'grp' pub_in = "'grp' × 'grp'"

definition "G = do {
    w ← sample_uniform (order 𝒢);
    return_spmf ((❙g [^] w, g' [^] w), w)}"

lemma lossless_G: "lossless_spmf G"
  by(simp add: G_def)

definition "challenge_space = {..< order 𝒢}" 

definition init :: "'grp pub_in ⇒ witness ⇒ (rand × 'grp msg) spmf"
  where "init h w = do {
    let (h, h') = h;  
    r ← sample_uniform (order 𝒢);
    return_spmf (r, ❙g [^] r, g' [^] r)}"

lemma lossless_init: "lossless_spmf (init h w)" 
  by(simp add:  init_def)

definition "response r w e = return_spmf ((w*e + r) mod (order 𝒢))"

lemma lossless_response: "lossless_spmf (response r w  e)"
  by(simp add: response_def)

definition check :: "'grp pub_in ⇒ 'grp msg ⇒ challenge ⇒ response ⇒ bool"
  where "check h a e z =  (fst a ⊗ (fst h [^] e) = ❙g [^] z ∧ snd a ⊗ (snd h [^] e) = g' [^] z ∧ fst a ∈ carrier 𝒢 ∧ snd a ∈ carrier 𝒢)"

definition R :: "('grp pub_in × witness) set"
  where "R = {(h, w). (fst h = ❙g [^] w ∧ snd h = g' [^] w)}"

definition S2 :: "'grp pub_in ⇒ challenge ⇒ ('grp msg, response) sim_out spmf"
  where "S2 H c = do {
  let (h, h') = H;
  z ← (sample_uniform (order 𝒢));
  let a = ❙g [^] z ⊗ inv (h [^] c); 
  let a' =  g' [^] z ⊗ inv (h' [^] c);
  return_spmf ((a,a'), z)}"

definition ss_adversary :: "'grp pub_in ⇒ ('grp msg, challenge, response) conv_tuple ⇒ ('grp msg, challenge, response) conv_tuple ⇒ nat spmf"
  where "ss_adversary x' c1 c2 = do {
    let ((a,a'), e, z) = c1;
    let ((b,b'), e', z') = c2;
    return_spmf (if (e mod order 𝒢 > e' mod order 𝒢) then (nat ((int z - int z') * (fst (bezw ((e mod order 𝒢 - e' mod order 𝒢) mod order 𝒢) (order 𝒢))) mod order 𝒢)) else 
(nat ((int z' - int z) * (fst (bezw ((e' mod order 𝒢 - e mod order 𝒢) mod order 𝒢) (order 𝒢))) mod order 𝒢)))}"

definition "valid_pub = carrier 𝒢 × carrier 𝒢"

end 

locale chaum_ped_Σ = chaum_ped_Σ_base + cyclic_group 𝒢
begin

lemma g'_in_carrier [simp]: "g' ∈ carrier 𝒢"
  by(simp add: g'_def) 

sublocale chaum_ped_sigma: Σ_protocols_base init response check R S2 ss_adversary challenge_space valid_pub 
  by unfold_locales (auto simp add: R_def valid_pub_def)

lemma completeness: 
  shows "chaum_ped_sigma.completeness"
proof-
  have "g' [^] y ⊗ (g' [^] w') [^] e = g' [^] ((w' * e + y) mod order 𝒢)" for y e w'
    by (simp add: Groups.add_ac(2) pow_carrier_mod nat_pow_pow nat_pow_mult)
  moreover have "❙g [^] y ⊗ (❙g [^] w') [^] e = ❙g [^] ((w' * e + y) mod order 𝒢)" for y e w'
    by (metis add.commute nat_pow_pow nat_pow_mult pow_generator_mod generator_closed mod_mult_right_eq)  
  ultimately show ?thesis
    unfolding chaum_ped_sigma.completeness_def chaum_ped_sigma.completeness_game_def
    by(auto simp add: R_def challenge_space_def init_def check_def response_def split_def bind_spmf_const)
qed

lemma hvzk_xr'_rewrite:
  assumes r: "r < order 𝒢"
  shows "((w*c + r) mod (order 𝒢) mod (order 𝒢) + (order 𝒢) * w*c - w*c) mod (order 𝒢) = r"
(is "?lhs = ?rhs")
proof-
  have "?lhs = (w*c + r  + (order 𝒢) * w*c- w*c) mod (order 𝒢)" 
    by (metis Nat.add_diff_assoc Num.of_nat_simps(1) One_nat_def add_less_same_cancel2 less_imp_le_nat 
        mod_add_left_eq mult.assoc mult_0_right n_less_m_mult_n nat_neq_iff not_add_less2 of_nat_0_le_iff prime_gt_1_nat prime_order) 
  thus ?thesis using r 
    by (metis ab_semigroup_add_class.add_ac(1) ab_semigroup_mult_class.mult_ac(1) diff_add_inverse mod_if mod_mult_self2)
qed

lemma hvzk_h_sub_rewrite:
  assumes "h = ❙g [^] w"  
    and z: "z < order 𝒢" 
  shows "❙g [^] ((z + (order 𝒢)* w * c - w*c)) = ❙g [^] z ⊗ inv (h [^] c)" 
    (is "?lhs = ?rhs")
proof(cases "w = 0")
  case True
  then show ?thesis using assms by simp
next
  case w_gt_0: False
  then show ?thesis 
  proof-
    have "(z + order 𝒢 * w * c - w * c) = (z + (order 𝒢 * w * c- w * c))"
      using z by (simp add: less_imp_le_nat mult_le_mono) 
    then have lhs: "?lhs = ❙g [^] z ⊗ ❙g [^] ((order 𝒢) * w *c - w*c)" 
      by(simp add: nat_pow_mult)
    have " ❙g [^] ((order 𝒢) * w *c - w*c) =  inv (h [^] c)"  
    proof(cases "c = 0")
      case True
      then show ?thesis using lhs by simp
    next
      case False
      hence *: "((order 𝒢)*w *c - w*c) > 0" using assms w_gt_0 
        using gr0I mult_less_cancel2 n_less_m_mult_n numeral_nat(7) prime_gt_1_nat prime_order zero_less_diff by presburger
      then have " ❙g [^] ((order 𝒢)*w*c - w*c) =  ❙g [^] int ((order 𝒢)*w*c - w*c)"
        by (simp add: int_pow_int) 
      also have "... = ❙g [^] int ((order 𝒢)*w*c) ⊗ inv (❙g [^] (w*c))" 
        using int_pow_diff[of "❙g" "order 𝒢 * w * c" "w * c"] * generator_closed int_ops(6) int_pow_neg int_pow_neg_int by presburger

      also have "... = ❙g [^] ((order 𝒢)*w*c) ⊗ inv (❙g [^] (w*c))"
        by (metis int_pow_int) 
      also have "... = ❙g [^] ((order 𝒢)*w*c) ⊗ inv ((❙g [^] w) [^] c)"
        by(simp add: nat_pow_pow)
      also have "... = ❙g [^] ((order 𝒢)*w*c) ⊗ inv (h [^] c)"
        using assms by simp
      also have "... = 𝟭 ⊗ inv (h [^] c)"
        using generator_pow_order
        by (metis generator_closed mult_is_0 nat_pow_0 nat_pow_pow)
      ultimately show ?thesis
        by (simp add: assms(1)) 
    qed
    then show ?thesis using lhs by simp
  qed
qed

lemma hvzk_h_sub2_rewrite:
  assumes  "h' = g' [^] w" 
    and z: "z < order 𝒢" 
  shows "g' [^] ((z + (order 𝒢)*w*c - w*c))  = g' [^] z ⊗ inv (h' [^] c)" 
    (is "?lhs = ?rhs")
proof(cases "w = 0")
  case True
  then show ?thesis 
    using assms by (simp add: g'_def)
next
  case w_gt_0: False
  then show ?thesis 
  proof-
    have "g' = ❙g [^] x" using g'_def by simp
    have g'_carrier: "g' ∈ carrier 𝒢" using g'_def by simp
    have 1: "g' [^] ((order 𝒢)*w*c- w*c) = inv (h' [^] c)"
    proof(cases "c = 0")
      case True
      then show ?thesis by simp
    next
      case False
      hence *: "((order 𝒢)*w*c - w*c) > 0" 
        using assms mult_strict_mono w_gt_0 prime_gt_1_nat prime_order by auto 
      then have " g' [^] ((order 𝒢)*w*c - w*c) = g' [^] (int (order 𝒢 * w * c) - int (w * c))"
        by (metis int_ops(6) int_pow_int of_nat_0_less_iff order.irrefl)
      also have "... = g' [^] ((order 𝒢)*w*c) ⊗ inv (g' [^] (w*c))" 
        by (metis g'_carrier int_pow_diff int_pow_int) 
      also have "... = g' [^] ((order 𝒢)*w*c) ⊗ inv (h' [^] c)"
        by(simp add: nat_pow_pow assms)
      also have "... = 𝟭 ⊗ inv (h' [^] c)" 
        by (metis g'_carrier nat_pow_one nat_pow_pow pow_order_eq_1)
      ultimately show ?thesis
        by (simp add: assms(1)) 
    qed
    have "(z + order 𝒢 * w * c - w * c) = (z + (order 𝒢 * w * c - w * c))"
      using z by (simp add: less_imp_le_nat mult_le_mono) 
    then have lhs: "?lhs = g' [^] z ⊗ g' [^] ((order 𝒢)*w*c - w*c)" 
      by(auto simp add: nat_pow_mult)
    then show ?thesis using 1 by simp
  qed
qed

lemma hv_zk2:
  assumes "(H, w) ∈ R" 
  shows "chaum_ped_sigma.R H w c = chaum_ped_sigma.S H c"
  including monad_normalisation
proof-
  have H: "H = (❙g [^] (w::nat), g' [^] w)" 
    using assms R_def  by(simp add: prod.expand)
  have g'_carrier: "g' ∈ carrier 𝒢" using g'_def by simp
  have "chaum_ped_sigma.R H w c  = do {
    let (h, h') = H;
    r ← sample_uniform (order 𝒢);
    let z = (w*c + r) mod (order 𝒢);
    let a = ❙g [^] ((z + (order 𝒢) * w*c - w*c) mod (order 𝒢)); 
    let a' = g' [^] ((z + (order 𝒢) * w*c - w*c) mod (order 𝒢));
    return_spmf ((a,a'),c, z)}"
    apply(simp add: chaum_ped_sigma.R_def Let_def response_def split_def init_def)
    using assms hvzk_xr'_rewrite 
    by(simp cong: bind_spmf_cong_simp)
  also have "... = do {
    let (h, h') = H;
    z ← map_spmf (λ r. (w*c + r) mod (order 𝒢)) (sample_uniform (order 𝒢));
    let a = ❙g [^] ((z + (order 𝒢) * w*c - w*c) mod (order 𝒢)); 
    let a' = g' [^] ((z + (order 𝒢) * w*c - w*c) mod (order 𝒢));
    return_spmf ((a,a'),c, z)}"
    by(simp add: bind_map_spmf Let_def o_def)
  also have "... = do {
    let (h, h') = H;
    z ← (sample_uniform (order 𝒢));
    let a = ❙g [^] ((z + (order 𝒢) * w*c - w*c) mod (order 𝒢)); 
    let a' = g' [^] ((z + (order 𝒢) * w*c - w*c) mod (order 𝒢));
    return_spmf ((a,a'),c, z)}"
    by(simp add: samp_uni_plus_one_time_pad)
  also have "... = do {
    let (h, h') = H;
    z ← (sample_uniform (order 𝒢));
    let a = ❙g [^] z ⊗ inv (h [^] c); 
    let a' = g' [^] ((z + (order 𝒢) * w*c - w*c) mod (order 𝒢));
    return_spmf ((a,a'),c, z)}"
    using hvzk_h_sub_rewrite assms
    apply(simp add: Let_def H)
    apply(intro bind_spmf_cong[OF refl]; clarsimp?)
    by (simp add: pow_generator_mod)
  also have "... = do {
    let (h, h') = H;
    z ← (sample_uniform (order 𝒢));
    let a = ❙g [^] z ⊗ inv (h [^] c); 
    let a' = g' [^] ((z + (order 𝒢)*w*c - w*c));
    return_spmf ((a,a'),c, z)}"
     using g'_carrier pow_carrier_mod[of "g'"] by simp
   also have "... = do {
    let (h, h') = H;
    z ← (sample_uniform (order 𝒢));
    let a = ❙g [^] z ⊗ inv (h [^] c); 
    let a' =  g' [^] z ⊗ inv (h' [^] c);
    return_spmf ((a,a'),c, z)}"
     using hvzk_h_sub2_rewrite assms H
     by(simp cong: bind_spmf_cong_simp)
   ultimately show ?thesis 
     unfolding chaum_ped_sigma.S_def chaum_ped_sigma.R_def
     by(simp add: init_def S2_def split_def Let_def Σ_protocols_base.S_def bind_map_spmf map_spmf_conv_bind_spmf)
qed

lemma HVZK: 
  shows "chaum_ped_sigma.HVZK"
    unfolding chaum_ped_sigma.HVZK_def 
    by(auto simp add: hv_zk2 R_def valid_pub_def   S2_def check_def cyclic_group_assoc)

lemma ss_rewrite1:
  assumes "fst h ∈ carrier 𝒢"
    and "a ∈ carrier 𝒢" 
    and e: "e < order 𝒢" 
    and "a ⊗ fst h [^] e = ❙g [^] z"  
    and e': "e' < e"
    and "a ⊗ fst h [^] e' = ❙g [^] z'"
  shows "fst h = ❙g [^] ((int z - int z') * inverse (e - e') (order 𝒢) mod int (order 𝒢))"
proof-
  have gcd: "gcd (e - e') (order 𝒢) = 1" 
    using e e' prime_field prime_order by simp
  have "a = ❙g [^] z ⊗ inv (fst h [^] e)" 
    using assms
    by (simp add: assms inv_solve_right)
  moreover have "a = ❙g [^] z' ⊗ inv (fst h [^] e')" 
    using assms
    by (simp add: assms inv_solve_right)
  ultimately have "❙g [^] z ⊗ fst h [^] e' = ❙g [^] z' ⊗ fst h [^] e"
    by (metis (no_types, lifting) assms cyclic_group_assoc cyclic_group_commute nat_pow_closed)
  moreover obtain t :: nat where t: "fst h = ❙g [^] t"
    using assms generatorE by blast
  ultimately have "❙g [^] (z + t * e') = ❙g [^] (z' + t * e)" 
    using nat_pow_pow 
    by (simp add: nat_pow_mult)
  hence "[z + t * e' = z' + t * e] (mod order 𝒢)"
    using group_eq_pow_eq_mod or_gt_0 by blast
  hence "[int z + int t * int e' = int z' + int t * int e] (mod order 𝒢)"
    using cong_int_iff by force
  hence "[int z - int z' = int t * int e - int t * int e'] (mod order 𝒢)"
    by (smt cong_diff_iff_cong_0)
  hence "[int z - int z' = int t * (int e - int e')] (mod order 𝒢)"
    by (simp add: right_diff_distrib)
  hence "[int z - int z' = int t * (e - e')] (mod order 𝒢)" 
    using assms by (simp add: of_nat_diff)
  hence "[(int z - int z') * fst (bezw (e - e') (order 𝒢))  = int t * (e - e') * fst (bezw (e - e') (order 𝒢))] (mod order 𝒢)"
    using cong_scalar_right by blast
  hence "[(int z - int z') * fst (bezw (e - e') (order 𝒢))  = int t * ((e - e') * fst (bezw (e - e') (order 𝒢)))] (mod order 𝒢)" 
    by (simp add: more_arith_simps(11))
  hence "[(int z - int z') * fst (bezw (e - e') (order 𝒢))  = int t * 1] (mod order 𝒢)" 
    by (metis (no_types, opaque_lifting) cong_scalar_left cong_trans inverse gcd)
  hence "[(int z - int z') * fst (bezw (e - e') (order 𝒢)) mod order 𝒢  = t] (mod order 𝒢)" 
    by simp
  hence "[nat ((int z - int z') * fst (bezw (e - e') (order 𝒢)) mod order 𝒢)  = t] (mod order 𝒢)" 
    by (metis cong_def int_ops(9) mod_mod_trivial nat_int)
  hence "❙g [^] (nat ((int z - int z') * fst (bezw (e - e') (order 𝒢)) mod order 𝒢))  = ❙g [^] t" 
    using order_gt_0 order_gt_0_iff_finite pow_generator_eq_iff_cong by blast
  thus ?thesis using t by simp
qed

lemma ss_rewrite2:
  assumes "fst h ∈ carrier 𝒢"
    and "snd h ∈ carrier 𝒢" 
    and "a ∈ carrier 𝒢" 
    and "b ∈ carrier 𝒢"
    and "e < order 𝒢" 
    and "a ⊗ fst h [^] e = ❙g [^] z" 
    and "b ⊗ snd h [^] e = g' [^] z"
    and "e' < e" 
    and "a ⊗ fst h [^] e' = ❙g [^] z'"
    and "b ⊗ snd h [^] e' = g' [^] z'"
  shows "snd h = g' [^] ((int z - int z') * inverse (e - e') (order 𝒢) mod int (order 𝒢))"
proof-
  have gcd: "gcd (e - e') (order 𝒢) = 1" 
    using prime_field assms prime_order by simp
  have "b = g' [^] z ⊗ inv (snd h [^] e)"
    by (simp add: assms inv_solve_right)
  moreover have "b = g' [^] z' ⊗ inv (snd h [^] e')"
    by (metis assms(2) assms(4) assms(10) g'_def generator_closed group.inv_solve_right' group_l_invI l_inv_ex nat_pow_closed)
  ultimately have "g' [^] z ⊗ snd h [^] e' = g' [^] z' ⊗ snd h [^] e" 
    by (metis (no_types, lifting) assms cyclic_group_assoc cyclic_group_commute nat_pow_closed)
  moreover obtain t :: nat where t: "snd h = ❙g [^] t"
    using assms(2) generatorE by blast
  ultimately have "❙g [^] (x * z + t * e') = ❙g [^] (x * z' + t * e)"
    using g'_def nat_pow_pow
    by (simp add: nat_pow_mult) 
  hence "[x * z + t * e' = x * z' + t * e] (mod order 𝒢)"
    using group_eq_pow_eq_mod order_gt_0 by blast
  hence "[int x * int z + int t * int e' = int x * int z' + int t * int e] (mod order 𝒢)"
    by (metis Groups.add_ac(2) Groups.mult_ac(2) cong_int_iff int_ops(7) int_plus)
  hence "[int x * int z - int x * int z' = int t * int e - int t * int e'] (mod order 𝒢)"
    by (smt cong_diff_iff_cong_0)
  hence "[int x * (int z - int z') = int t * (int e - int e')] (mod order 𝒢)"
    by (simp add: int_distrib(4))
  hence "[int x * (int z - int z') = int t * (e - e')] (mod order 𝒢)"
    using assms by (simp add: of_nat_diff)
  hence "[(int x * (int z - int z')) * fst (bezw (e - e') (order 𝒢)) = int t * (e - e') * fst (bezw (e - e') (order 𝒢))] (mod order 𝒢)"
    using cong_scalar_right by blast
  hence "[(int x * (int z - int z')) * fst (bezw (e - e') (order 𝒢)) = int t * ((e - e') * fst (bezw (e - e') (order 𝒢)))] (mod order 𝒢)"
    by (simp add: more_arith_simps(11))
  hence *: "[(int x * (int z - int z')) * fst (bezw (e - e') (order 𝒢)) = int t * 1] (mod order 𝒢)"
    by (metis (no_types, opaque_lifting) cong_scalar_left cong_trans gcd inverse)
  hence "[nat ((int x * (int z - int z')) * fst (bezw (e - e') (order 𝒢)) mod order 𝒢) = t] (mod order 𝒢)"
    by (metis cong_def cong_mod_right more_arith_simps(6) nat_int zmod_int)
  hence "❙g [^] (nat ((int x * (int z - int z')) * fst (bezw (e - e') (order 𝒢)) mod order 𝒢)) = ❙g [^] t"
    using order_gt_0 order_gt_0_iff_finite pow_generator_eq_iff_cong by blast
  thus ?thesis using t 
    by (metis (mono_tags, opaque_lifting) * cong_def g'_def generator_closed int_pow_int int_pow_pow mod_mult_right_eq more_arith_simps(11) more_arith_simps(6) pow_generator_mod_int)
qed

lemma ss_rewrite_snd_h:
  assumes e_e'_mod: "e' mod order 𝒢 < e mod order 𝒢"
    and h_mem: "snd h ∈ carrier 𝒢"
    and a_mem: "snd a ∈ carrier 𝒢"
    and a1: "snd a ⊗ snd h [^] e = g' [^] z" 
    and a2: "snd a ⊗ snd h [^] e' = g' [^] z'" 
  shows "snd h = g' [^] ((int z - int z') * fst (bezw ((e mod order 𝒢 - e' mod order 𝒢) mod order 𝒢) (order 𝒢)) mod int (order 𝒢))"
proof-
  have gcd: "gcd ((e mod order 𝒢 - e' mod order 𝒢) mod order 𝒢) (order 𝒢) = 1"
    using prime_field 
    by (simp add: assms less_imp_diff_less linorder_not_le prime_order)
  have "snd a = g' [^] z ⊗ inv (snd h [^] e)"
    using a1 
    by (metis (no_types, lifting) Group.group.axioms(1) h_mem a_mem group.inv_closed group_l_invI l_inv_ex monoid.m_assoc nat_pow_closed r_inv r_one)
  moreover have "snd a = g' [^] z' ⊗ inv (snd h [^] e')"
    by (metis a2 h_mem a_mem g'_def generator_closed group.inv_solve_right' group_l_invI l_inv_ex nat_pow_closed)
  ultimately have "g' [^] z ⊗ snd h [^] e' = g' [^] z' ⊗ snd h [^] e" 
    by (metis (no_types, lifting) a2 h_mem a_mem a1 cyclic_group_assoc cyclic_group_commute nat_pow_closed)
  moreover obtain t :: nat where t: "snd h = ❙g [^] t"
    using assms(2) generatorE by blast
  ultimately have "❙g [^] (x * z + t * e') = ❙g [^] (x * z' + t * e)"
    using g'_def nat_pow_pow
    by (simp add: nat_pow_mult) 
  hence "[x * z + t * e' = x * z' + t * e] (mod order 𝒢)"
    using group_eq_pow_eq_mod order_gt_0 by blast
  hence "[int x * int z + int t * int e' = int x * int z' + int t * int e] (mod order 𝒢)"
    by (metis Groups.add_ac(2) Groups.mult_ac(2) cong_int_iff int_ops(7) int_plus)
  hence "[int x * int z - int x * int z' = int t * int e - int t * int e'] (mod order 𝒢)"
    by (smt cong_diff_iff_cong_0)
  hence "[int x * (int z - int z') = int t * (int e - int e')] (mod order 𝒢)"
    by (simp add: int_distrib(4))
  hence "[int x * (int z - int z') = int t * (int e mod order 𝒢 - int e' mod order 𝒢) mod order 𝒢] (mod order 𝒢)"
    by (metis (no_types, lifting) cong_def mod_diff_eq mod_mod_trivial mod_mult_right_eq)
  hence *: "[int x * (int z - int z') = int t * (e mod order 𝒢 - e' mod order 𝒢) mod order 𝒢] (mod order 𝒢)"
    by (simp add: assms(1) int_ops(9) less_imp_le_nat of_nat_diff)
  hence "[int x * (int z - int z') * fst (bezw ((e mod order 𝒢 - e' mod order 𝒢) mod order 𝒢) (order 𝒢)) 
               = int t * ((e mod order 𝒢 - e' mod order 𝒢) mod order 𝒢 
                  * fst (bezw ((e mod order 𝒢 - e' mod order 𝒢) mod order 𝒢) (order 𝒢)))] (mod order 𝒢)"
    by (metis (no_types, lifting) cong_mod_right cong_scalar_right less_imp_diff_less mod_if more_arith_simps(11) or_gt_0 unique_euclidean_semiring_numeral_class.pos_mod_bound)
  hence "[int x * (int z - int z') * fst (bezw ((e mod order 𝒢 - e' mod order 𝒢) mod order 𝒢) (order 𝒢)) 
               = int t * 1] (mod order 𝒢)"
    by (meson Number_Theory_Aux.inverse * gcd cong_scalar_left cong_trans)
  hence "❙g [^] (int x * (int z - int z') * fst (bezw ((e mod order 𝒢 - e' mod order 𝒢) mod order 𝒢) (order 𝒢))) = ❙g [^] t"
    by (metis cong_def int_pow_int more_arith_simps(6) pow_generator_mod_int)
  thus ?thesis using t 
    by (metis (mono_tags, opaque_lifting) g'_def generator_closed int_pow_int int_pow_pow mod_mult_right_eq more_arith_simps(11) pow_generator_mod_int)
qed

lemma special_soundness:
  shows "chaum_ped_sigma.special_soundness"
  unfolding chaum_ped_sigma.special_soundness_def 
  apply(auto simp add: challenge_space_def check_def ss_adversary_def R_def valid_pub_def)
  using ss_rewrite2 ss_rewrite1 by auto

theorem Σ_protocol:  "chaum_ped_sigma.Σ_protocol"
  by(simp add: chaum_ped_sigma.Σ_protocol_def completeness HVZK special_soundness)

sublocale chaum_ped_Σ_commit: Σ_protocols_to_commitments init response check R S2 ss_adversary challenge_space valid_pub G
  apply unfold_locales
      apply(auto simp add: Σ_protocol lossless_init lossless_response lossless_G)
  by(simp add: R_def G_def)

sublocale dis_log: dis_log 𝒢 
  unfolding dis_log_def by simp

sublocale dis_log_alt: dis_log_alt 𝒢 x 
  unfolding dis_log_alt_def by simp

lemma reduction_to_dis_log: 
  shows "chaum_ped_Σ_commit.rel_advantage 𝒜 = dis_log.advantage (dis_log_alt.adversary3 𝒜)"
proof-
  have "chaum_ped_Σ_commit.rel_game 𝒜 = TRY do {
    w ← sample_uniform (order 𝒢);
    let (h,w) = ((❙g [^] w, g' [^] w), w);
    w' ← 𝒜 h;
    return_spmf ((fst h = ❙g [^] w' ∧ snd h = g' [^] w'))} ELSE return_spmf False"
    unfolding chaum_ped_Σ_commit.rel_game_def 
    by(simp add:  G_def R_def)
  also have "... = TRY do {    
    w ← sample_uniform (order 𝒢);
    let (h,w) = ((❙g [^] w, g' [^] w), w);
    w' ← 𝒜 h;
    return_spmf ([w = w'] (mod (order 𝒢)) ∧ [x*w = x*w'] (mod order 𝒢))} ELSE return_spmf False"
    apply(intro try_spmf_cong bind_spmf_cong[OF refl]; simp add: dis_log_alt.dis_log3_def dis_log_alt.g'_def g'_def)
    by (simp add: finite_carrier nat_pow_pow pow_generator_eq_iff_cong)
  also have "... = dis_log_alt.dis_log3 𝒜"
    apply(auto simp add:  dis_log_alt.dis_log3_def dis_log_alt.g'_def g'_def)
    by(intro try_spmf_cong  bind_spmf_cong[OF refl]; clarsimp?; auto simp add: cong_scalar_left)
  ultimately have "chaum_ped_Σ_commit.rel_advantage 𝒜 = dis_log_alt.advantage3 𝒜"
    by(simp add: chaum_ped_Σ_commit.rel_advantage_def dis_log_alt.advantage3_def)
  thus ?thesis
    by (simp add: dis_log_alt_reductions.dis_log_adv3 cyclic_group_axioms dis_log_alt.dis_log_alt_axioms dis_log_alt_reductions.intro)
qed

lemma commitment_correct: "chaum_ped_Σ_commit.abstract_com.correct"
  by(simp add: chaum_ped_Σ_commit.commit_correct)

lemma  "chaum_ped_Σ_commit.abstract_com.perfect_hiding_ind_cpa 𝒜"
  using chaum_ped_Σ_commit.perfect_hiding by blast

lemma binding: "chaum_ped_Σ_commit.abstract_com.bind_advantage 𝒜 ≤ dis_log.advantage (dis_log_alt.adversary3 ((chaum_ped_Σ_commit.adversary 𝒜)))"
  using chaum_ped_Σ_commit.bind_advantage reduction_to_dis_log by simp

end

locale chaum_ped_asymp = 
  fixes 𝒢 :: "nat ⇒ 'grp cyclic_group"
    and x :: nat
  assumes cp_Σ: "⋀η. chaum_ped_Σ (𝒢 η)"
begin

sublocale chaum_ped_Σ "𝒢 η" for η 
  by(simp add: cp_Σ)

text‹The ‹Σ›-protocol statement comes easily in the asympotic setting.›

theorem sigma_protocol:
  shows "chaum_ped_sigma.Σ_protocol n"
  by(simp add: Σ_protocol)

text‹We now show the statements of security for the commitment scheme in the asymptotic setting, the main difference is that
we are able to show the binding advantage is negligible in the security parameter.›

lemma asymp_correct: "chaum_ped_Σ_commit.abstract_com.correct n" 
  using  chaum_ped_Σ_commit.commit_correct by simp

lemma asymp_perfect_hiding: "chaum_ped_Σ_commit.abstract_com.perfect_hiding_ind_cpa n (𝒜 n)"
  using chaum_ped_Σ_commit.perfect_hiding by blast

lemma asymp_computational_binding: 
  assumes "negligible (λ n. dis_log.advantage n (dis_log_alt.adversary3 n ((chaum_ped_Σ_commit.adversary n (𝒜 n)))))"
  shows "negligible (λ n. chaum_ped_Σ_commit.abstract_com.bind_advantage n (𝒜 n))"
  using chaum_ped_Σ_commit.bind_advantage assms chaum_ped_Σ_commit.abstract_com.bind_advantage_def negligible_le binding by auto

end

end