Theory Okamoto_Sigma_Commit

subsection‹Okamoto ‹Σ›-protocol›

theory Okamoto_Sigma_Commit imports
  Commitment_Schemes
  Sigma_Protocols
  Cyclic_Group_Ext
  Discrete_Log
  "HOL.GCD"
  Number_Theory_Aux
  Uniform_Sampling 
begin 

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

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

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

lemma order_gt_0 [simp]:"order 𝒢 > 0" 
  using order_gt_1 by simp

definition "response r w e = do {
  let (r1,r2) = r;
  let (x1,x2) = w;
  let z1 = (e * x1 + r1) mod (order 𝒢);
  let z2 = (e * x2 + r2) mod (order 𝒢);
  return_spmf ((z1,z2))}"

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

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

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

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

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

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

definition G :: "('grp pub_in × witness) spmf"
  where "G = do {
    w1 ← sample_uniform (order 𝒢);
    w2 ← sample_uniform (order 𝒢);
    return_spmf (❙g [^] w1 ⊗ g' [^] w2 , (w1,w2))}"

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

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

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

definition R2 :: "'grp pub_in ⇒ witness ⇒ challenge ⇒ ('grp msg, challenge, response) conv_tuple spmf"
  where "R2 h w c = do { 
    let (x1,x2) = w; 
    r1 ← sample_uniform (order 𝒢);
    r2 ← sample_uniform (order 𝒢);
    let z1 = (c * x1 + r1) mod (order 𝒢);
    let z2 = (c * x2 + r2) mod (order 𝒢);
    return_spmf (❙g [^] r1 ⊗ g' [^] r2 ,c,(z1,z2))}"

definition ss_adversary :: "'grp ⇒ ('grp msg, challenge, response) conv_tuple ⇒ ('grp msg, challenge, response) conv_tuple ⇒ (nat × nat) spmf"
  where "ss_adversary y c1 c2 = do {
    let (a, e, (z1,z2)) = c1;
    let (a', e', (z1',z2')) = c2;
    return_spmf (if (e > e') then (nat ((int z1 - int z1') * inverse (e - e') (order 𝒢) mod order 𝒢)) else 
                      (nat ((int z1' - int z1) * inverse (e' - e) (order 𝒢) mod order 𝒢)), 
                 if (e > e') then (nat ((int z2  - int z2') * inverse (e - e') (order 𝒢) mod order 𝒢)) else 
                      (nat ((int z2' - int z2) * inverse (e' - e) (order 𝒢) mod order 𝒢)))}"

definition "valid_pub = carrier 𝒢"
end

locale okamoto = okamoto_base + cyclic_group 𝒢
begin

lemma g'_in_carrier [simp]: "g' ∈ carrier 𝒢" 
  using g'_def by auto

sublocale Σ_protocols_base: Σ_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 "Σ_protocols_base.R h w c = R2 h w c"
  by(simp add: Σ_protocols_base.R_def R2_def; simp add: init_def split_def response_def)

lemma completeness: 
  shows "Σ_protocols_base.completeness"
proof-
  have "(❙g [^] ((e * fst w' + y) mod order 𝒢) ⊗ g' [^] ((e * snd w' + ya) mod order 𝒢) = ❙g [^] y ⊗ g' [^] ya ⊗ (❙g [^] fst w' ⊗ g' [^] snd w') [^] e)" 
    for e y ya :: nat and w' :: "nat × nat"
  proof-
    have "❙g [^] ((e * fst w' + y) mod order 𝒢) ⊗ g' [^] ((e * snd w' + ya) mod order 𝒢) = ❙g [^] ((y + e * fst w')) ⊗ g' [^] ((ya + e * snd w'))"
      by (simp add: cyclic_group.pow_carrier_mod cyclic_group_axioms g'_def add.commute pow_generator_mod)
    also have "... = ❙g [^] y ⊗ ❙g [^] (e * fst w') ⊗ g' [^] ya ⊗ g' [^] (e * snd w')" 
      by (simp add: g'_def m_assoc nat_pow_mult)
    also have "... = ❙g [^] y ⊗ g' [^] ya ⊗ ❙g [^] (e * fst w') ⊗ g' [^] (e * snd w')" 
      by (smt add.commute g'_def generator_closed m_assoc nat_pow_closed nat_pow_mult nat_pow_pow)
    also have "... = ❙g [^] y ⊗ g' [^] ya ⊗ ((❙g [^] fst w') [^] e ⊗ (g' [^] snd w') [^] e)" 
      by (simp add: m_assoc mult.commute nat_pow_pow)
    also have "... =  ❙g [^] y ⊗ g' [^] ya ⊗ ((❙g [^] fst w' ⊗ g' [^] snd w') [^] e)"   
      by (smt power_distrib g'_def generator_closed mult.commute nat_pow_closed nat_pow_mult nat_pow_pow)
    ultimately show ?thesis by simp
  qed
  thus ?thesis 
  unfolding Σ_protocols_base.completeness_def Σ_protocols_base.completeness_game_def
  by(simp add: R_def challenge_space_def init_def check_def response_def split_def bind_spmf_const)
qed

lemma hvzk_z_r:
  assumes r1: "r1 < order 𝒢" 
  shows "r1 = ((r1 + c * (x1 :: nat)) mod (order 𝒢) + order 𝒢 * c * x1 - c * x1) mod (order 𝒢)"
proof(cases "x1 = 0")
  case True
  then show ?thesis using r1 by simp
next
  case x1_neq_0: False
  have z1_eq: "[(r1 + c * x1) mod (order 𝒢) + order 𝒢 * c * x1 = r1 + c * x1] (mod (order 𝒢))"
    using gr_implies_not_zero order_gt_1
    by (simp add: Groups.mult_ac(1) cong_def)
  hence "[(r1 + c * x1) mod (order 𝒢) + order 𝒢 * c * x1 - c * x1 = r1] (mod (order 𝒢))" 
  proof(cases "c = 0")
    case True
    then show ?thesis 
      using z1_eq by auto
  next
    case False
    have "order 𝒢 * c * x1 - c * x1 > 0" using x1_neq_0 False 
      using prime_gt_1_nat prime_order by auto 
    thus ?thesis 
      by (smt Groups.add_ac(2) add_diff_inverse_nat cong_add_lcancel_nat diff_is_0_eq le_simps(1) neq0_conv trans_less_add2 z1_eq zero_less_diff)
  qed
  thus ?thesis 
    by (simp add: r1 cong_def)
qed

lemma hvzk_z1_r1_tuple_rewrite: 
  assumes r1: "r1 < order 𝒢" 
  shows "(❙g [^] r1 ⊗ g' [^] r2, c, (r1 + c * x1) mod order 𝒢, (r2 + c * x2) mod order 𝒢) = 
              (❙g [^] (((r1 + c * x1) mod order 𝒢 + order 𝒢 * c * x1 - c * x1) mod order 𝒢)  
                  ⊗ g' [^] r2, c, (r1 + c * x1) mod order 𝒢, (r2 + c * x2) mod order 𝒢)"
proof-
  have "❙g [^] r1 = ❙g [^] (((r1 + c * x1) mod order 𝒢 + order 𝒢 * c * x1 - c * x1) mod order 𝒢)"
    using assms hvzk_z_r by simp
  thus ?thesis by argo
qed

lemma hvzk_z2_r2_tuple_rewrite: 
  assumes "xb < order 𝒢" 
  shows "(❙g [^] (((x' + xa * x1) mod order 𝒢 + order 𝒢 * xa * x1 - xa * x1) mod order 𝒢) 
            ⊗ g' [^] xb, xa, (x' + xa * x1) mod order 𝒢, (xb + xa * x2) mod order 𝒢) =
               (❙g [^] (((x' + xa * x1) mod order 𝒢 + order 𝒢 * xa * x1 - xa * x1) mod order 𝒢) 
                ⊗ g' [^] (((xb + xa * x2) mod order 𝒢 + order 𝒢 * xa * x2 - xa * x2) mod order 𝒢), xa, (x' + xa * x1) mod order 𝒢, (xb + xa * x2) mod order 𝒢)"
proof-
  have "g' [^] xb = g' [^] (((xb + xa * x2) mod order 𝒢 + order 𝒢 * xa * x2 - xa * x2) mod order 𝒢)"
    using hvzk_z_r assms by simp
    thus ?thesis by argo
qed

lemma hvzk_sim_inverse_rewrite: 
  assumes h: "h =  ❙g [^] (x1 :: nat) ⊗ g' [^] (x2 :: nat)"
  shows "❙g [^] (((z1::nat) + order 𝒢 * c * x1 - c * x1) mod (order 𝒢)) 
            ⊗ g' [^] (((z2::nat) + order 𝒢 * c * x2 - c * x2) mod (order 𝒢))
                = (❙g [^] z1 ⊗ g' [^] z2) ⊗ (inv h [^] c)"
(is "?lhs = ?rhs")
proof-
  have in_carrier1: "(g' [^] x2) [^] c ∈ carrier 𝒢" by simp 
  have in_carrier2: "(❙g [^] x1) [^] c ∈ carrier 𝒢" by simp
  have pow_distrib1: "order 𝒢 * c * x1 - c * x1 = (order 𝒢 - 1) * c * x1" 
    and pow_distrib2: "order 𝒢 * c * x2 - c * x2 = (order 𝒢 - 1) * c * x2" 
    using assms by (simp add: diff_mult_distrib)+
  have "?lhs = ❙g [^] (z1 + order 𝒢 * c * x1 - c * x1) ⊗ g' [^] (z2 + order 𝒢 * c  * x2 - c * x2)"
    by (simp add: pow_carrier_mod)
  also have "... = ❙g [^] (z1 + (order 𝒢 * c * x1 - c * x1)) ⊗ g' [^] (z2 + (order 𝒢 * c * x2 - c * x2))" 
    using h 
    by (smt Nat.add_diff_assoc diff_zero le_simps(1) nat_0_less_mult_iff neq0_conv pow_distrib1 pow_distrib2 prime_gt_1_nat prime_order zero_less_diff)
  also have "... =  ❙g [^] z1 ⊗ ❙g [^] (order 𝒢 * c * x1 - c * x1) ⊗ g' [^] z2 ⊗ g' [^] (order 𝒢 * c * x2 - c * x2)"
    using nat_pow_mult 
    by (simp add: m_assoc) 
  also have "... = ❙g [^] z1 ⊗ g' [^] z2 ⊗ ❙g [^] (order 𝒢 * c * x1 - c * x1) ⊗ g' [^] (order 𝒢 * c * x2 - c * x2)"
    by (smt add.commute g'_def generator_closed m_assoc nat_pow_closed nat_pow_mult nat_pow_pow)
  also have "... = ❙g [^] z1 ⊗ g' [^] z2 ⊗ ❙g [^] ((order 𝒢 - 1) * c * x1) ⊗ g' [^] ((order 𝒢 - 1) * c * x2)" 
    using pow_distrib1 pow_distrib2 by argo
  also have "... = ❙g [^] z1 ⊗ g' [^] z2 ⊗ (❙g [^] (order 𝒢 - 1)) [^] (c * x1) ⊗ (g' [^] ((order 𝒢 - 1))) [^] (c * x2)" 
    by (simp add: more_arith_simps(11) nat_pow_pow)
  also have "... = ❙g [^] z1 ⊗ g' [^] z2 ⊗ (inv (❙g [^] c)) [^] x1 ⊗ (inv (g' [^] c)) [^] x2"
    using assms neg_power_inverse  inverse_pow_pow nat_pow_pow prime_gt_1_nat prime_order by auto
  also have "... = ❙g [^] z1 ⊗ g' [^] z2 ⊗ (inv ((❙g [^] c) [^] x1)) ⊗ (inv ((g' [^] c) [^] x2))" 
    by (simp add: inverse_pow_pow)
  also have "... = ❙g [^] z1 ⊗ g' [^] z2 ⊗ ((inv ((❙g [^] x1) [^] c)) ⊗ (inv ((g' [^] x2) [^] c)))" 
    by (simp add: mult.commute cyclic_group_assoc nat_pow_pow)
  also have "... = ❙g [^] z1 ⊗ g' [^] z2 ⊗ inv ((❙g [^] x1) [^] c ⊗ (g' [^] x2) [^] c)"
    using inverse_split in_carrier2 in_carrier1 by simp
  also have "... = ❙g [^] z1 ⊗ g' [^] z2 ⊗ inv (h [^] c)" 
    using h  cyclic_group_commute monoid_comm_monoidI 
    by (simp add: pow_mult_distrib)
  ultimately show ?thesis 
    by (simp add: h inverse_pow_pow)
qed

lemma hv_zk: 
  assumes "h =  ❙g [^] x1 ⊗ g' [^] x2"
  shows "Σ_protocols_base.R h (x1,x2) c = Σ_protocols_base.S h c"
  including monad_normalisation
proof-
  have "Σ_protocols_base.R h (x1,x2) c = do { 
    r1 ← sample_uniform (order 𝒢);
    r2 ← sample_uniform (order 𝒢);
    let z1 = (r1 + c * x1) mod (order 𝒢);
    let z2 = (r2 + c * x2) mod (order 𝒢);
    return_spmf ( ❙g [^] r1 ⊗ g' [^] r2 ,c,(z1,z2))}"
      by(simp add: Σ_protocols_base.R_def R2_def; simp add: add.commute init_def split_def response_def)
    also have "... = do { 
    r2 ← sample_uniform (order 𝒢);
    z1 ← map_spmf (λ r1. (r1 + c * x1) mod (order 𝒢)) (sample_uniform (order 𝒢));
    let z2 = (r2 + c * x2) mod (order 𝒢);
    return_spmf (❙g [^] ((z1 + order 𝒢 * c * x1 - c * x1) mod (order 𝒢)) ⊗ g' [^] r2 ,c,(z1,z2))}"
      by(simp add: bind_map_spmf o_def Let_def hvzk_z1_r1_tuple_rewrite assms cong: bind_spmf_cong_simp)
  also have "... = do { 
    z1 ← map_spmf (λ r1. (r1 + c * x1) mod (order 𝒢)) (sample_uniform (order 𝒢));
    z2 ← map_spmf (λ r2. (r2 + c * x2) mod (order 𝒢)) (sample_uniform (order 𝒢));
    return_spmf (❙g [^] ((z1 + order 𝒢 * c * x1 - c * x1) mod (order 𝒢)) ⊗ g' [^] ((z2 + order 𝒢 * c * x2 - c * x2) mod (order 𝒢)) ,c,(z1,z2))}"
    by(simp add: bind_map_spmf o_def Let_def hvzk_z2_r2_tuple_rewrite cong: bind_spmf_cong_simp)
  also have "... = do { 
    z1 ← map_spmf (λ r1. (c * x1 + r1) mod (order 𝒢)) (sample_uniform (order 𝒢));
    z2 ← map_spmf (λ r2. (c * x2 + r2) mod (order 𝒢)) (sample_uniform (order 𝒢));
    return_spmf (❙g [^] ((z1 + order 𝒢 * c * x1 - c * x1) mod (order 𝒢)) ⊗ g' [^] ((z2 + order 𝒢 * c * x2 - c * x2) mod (order 𝒢)) ,c,(z1,z2))}"
    by(simp add: add.commute)
  also have "... = do { 
    z1 ← (sample_uniform (order 𝒢));
    z2 ← (sample_uniform (order 𝒢));
    return_spmf (❙g [^] ((z1 + order 𝒢 * c * x1 - c * x1) mod (order 𝒢)) ⊗ g' [^] ((z2 + order 𝒢 * c * x2 - c * x2) mod (order 𝒢)) ,c,(z1,z2))}"
      by(simp add: samp_uni_plus_one_time_pad)
  also have "... = do { 
    z1 ← (sample_uniform (order 𝒢));
    z2 ← (sample_uniform (order 𝒢));
    return_spmf ((❙g [^] z1 ⊗ g' [^] z2) ⊗ (inv h [^] c) ,c,(z1,z2))}"
      by(simp add: hvzk_sim_inverse_rewrite assms cong: bind_spmf_cong_simp) 
  ultimately show ?thesis 
    by(simp add: Σ_protocols_base.S_def S2_def bind_map_spmf map_spmf_conv_bind_spmf)
qed

lemma HVZK: 
  shows "Σ_protocols_base.HVZK"
  unfolding Σ_protocols_base.HVZK_def 
  apply(auto simp add: R_def challenge_space_def hv_zk S2_def check_def valid_pub_def)
  by (metis (no_types, lifting) cyclic_group_commute g'_in_carrier generator_closed inv_closed inv_solve_left inverse_pow_pow m_closed nat_pow_closed)

lemma ss_rewrite:
  assumes "h ∈ carrier 𝒢"
    and "a ∈ carrier 𝒢"
    and "e < order 𝒢" 
    and "❙g [^] z1 ⊗ g' [^] z1' = a ⊗ h [^] e"
    and "e' < e"
    and "❙g [^] z2 ⊗ g' [^] z2' = a ⊗ h [^] e' "
  shows "h = ❙g [^] ((int z1 - int z2) * fst (bezw (e - e') (order 𝒢)) mod int (order 𝒢)) ⊗ g' [^] ((int z1' - int z2') * fst (bezw (e - e') (order 𝒢)) mod int (order 𝒢))"
proof-
  have gcd: "gcd (e - e') (order 𝒢) = 1"
    using prime_field assms prime_order by simp 
  have "❙g [^] z1 ⊗ g' [^] z1' ⊗ inv (h [^] e) = a" 
    by (simp add: inv_solve_right' assms)
  moreover have "❙g [^] z2 ⊗ g' [^] z2' ⊗ inv (h [^] e') = a" 
    by (simp add: assms inv_solve_right')
  ultimately have "❙g [^] z2 ⊗ g' [^] z2' ⊗ inv (h [^] e') = ❙g [^] z1 ⊗ g' [^] z1' ⊗ inv (h [^] e)"
    using g'_def by (simp add: nat_pow_pow)
  moreover obtain t :: nat where t: "h = ❙g [^] t" 
    using assms generatorE by blast
  ultimately have "❙g [^] z2 ⊗ ❙g [^] (x * z2') ⊗ ❙g [^] (t * e) = ❙g [^] z1 ⊗ ❙g [^] (x * z1') ⊗ (❙g [^] (t * e'))" 
    using assms(2) assms(4) cyclic_group_commute m_assoc g'_def nat_pow_pow by auto
  hence "❙g [^] (z2 + x * z2' + t * e) = ❙g [^] (z1 + x * z1' + t * e')"  
    by (simp add: nat_pow_mult)
  hence "[z2 + x * z2' + t * e = z1 + x * z1' + t * e'] (mod order 𝒢)"
    using group_eq_pow_eq_mod order_gt_0 by blast
  hence "[int z2 + int x * int z2' + int t * int e = int z1 + int x * int z1' + int t * int e'] (mod order 𝒢)"
    using cong_int_iff by force
  hence "[int z1 + int x * int z1' - int z2 - int x * int z2' = int t * int e - int t * int e'] (mod order 𝒢)"
    by (smt cong_diff_iff_cong_0 cong_sym)
  hence "[int z1 + int x * int z1' - int z2 - int x * int z2' = int t * (e - e')] (mod order 𝒢)"
    using int_distrib(4) assms by (simp add: of_nat_diff)
  hence "[(int z1 + int x * int z1' - int z2 - int x * int z2') * fst (bezw (e - e') (order 𝒢)) = int t * (e - e') * fst (bezw (e - e') (order 𝒢))] (mod order 𝒢)"
    using cong_scalar_right by blast
  hence "[(int z1 + int x * int z1' - int z2 - int x * int z2') * fst (bezw (e - e') (order 𝒢)) = int t * ((e - e') * fst (bezw (e - e') (order 𝒢)))] (mod order 𝒢)"
    by (simp add: mult.assoc)
  hence "[(int z1 + int x * int z1' - int z2 - int x * int z2') * 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 z1 - int z2 + int x * int z1' - int x * int z2') * fst (bezw (e - e') (order 𝒢)) = int t] (mod order 𝒢)"
    by smt
  hence "[(int z1 - int z2 + int x * (int z1' - int z2')) * fst (bezw (e - e') (order 𝒢)) = int t] (mod order 𝒢)"
    by (simp add: Rings.ring_distribs(4) add_diff_eq)
  hence "[nat ((int z1 - int z2 + int x * (int z1' - int z2')) * fst (bezw (e - e') (order 𝒢)) mod (order 𝒢)) = int t] (mod order 𝒢)"
    by auto
  hence "❙g [^] (nat ((int z1 - int z2 + int x * (int z1' - int z2')) * fst (bezw (e - e') (order 𝒢)) mod (order 𝒢))) = ❙g [^] t"
    using cong_int_iff finite_carrier pow_generator_eq_iff_cong by blast
  hence "❙g [^] ((int z1 - int z2 + int x * (int z1' - int z2')) * fst (bezw (e - e') (order 𝒢))) = ❙g [^] t"
    using pow_generator_mod_int by auto
  hence "❙g [^] ((int z1 - int z2) * fst (bezw (e - e') (order 𝒢)) + int x * (int z1' - int z2') * fst (bezw (e - e') (order 𝒢))) = ❙g [^] t"
    by (metis Rings.ring_distribs(2) t)
  hence "❙g [^] ((int z1 - int z2) * fst (bezw (e - e') (order 𝒢))) ⊗ ❙g [^] (int x * (int z1' - int z2') * fst (bezw (e - e') (order 𝒢))) = ❙g [^] t"
    using int_pow_mult by auto
  thus ?thesis 
    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 t)
qed

lemma 
  assumes h_mem: "h ∈ carrier 𝒢" 
    and a_mem: "a ∈ carrier 𝒢" 
    and a: "❙g [^] fst z ⊗ g' [^] snd z = a ⊗ h [^] e"
    and a': "❙g [^] fst z' ⊗ g' [^] snd z' = a ⊗ h [^] e'"
    and e_e'_mod: "e' mod order 𝒢 < e mod order 𝒢"
  shows "h = ❙g [^] ((int (fst z) - int (fst z')) * fst (bezw ((e mod order 𝒢 - e' mod order 𝒢) mod order 𝒢) (order 𝒢)) mod int (order 𝒢)) 
              ⊗ g' [^] ((int (snd z) - int (snd 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 "❙g [^] fst z ⊗ g' [^] snd z ⊗ inv (h [^] e) = a" 
    using a h_mem a_mem by (simp add: inv_solve_right')
  moreover have "❙g [^] fst z' ⊗ g' [^] snd z' ⊗ inv (h [^] e') = a" 
    using a h_mem a_mem by (simp add: assms(4) inv_solve_right')
  ultimately have "❙g [^] fst z ⊗ ❙g [^] (x * snd z) ⊗ inv (h [^] e) = ❙g [^] fst z' ⊗ ❙g [^] (x * snd z') ⊗ inv (h [^] e')"
    using g'_def by (simp add: nat_pow_pow)
  moreover obtain t :: nat where t: "h = ❙g [^] t" 
    using h_mem generatorE by blast
  ultimately have "❙g [^] fst z ⊗ ❙g [^] (x * snd z) ⊗ ❙g [^] (t * e') = ❙g [^] fst z' ⊗ ❙g [^] (x * snd z') ⊗ ❙g [^] (t * e)"
    using a_mem assms(3) assms(4) cyclic_group_assoc cyclic_group_commute g'_def nat_pow_pow by auto
  hence "❙g [^] (fst z + x * snd z + t * e') = ❙g [^] (fst z' + x * snd z' + t * e)"
    by (simp add: nat_pow_mult)
  hence "[fst z + x * snd z + t * e' = fst z' + x * snd z' + t * e] (mod order 𝒢)"
    using group_eq_pow_eq_mod order_gt_0 by blast
  hence "[int (fst z) + int x * int (snd z) + int t * int e' = int (fst z') + int x * int (snd z') + int t * int e] (mod order 𝒢)"
    using cong_int_iff by force
  hence "[int (fst z) - int (fst z') + int x * int (snd z) - int x * int (snd z') =  int t * int e - int t  * int e'] (mod order 𝒢)"
    by (smt cong_diff_iff_cong_0)
  hence "[int (fst z) - int (fst z') + int x * (int (snd z) - int (snd z')) =  int t * (int e -  int e')] (mod order 𝒢)"
  proof -
    have "[int (fst z) + (int (x * snd z) - (int (fst z') + int (x * snd z'))) = int t * (int e - int e')] (mod int (order 𝒢))"
      by (simp add: Rings.ring_distribs(4) ‹[int (fst z) - int (fst z') + int x * int (snd z) - int x * int (snd z') = int t * int e - int t * int e'] (mod int (order 𝒢))› add_diff_add add_diff_eq)
    then have "∃i. [int (fst z) + (int x * int (snd z) - (int (fst z') + i * int (snd z'))) = int t * (int e - int e') + int (snd z') * (int x - i)] (mod int (order 𝒢))"
      by (metis (no_types) add.commute arith_simps(49) cancel_comm_monoid_add_class.diff_cancel int_ops(7) mult_eq_0_iff)
    then have "∃i. [int (fst z) - int (fst z') + (int x * (int (snd z) - int (snd z')) + i) = int t * (int e - int e') + i] (mod int (order 𝒢))"
      by (metis (no_types) add_diff_add add_diff_eq mult_diff_mult mult_of_nat_commute)
    then show ?thesis
      by (metis (no_types) add.assoc cong_add_rcancel)
  qed
  hence "[int (fst z) - int (fst z') + int x * (int (snd z) - int (snd z')) =  int t * (int e mod order 𝒢 - int e' mod order 𝒢) mod order 𝒢] (mod order 𝒢)"
    by (metis (mono_tags, lifting) cong_def mod_diff_eq mod_mod_trivial mod_mult_right_eq)
  hence "[int (fst z) - int (fst z') + int x * (int (snd z) - int (snd z')) =  int t * (e mod order 𝒢 - e' mod order 𝒢) mod order 𝒢] (mod order 𝒢)"
    using e_e'_mod 
    by (simp add: int_ops(9) of_nat_diff)
  hence "[(int (fst z) - int (fst z') + int x * (int (snd z) - int (snd z'))) 
            * fst (bezw ((e mod order 𝒢 - e' mod order 𝒢) mod order 𝒢) (order 𝒢)) mod order 𝒢 
               =  int t * (e mod order 𝒢 - e' mod order 𝒢) mod order 𝒢 
                  * fst (bezw ((e mod order 𝒢 - e' mod order 𝒢) mod order 𝒢) (order 𝒢)) mod order 𝒢] (mod order 𝒢)"
    using cong_cong_mod_int cong_scalar_right by blast
  hence "[(int (fst z) - int (fst z') + int x * (int (snd z) - int (snd z'))) 
            * fst (bezw ((e mod order 𝒢 - e' mod order 𝒢) mod order 𝒢) (order 𝒢)) mod order 𝒢 
               =  int t * ((e mod order 𝒢 - e' mod order 𝒢) mod order 𝒢 
                  * fst (bezw ((e mod order 𝒢 - e' mod order 𝒢) mod order 𝒢) (order 𝒢)) mod order 𝒢)] (mod order 𝒢)"
    by (metis (no_types, lifting) Groups.mult_ac(1) cong_mod_right less_imp_diff_less mod_less mod_mult_left_eq mod_mult_right_eq order_gt_0 unique_euclidean_semiring_numeral_class.pos_mod_bound)
  hence "[(int (fst z) - int (fst z') + int x * (int (snd z) - int (snd z'))) 
            * fst (bezw ((e mod order 𝒢 - e' mod order 𝒢) mod order 𝒢) (order 𝒢)) mod order 𝒢 
               =  int t * 1] (mod order 𝒢)"
    using inverse gcd 
    by (smt Num.of_nat_simps(5) Number_Theory_Aux.inverse cong_def mod_mult_right_eq more_arith_simps(6) of_nat_1)
  hence "[((int (fst z) - int (fst z')) + (int x * (int (snd z) - int (snd z')))) 
            * fst (bezw ((e mod order 𝒢 - e' mod order 𝒢) mod order 𝒢) (order 𝒢)) mod order 𝒢 
               = int t] (mod order 𝒢)"
    by auto
  hence "[(int (fst z) - int (fst z')) * (fst (bezw ((e mod order 𝒢 - e' mod order 𝒢) mod order 𝒢) (order 𝒢)) mod order 𝒢) + (int x * (int (snd z) - int (snd z'))) 
            * (fst (bezw ((e mod order 𝒢 - e' mod order 𝒢) mod order 𝒢) (order 𝒢)) mod order 𝒢) 
               = int t] (mod order 𝒢)"
    by (metis (no_types, opaque_lifting) cong_mod_left distrib_right mod_mult_right_eq)
  hence "[(int (fst z) - int (fst z')) * fst (bezw ((e mod order 𝒢 - e' mod order 𝒢) mod order 𝒢) (order 𝒢)) mod order 𝒢 + (int x * (int (snd z) - int (snd z'))) 
            * (fst (bezw ((e mod order 𝒢 - e' mod order 𝒢) mod order 𝒢) (order 𝒢)) mod order 𝒢) 
               = t] (mod order 𝒢)"
  proof -
    have "[(int (fst z) - int (fst z')) * fst (bezw ((e mod order 𝒢 - e' mod order 𝒢) mod order 𝒢) (order 𝒢)) = (int (fst z) - int (fst z')) * (fst (bezw ((e mod order 𝒢 - e' mod order 𝒢) mod order 𝒢) (order 𝒢)) mod int (order 𝒢))] (mod int (order 𝒢))"
      by (metis (no_types) cong_def mod_mult_right_eq)
    then show ?thesis
      by (meson ‹[(int (fst z) - int (fst z')) * (fst (bezw ((e mod order 𝒢 - e' mod order 𝒢) mod order 𝒢) (order 𝒢)) mod int (order 𝒢)) + int x * (int (snd z) - int (snd z')) * (fst (bezw ((e mod order 𝒢 - e' mod order 𝒢) mod order 𝒢) (order 𝒢)) mod int (order 𝒢)) = int t] (mod int (order 𝒢))› cong_add_rcancel cong_mod_left cong_trans)
  qed
  hence "[(int (fst z) - int (fst z')) * fst (bezw ((e mod order 𝒢 - e' mod order 𝒢) mod order 𝒢) (order 𝒢)) mod order 𝒢 + (int x * (int (snd z) - int (snd z'))) 
            * fst (bezw ((e mod order 𝒢 - e' mod order 𝒢) mod order 𝒢) (order 𝒢)) mod order 𝒢
               = t] (mod order 𝒢)"
  proof -
    have "int x * ((int (snd z) - int (snd z')) * (fst (bezw ((e mod order 𝒢 - e' mod order 𝒢) mod order 𝒢) (order 𝒢)) mod int (order 𝒢))) mod int (order 𝒢) = int x * ((int (snd z) - int (snd z')) * fst (bezw ((e mod order 𝒢 - e' mod order 𝒢) mod order 𝒢) (order 𝒢))) mod int (order 𝒢) mod int (order 𝒢)"
      by (metis (no_types) mod_mod_trivial mod_mult_right_eq)
    then have "[int x * ((int (snd z) - int (snd z')) * fst (bezw ((e mod order 𝒢 - e' mod order 𝒢) mod order 𝒢) (order 𝒢))) mod int (order 𝒢) = int x * ((int (snd z) - int (snd z')) * (fst (bezw ((e mod order 𝒢 - e' mod order 𝒢) mod order 𝒢) (order 𝒢)) mod int (order 𝒢)))] (mod int (order 𝒢))"
      by (metis (no_types) cong_def)
    then have "[(int (fst z) - int (fst z')) * fst (bezw ((e mod order 𝒢 - e' mod order 𝒢) mod order 𝒢) (order 𝒢)) mod int (order 𝒢) + int x * ((int (snd z) - int (snd z')) * fst (bezw ((e mod order 𝒢 - e' mod order 𝒢) mod order 𝒢) (order 𝒢))) mod int (order 𝒢) = (int (fst z) - int (fst z')) * fst (bezw ((e mod order 𝒢 - e' mod order 𝒢) mod order 𝒢) (order 𝒢)) mod int (order 𝒢) + int x * (int (snd z) - int (snd z')) * (fst (bezw ((e mod order 𝒢 - e' mod order 𝒢) mod order 𝒢) (order 𝒢)) mod int (order 𝒢))] (mod int (order 𝒢))"
      by (metis (no_types) Groups.mult_ac(1) cong_add cong_refl)
    then have "[(int (fst z) - int (fst z')) * fst (bezw ((e mod order 𝒢 - e' mod order 𝒢) mod order 𝒢) (order 𝒢)) mod int (order 𝒢) + int x * ((int (snd z) - int (snd z')) * fst (bezw ((e mod order 𝒢 - e' mod order 𝒢) mod order 𝒢) (order 𝒢))) mod int (order 𝒢) = int t] (mod int (order 𝒢))"
      using ‹[(int (fst z) - int (fst z')) * fst (bezw ((e mod order 𝒢 - e' mod order 𝒢) mod order 𝒢) (order 𝒢)) mod int (order 𝒢) + int x * (int (snd z) - int (snd z')) * (fst (bezw ((e mod order 𝒢 - e' mod order 𝒢) mod order 𝒢) (order 𝒢)) mod int (order 𝒢)) = int t] (mod int (order 𝒢))› cong_trans by blast
    then show ?thesis
      by (metis (no_types) Groups.mult_ac(1))
  qed
  hence "❙g [^] ((int (fst z) - int (fst z')) * fst (bezw ((e mod order 𝒢 - e' mod order 𝒢) mod order 𝒢) (order 𝒢)) mod order 𝒢 + (int x * (int (snd z) - int (snd z'))) 
            * fst (bezw ((e mod order 𝒢 - e' mod order 𝒢) mod order 𝒢) (order 𝒢)) mod order 𝒢)
               = ❙g [^] t"
    by (metis cong_def int_pow_int pow_generator_mod_int)
  hence "❙g [^] ((int (fst z) - int (fst z')) * fst (bezw ((e mod order 𝒢 - e' mod order 𝒢) mod order 𝒢) (order 𝒢)) mod order 𝒢) ⊗ ❙g [^] ((int x * (int (snd z) - int (snd z'))) 
            * fst (bezw ((e mod order 𝒢 - e' mod order 𝒢) mod order 𝒢) (order 𝒢)) mod order 𝒢)
               = ❙g [^] t"
    using int_pow_mult by auto
  hence "❙g [^] ((int (fst z) - int (fst z')) * fst (bezw ((e mod order 𝒢 - e' mod order 𝒢) mod order 𝒢) (order 𝒢)) mod order 𝒢) ⊗ ❙g [^] ((int x * ((int (snd z) - int (snd z'))) 
            * fst (bezw ((e mod order 𝒢 - e' mod order 𝒢) mod order 𝒢) (order 𝒢)) mod order 𝒢))
               = ❙g [^] t"
    by blast
  hence "❙g [^] ((int (fst z) - int (fst z')) * fst (bezw ((e mod order 𝒢 - e' mod order 𝒢) mod order 𝒢) (order 𝒢)) mod order 𝒢) ⊗ g' [^] ((((int (snd z) - int (snd z'))) 
            * fst (bezw ((e mod order 𝒢 - e' mod order 𝒢) mod order 𝒢) (order 𝒢)) mod order 𝒢))
               = ❙g [^] t"
    by (smt g'_def cyclic_group.generator_closed int_pow_int int_pow_pow mod_mult_right_eq more_arith_simps(11) okamoto_axioms okamoto_def pow_generator_mod_int)
  thus ?thesis using t by simp
qed

lemma special_soundness:
  shows "Σ_protocols_base.special_soundness"       
  unfolding Σ_protocols_base.special_soundness_def 
  by(auto simp add: valid_pub_def check_def R_def ss_adversary_def Let_def ss_rewrite challenge_space_def split_def)

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

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

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 add:)

lemma reduction_to_dis_log:
  shows "okamoto_Σ_commit.rel_advantage 𝒜 = dis_log.advantage (dis_log_alt.adversary2 𝒜)"
proof-
  have exp_rewrite: "❙g [^] w1 ⊗ g' [^] w2 =  ❙g [^] (w1 + x * w2)" for w1 w2 :: nat
    by (simp add: nat_pow_mult nat_pow_pow g'_def)
  have "okamoto_Σ_commit.rel_game 𝒜 = TRY do {
    w1 ← sample_uniform (order 𝒢);
    w2 ← sample_uniform (order 𝒢);
    let h = (❙g [^] w1 ⊗ g' [^] w2);
    (w1',w2') ← 𝒜 h;
    return_spmf (h = ❙g [^] w1' ⊗ g' [^] w2')} ELSE return_spmf False"
    unfolding okamoto_Σ_commit.rel_game_def
    by(simp add: Let_def split_def R_def G_def)
  also have "... = TRY do {
    w1 ← sample_uniform (order 𝒢);
    w2 ← sample_uniform (order 𝒢);
    let w = (w1 + x * w2) mod (order 𝒢);
    let h = ❙g [^] w;
    (w1',w2') ← 𝒜 h;
    return_spmf (h = ❙g [^] w1' ⊗ g' [^] w2')} ELSE return_spmf False"
    using g'_def exp_rewrite pow_generator_mod by simp
  also have "... = TRY do {
    w2 ← sample_uniform (order 𝒢);
    w ← map_spmf (λ w1. (x * w2 + w1) mod (order 𝒢)) (sample_uniform (order 𝒢));
    let h = ❙g [^] w;
    (w1',w2') ← 𝒜 h;
    return_spmf (h = ❙g [^] w1' ⊗ g' [^] w2')} ELSE return_spmf False"
    including monad_normalisation
    by(simp add: bind_map_spmf o_def Let_def add.commute)
  also have "... = TRY do {
    w2 :: nat ← sample_uniform (order 𝒢);
    w ← sample_uniform (order 𝒢);
    let h = ❙g [^] w;
    (w1',w2') ← 𝒜 h;
    return_spmf (h = ❙g [^] w1' ⊗ g' [^] w2')} ELSE return_spmf False"
    using samp_uni_plus_one_time_pad add.commute by simp
  also have "... = TRY do {
    w ← sample_uniform (order 𝒢);
    let h = ❙g [^] w;
    (w1',w2') ← 𝒜 h;
    return_spmf (h = ❙g [^] w1' ⊗ g' [^] w2')} ELSE return_spmf False"
    by(simp add: bind_spmf_const)
  also have "... = dis_log_alt.dis_log2 𝒜"
    apply(simp add: dis_log_alt.dis_log2_def Let_def dis_log_alt.g'_def g'_def)
    apply(intro try_spmf_cong)
     apply(intro bind_spmf_cong[OF refl]; clarsimp?)
     apply auto
    using exp_rewrite pow_generator_mod g'_def 
     apply (metis group_eq_pow_eq_mod okamoto_axioms okamoto_base.order_gt_0 okamoto_def)
    using exp_rewrite g'_def order_gt_0_iff_finite pow_generator_eq_iff_cong by auto
  ultimately have "okamoto_Σ_commit.rel_game 𝒜 = dis_log_alt.dis_log2 𝒜"
    by simp
  hence "okamoto_Σ_commit.rel_advantage 𝒜 = dis_log_alt.advantage2 𝒜"
    by(simp add: okamoto_Σ_commit.rel_advantage_def dis_log_alt.advantage2_def)
  thus ?thesis
    by (simp add: dis_log_alt_reductions.dis_log_adv2 cyclic_group_axioms dis_log_alt.dis_log_alt_axioms dis_log_alt_reductions.intro)
qed

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

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

lemma binding: 
  shows "okamoto_Σ_commit.abstract_com.bind_advantage 𝒜 
          ≤ dis_log.advantage (dis_log_alt.adversary2 (okamoto_Σ_commit.adversary 𝒜))"
  using okamoto_Σ_commit.bind_advantage reduction_to_dis_log by auto

end

locale okamoto_asymp = 
  fixes 𝒢 :: "nat ⇒ 'grp cyclic_group"
    and x :: nat
  assumes okamoto: "⋀η. okamoto (𝒢 η)"
begin

sublocale okamoto "𝒢 η" for η 
  by(simp add: okamoto)

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

theorem sigma_protocol:
  shows "Σ_protocols_base.Σ_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: "okamoto_Σ_commit.abstract_com.correct n" 
  using  okamoto_Σ_commit.commit_correct by simp

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

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

end

end