diff --git a/thys/Sigma_Commit_Crypto/Chaum_Pedersen_Sigma_Commit.thy b/thys/Sigma_Commit_Crypto/Chaum_Pedersen_Sigma_Commit.thy --- a/thys/Sigma_Commit_Crypto/Chaum_Pedersen_Sigma_Commit.thy +++ b/thys/Sigma_Commit_Crypto/Chaum_Pedersen_Sigma_Commit.thy @@ -1,509 +1,506 @@ 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' = \<^bold>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 ((\<^bold>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, \<^bold>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) = \<^bold>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 = \<^bold>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 = \<^bold>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 "\<^bold>g [^] y \ (\<^bold>g [^] w') [^] e = \<^bold>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 = \<^bold>g [^] w" and z: "z < order \" shows "\<^bold>g [^] ((z + (order \)* w * c - w*c)) = \<^bold>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 = \<^bold>g [^] z \ \<^bold>g [^] ((order \) * w *c - w*c)" by(simp add: nat_pow_mult) have " \<^bold>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 " \<^bold>g [^] ((order \)*w*c - w*c) = \<^bold>g [^] int ((order \)*w*c - w*c)" by (simp add: int_pow_int) also have "... = \<^bold>g [^] int ((order \)*w*c) \ inv (\<^bold>g [^] (w*c))" using int_pow_diff[of "\<^bold>g" "order \ * w * c" "w * c"] * generator_closed int_ops(6) int_pow_neg int_pow_neg_int by presburger also have "... = \<^bold>g [^] ((order \)*w*c) \ inv (\<^bold>g [^] (w*c))" by (metis int_pow_int) also have "... = \<^bold>g [^] ((order \)*w*c) \ inv ((\<^bold>g [^] w) [^] c)" by(simp add: nat_pow_pow) also have "... = \<^bold>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' = \<^bold>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 - 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"] g'_carrier - by (metis * chaum_ped_\_axioms chaum_ped_\_def cyclic_group_def group.int_pow_neg_int int_ops(6) int_pow_neg less_not_refl2 of_nat_eq_0_iff) + 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 int_pow_int) + 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 = (\<^bold>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 = \<^bold>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 = \<^bold>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 = \<^bold>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 = \<^bold>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 = \<^bold>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 = \<^bold>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 = \<^bold>g [^] z" and e': "e' < e" and "a \ fst h [^] e' = \<^bold>g [^] z'" shows "fst h = \<^bold>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 = \<^bold>g [^] z \ inv (fst h [^] e)" using assms by (simp add: assms inv_solve_right) moreover have "a = \<^bold>g [^] z' \ inv (fst h [^] e')" using assms by (simp add: assms inv_solve_right) ultimately have "\<^bold>g [^] z \ fst h [^] e' = \<^bold>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 = \<^bold>g [^] t" using assms generatorE by blast ultimately have "\<^bold>g [^] (z + t * e') = \<^bold>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, hide_lams) 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 "\<^bold>g [^] (nat ((int z - int z') * fst (bezw (e - e') (order \)) mod order \)) = \<^bold>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 = \<^bold>g [^] z" and "b \ snd h [^] e = g' [^] z" and "e' < e" and "a \ fst h [^] e' = \<^bold>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 = \<^bold>g [^] t" using assms(2) generatorE by blast ultimately have "\<^bold>g [^] (x * z + t * e') = \<^bold>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, hide_lams) 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 "\<^bold>g [^] (nat ((int x * (int z - int z')) * fst (bezw (e - e') (order \)) mod order \)) = \<^bold>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, hide_lams) * 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 = \<^bold>g [^] t" using assms(2) generatorE by blast ultimately have "\<^bold>g [^] (x * z + t * e') = \<^bold>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 "\<^bold>g [^] (int x * (int z - int z') * fst (bezw ((e mod order \ - e' mod order \) mod order \) (order \))) = \<^bold>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, hide_lams) 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) = ((\<^bold>g [^] w, g' [^] w), w); w' \ \ h; return_spmf ((fst h = \<^bold>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) = ((\<^bold>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