diff --git a/thys/Sigma_Commit_Crypto/Pedersen.thy b/thys/Sigma_Commit_Crypto/Pedersen.thy --- a/thys/Sigma_Commit_Crypto/Pedersen.thy +++ b/thys/Sigma_Commit_Crypto/Pedersen.thy @@ -1,291 +1,291 @@ subsection\Pedersen Commitment Scheme\ text\The Pedersen commitment scheme \cite{BLP:conf/crypto/Pedersen91} is a commitment scheme based on a cyclic group. We use the construction of cyclic groups from CryptHOL to formalise the commitment scheme. We prove perfect hiding and computational binding, with a reduction to the discrete log problem. We a proof of the Pedersen commitment scheme is realised in the instantiation of the Schnorr \\\-protocol with the general construction of commitment schemes from \\\-protocols. The commitment scheme that is realised there however take the inverse of the message in the commitment phase due to the construction of the simulator in the \\\-protocol proof. The two schemes are in some way equal however as we do not have a well defined notion of equality for commitment schemes we keep this section of the formalisation. This also serves as reference to the formal proof of the Pedersen commitment scheme we provide in \cite{DBLP:conf/post/ButlerAG19}.\ theory Pedersen imports Commitment_Schemes "HOL-Number_Theory.Cong" Cyclic_Group_Ext Discrete_Log Number_Theory_Aux Uniform_Sampling begin locale pedersen_base = fixes \ :: "'grp cyclic_group" (structure) assumes prime_order: "prime (order \)" begin lemma order_gt_0 [simp]: "order \ > 0" by (simp add: prime_gt_0_nat prime_order) type_synonym 'grp' ck = "'grp'" type_synonym 'grp' vk = "'grp'" type_synonym plain = "nat" type_synonym 'grp' commit = "'grp'" -type_synonym opening = "nat" +type_synonym "opening" = "nat" definition key_gen :: "('grp ck \ 'grp vk) spmf" where "key_gen = do { x :: nat \ sample_uniform (order \); let h = \<^bold>g [^] x; return_spmf (h, h) }" definition commit :: "'grp ck \ plain \ ('grp commit \ opening) spmf" where "commit ck m = do { d :: nat \ sample_uniform (order \); let c = (\<^bold>g [^] d) \ (ck [^] m); return_spmf (c,d) }" definition commit_inv :: "'grp ck \ plain \ ('grp commit \ opening) spmf" where "commit_inv ck m = do { d :: nat \ sample_uniform (order \); let c = (\<^bold>g [^] d) \ (inv ck [^] m); return_spmf (c,d) }" definition verify :: "'grp vk \ plain \ 'grp commit \ opening \ bool" where "verify v_key m c d = (c = (\<^bold>g [^] d \ v_key [^] m))" definition valid_msg :: "plain \ bool" where "valid_msg msg \ (msg < order \)" definition dis_log_\ :: "('grp ck, plain, 'grp commit, opening) bind_adversary \ 'grp ck \ nat spmf" where "dis_log_\ \ h = do { (c, m, d, m', d') \ \ h; _ :: unit \ assert_spmf (m \ m' \ valid_msg m \ valid_msg m'); _ :: unit \ assert_spmf (c = \<^bold>g [^] d \ h [^] m \ c = \<^bold>g [^] d' \ h [^] m'); return_spmf (if (m > m') then (nat ((int d' - int d) * inverse (m - m') (order \) mod order \)) else (nat ((int d - int d') * inverse (m' - m) (order \) mod order \)))}" sublocale ped_commit: abstract_commitment key_gen commit verify valid_msg . sublocale discrete_log: dis_log _ unfolding dis_log_def by(simp) end locale pedersen = pedersen_base + cyclic_group \ begin lemma mod_one_cancel: assumes "[int y * z * x = y' * x] (mod order \)" and "[z * x = 1] (mod order \)" shows "[int y = y' * x] (mod order \)" by (metis assms Groups.mult_ac(2) cong_scalar_right cong_sym_eq cong_trans more_arith_simps(11) more_arith_simps(5)) lemma dis_log_break: fixes d d' m m' :: nat assumes c: " \<^bold>g [^] d' \ (\<^bold>g [^] y) [^] m' = \<^bold>g [^] d \ (\<^bold>g [^] y) [^] m" and y_less_order: "y < order \" and m_ge_m': "m > m'" and m: "m < order \" shows "y = nat ((int d' - int d) * (fst (bezw ((m - m')) (order \))) mod order \)" proof - have mm': "\ [m = m'] (mod order \)" using m m_ge_m' basic_trans_rules(19) cong_less_modulus_unique_nat by blast hence gcd: "int (gcd ((m - m')) (order \)) = 1" using assms(3) assms(4) prime_field prime_order by auto have "\<^bold>g [^] (d + y * m) = \<^bold>g [^] (d' + y * m')" using c by (simp add: nat_pow_mult nat_pow_pow) hence "[d + y * m = d' + y * m'] (mod order \)" by(simp add: pow_generator_eq_iff_cong finite_carrier) hence "[int d + int y * int m = int d' + int y * int m'] (mod order \)" using cong_int_iff by force from cong_diff[OF this cong_refl, of "int d + int y * int m'"] have "[int y * int (m - m') = int d' - int d] (mod order \)" using m_ge_m' by(simp add: int_distrib of_nat_diff) hence *: "[int y * int (m - m') * (fst (bezw ((m - m')) (order \))) = (int d' - int d) * (fst (bezw ((m - m')) (order \)))] (mod order \)" by (simp add: cong_scalar_right) hence "[int y * (int (m - m') * (fst (bezw ((m - m')) (order \)))) = (int d' - int d) * (fst (bezw ((m - m')) (order \)))] (mod order \)" by (simp add: more_arith_simps(11)) hence "[int y * 1 = (int d' - int d) * (fst (bezw ((m - m')) (order \)))] (mod order \)" using inverse gcd by (smt Groups.mult_ac(2) Number_Theory_Aux.inverse Totient.of_nat_eq_1_iff * cong_def int_ops(9) mod_mult_right_eq mod_one_cancel) hence "[int y = (int d' - int d) * (fst (bezw ((m - m')) (order \)))] (mod order \)" by simp hence "y mod order \ = (int d' - int d) * (fst (bezw ((m - m')) (order \))) mod order \" using cong_def zmod_int by auto thus ?thesis using y_less_order by simp qed lemma dis_log_break': assumes "y < order \" and "\ m' < m" and "m \ m'" and m: "m' < order \" and "\<^bold>g [^] d \ (\<^bold>g [^] y) [^] m = \<^bold>g [^] d' \ (\<^bold>g [^] y) [^] m'" shows "y = nat ((int d - int d') * fst (bezw ((m' - m)) (order \)) mod int (order \))" proof- have "m' > m" using assms using group_eq_pow_eq_mod nat_neq_iff order_gt_0 by blast thus ?thesis using dis_log_break[of d y m d' m' ]assms cong_sym_eq assms by blast qed lemma set_spmf_samp_uni [simp]: "set_spmf (sample_uniform (order \)) = {x. x < order \}" by(auto simp add: sample_uniform_def) lemma correct: shows "spmf (ped_commit.correct_game m) True = 1" using finite_carrier order_gt_0_iff_finite apply(simp add: abstract_commitment.correct_game_def Let_def commit_def verify_def) by(simp add: key_gen_def Let_def bind_spmf_const cong: bind_spmf_cong_simp) theorem abstract_correct: shows "ped_commit.correct" unfolding abstract_commitment.correct_def using correct by simp lemma perfect_hiding: shows "spmf (ped_commit.hiding_game_ind_cpa \) True - 1/2 = 0" including monad_normalisation proof - obtain \1 \2 where [simp]: "\ = (\1, \2)" by(cases \) note [simp] = Let_def split_def have "ped_commit.hiding_game_ind_cpa (\1, \2) = TRY do { (ck,vk) \ key_gen; ((m0, m1), \) \ \1 vk; _ :: unit \ assert_spmf (valid_msg m0 \ valid_msg m1); b \ coin_spmf; (c,d) \ commit ck (if b then m0 else m1); b' \ \2 c \; return_spmf (b' = b)} ELSE coin_spmf" by(simp add: abstract_commitment.hiding_game_ind_cpa_def) also have "... = TRY do { x :: nat \ sample_uniform (order \); let h = \<^bold>g [^] x; ((m0, m1), \) \ \1 h; _ :: unit \ assert_spmf (valid_msg m0 \ valid_msg m1); b \ coin_spmf; d :: nat \ sample_uniform (order \); let c = ((\<^bold>g [^] d) \ (h [^] (if b then m0 else m1))); b' \ \2 c \; return_spmf (b' = b)} ELSE coin_spmf" by(simp add: commit_def key_gen_def) also have "... = TRY do { x :: nat \ sample_uniform (order \); let h = (\<^bold>g [^] x); ((m0, m1), \) \ \1 h; _ :: unit \ assert_spmf (valid_msg m0 \ valid_msg m1); b \ coin_spmf; z \ map_spmf (\z. \<^bold>g [^] z \ (h [^] (if b then m0 else m1))) (sample_uniform (order \)); guess :: bool \ \2 z \; return_spmf(guess = b)} ELSE coin_spmf" by(simp add: bind_map_spmf o_def) also have "... = TRY do { x :: nat \ sample_uniform (order \); let h = (\<^bold>g [^] x); ((m0, m1), \) \ \1 h; _ :: unit \ assert_spmf (valid_msg m0 \ valid_msg m1); b \ coin_spmf; z \ map_spmf (\z. \<^bold>g [^] z) (sample_uniform (order \)); guess :: bool \ \2 z \; return_spmf(guess = b)} ELSE coin_spmf" by(simp add: sample_uniform_one_time_pad) also have "... = TRY do { x :: nat \ sample_uniform (order \); let h = (\<^bold>g [^] x); ((m0, m1), \) \ \1 h; _ :: unit \ assert_spmf (valid_msg m0 \ valid_msg m1); z \ map_spmf (\z. \<^bold>g [^] z) (sample_uniform (order \)); guess :: bool \ \2 z \; map_spmf((=) guess) coin_spmf} ELSE coin_spmf" by(simp add: map_spmf_conv_bind_spmf) also have "... = coin_spmf" by(auto simp add: bind_spmf_const map_eq_const_coin_spmf try_bind_spmf_lossless2' scale_bind_spmf weight_spmf_le_1 scale_scale_spmf) ultimately show ?thesis by(simp add: spmf_of_set) qed theorem abstract_perfect_hiding: shows "ped_commit.perfect_hiding_ind_cpa \" proof- have "spmf (ped_commit.hiding_game_ind_cpa \) True - 1/2 = 0" using perfect_hiding by fastforce thus ?thesis by(simp add: abstract_commitment.perfect_hiding_ind_cpa_def abstract_commitment.hiding_advantage_ind_cpa_def) qed lemma bind_output_cong: assumes "x < order \" shows "(x = nat ((int b - int ab) * fst (bezw (aa - ac) (order \)) mod int (order \))) \ [x = nat ((int b - int ab) * fst (bezw (aa - ac) (order \)) mod int (order \))] (mod order \)" using assms cong_less_modulus_unique_nat nat_less_iff by auto lemma bind_game_eq_dis_log: shows "ped_commit.bind_game \ = discrete_log.dis_log (dis_log_\ \)" proof- note [simp] = Let_def split_def have "ped_commit.bind_game \ = TRY do { (ck,vk) \ key_gen; (c, m, d, m', d') \ \ ck; _ :: unit \ assert_spmf(m \ m' \ valid_msg m \ valid_msg m'); let b = verify vk m c d; let b' = verify vk m' c d'; _ :: unit \ assert_spmf (b \ b'); return_spmf True} ELSE return_spmf False" by(simp add: abstract_commitment.bind_game_alt_def) also have "... = TRY do { x :: nat \ sample_uniform (Coset.order \); (c, m, d, m', d') \ \ (\<^bold>g [^] x); _ :: unit \ assert_spmf (m \ m' \ valid_msg m \ valid_msg m'); _ :: unit \ assert_spmf (c = \<^bold>g [^] d \ (\<^bold>g [^] x) [^] m \ c = \<^bold>g [^] d' \ (\<^bold>g [^] x) [^] m'); return_spmf True} ELSE return_spmf False" by(simp add: verify_def key_gen_def) also have "... = TRY do { x :: nat \ sample_uniform (order \); (c, m, d, m', d') \ \ (\<^bold>g [^] x); _ :: unit \ assert_spmf (m \ m' \ valid_msg m \ valid_msg m'); _ :: unit \ assert_spmf (c = \<^bold>g [^] d \ (\<^bold>g [^] x) [^] m \ c = \<^bold>g [^] d' \ (\<^bold>g [^] x) [^] m'); return_spmf (x = (if (m > m') then (nat ((int d' - int d) * (fst (bezw ((m - m')) (order \))) mod order \)) else (nat ((int d - int d') * (fst (bezw ((m' - m)) (order \))) mod order \))))} ELSE return_spmf False" apply(intro try_spmf_cong bind_spmf_cong[OF refl]; clarsimp?) apply(auto simp add: valid_msg_def) apply(intro bind_spmf_cong[OF refl]; clarsimp?)+ apply(simp add: dis_log_break) apply(intro bind_spmf_cong[OF refl]; clarsimp?)+ by(simp add: dis_log_break') ultimately show ?thesis apply(simp add: discrete_log.dis_log_def dis_log_\_def cong: bind_spmf_cong_simp) apply(intro try_spmf_cong bind_spmf_cong[OF refl]; clarsimp?)+ using bind_output_cong by auto qed theorem pedersen_bind: "ped_commit.bind_advantage \ = discrete_log.advantage (dis_log_\ \)" unfolding abstract_commitment.bind_advantage_def discrete_log.advantage_def using bind_game_eq_dis_log by simp end locale pedersen_asymp = fixes \ :: "nat \ 'grp cyclic_group" assumes pedersen: "\\. pedersen (\ \)" begin sublocale pedersen "\ \" for \ by(simp add: pedersen) theorem pedersen_correct_asym: shows "ped_commit.correct n" using abstract_correct by simp theorem pedersen_perfect_hiding_asym: shows "ped_commit.perfect_hiding_ind_cpa n (\ n)" by (simp add: abstract_perfect_hiding) theorem pedersen_bind_asym: shows "negligible (\ n. ped_commit.bind_advantage n (\ n)) \ negligible (\ n. discrete_log.advantage n (dis_log_\ n (\ n)))" by(simp add: pedersen_bind) end end diff --git a/thys/Sigma_Commit_Crypto/Rivest.thy b/thys/Sigma_Commit_Crypto/Rivest.thy --- a/thys/Sigma_Commit_Crypto/Rivest.thy +++ b/thys/Sigma_Commit_Crypto/Rivest.thy @@ -1,363 +1,363 @@ subsection\Rivest Commitment Scheme\ text\The Rivest commitment scheme was first introduced in \cite{rivest1999}. We note however the original scheme did not allow for perfect hiding. This was pointed out by Blundo and Masucci in \cite{DBLP:journals/dcc/BlundoMSW02} who alightly ammended the commitment scheme so that is provided perfect hiding. The Rivest commitment scheme uses a trusted initialiser to provide correlated randomness to the two parties before an execution of the protocol. In our framework we set these as keys that held by the respective parties.\ theory Rivest imports Commitment_Schemes "HOL-Number_Theory.Cong" CryptHOL.CryptHOL Cyclic_Group_Ext Discrete_Log Number_Theory_Aux Uniform_Sampling begin locale rivest = fixes q :: nat assumes prime_q: "prime q" begin lemma q_gt_0 [simp]: "q > 0" by (simp add: prime_q prime_gt_0_nat) type_synonym ck = "nat \ nat" type_synonym vk = "nat \ nat" type_synonym plain = "nat" type_synonym commit = "nat" -type_synonym opening = "nat \ nat" +type_synonym "opening" = "nat \ nat" definition key_gen :: "(ck \ vk) spmf" where "key_gen = do { a :: nat \ sample_uniform q; b :: nat \ sample_uniform q; x1 :: nat \ sample_uniform q; let y1 = (a * x1 + b) mod q; return_spmf ((a,b), (x1,y1))}" definition commit :: "ck \ plain \ (commit \ opening) spmf" where "commit ck m = do { let (a,b) = ck; return_spmf ((m + a) mod q, (a,b))}" fun verify :: "vk \ plain \ commit \ opening \ bool" where "verify (x1,y1) m c (a,b) = (((c = (m + a) mod q)) \ (y1 = (a * x1 + b) mod q))" definition valid_msg :: "plain \ bool" where "valid_msg msg \ msg \ {..< q}" sublocale rivest_commit: abstract_commitment key_gen commit verify valid_msg . lemma abstract_correct: "rivest_commit.correct" unfolding abstract_commitment.correct_def abstract_commitment.correct_game_def by(simp add: key_gen_def commit_def bind_spmf_const lossless_weight_spmfD) lemma rivest_hiding: "(spmf (rivest_commit.hiding_game_ind_cpa \) True - 1/2 = 0)" including monad_normalisation proof- note [simp] = Let_def split_def obtain \1 \2 where [simp]: "\ = (\1, \2)" by(cases \) have "rivest_commit.hiding_game_ind_cpa (\1, \2) = TRY do { a :: nat \ sample_uniform q; x1 :: nat \ sample_uniform q; y1 \ map_spmf (\ b. (a * x1 + b) mod q) (sample_uniform q); ((m0, m1), \) \ \1 (x1,y1); _ :: unit \ assert_spmf (valid_msg m0 \ valid_msg m1); d \ coin_spmf; let c = ((if d then m0 else m1) + a) mod q; b' \ \2 c \; return_spmf (b' = d)} ELSE coin_spmf" unfolding abstract_commitment.hiding_game_ind_cpa_def by(simp add: commit_def key_gen_def o_def bind_map_spmf) also have "... = TRY do { a :: nat \ sample_uniform q; x1 :: nat \ sample_uniform q; y1 \ sample_uniform q; ((m0, m1), \) \ \1 (x1,y1); _ :: unit \ assert_spmf (valid_msg m0 \ valid_msg m1); d \ coin_spmf; let c = ((if d then m0 else m1) + a) mod q; b' \ \2 c \; return_spmf (b' = d)} ELSE coin_spmf" by(simp add: samp_uni_plus_one_time_pad) also have "... = TRY do { x1 :: nat \ sample_uniform q; y1 \ sample_uniform q; ((m0, m1), \) \ \1 (x1,y1); _ :: unit \ assert_spmf (valid_msg m0 \ valid_msg m1); d \ coin_spmf; c \ map_spmf (\ a. ((if d then m0 else m1) + a) mod q) (sample_uniform q); b' \ \2 c \; return_spmf (b' = d)} ELSE coin_spmf" by(simp add: o_def bind_map_spmf) also have "... = TRY do { x1 :: nat \ sample_uniform q; y1 \ sample_uniform q; ((m0, m1), \) \ \1 (x1,y1); _ :: unit \ assert_spmf (valid_msg m0 \ valid_msg m1); d \ coin_spmf; c \ sample_uniform q; b' :: bool \ \2 c \; return_spmf (b' = d)} ELSE coin_spmf" by(simp add: samp_uni_plus_one_time_pad) also have "... = TRY do { x1 :: nat \ sample_uniform q; y1 \ sample_uniform q; ((m0, m1), \) \ \1 (x1,y1); _ :: unit \ assert_spmf (valid_msg m0 \ valid_msg m1); c :: nat \ sample_uniform q; guess :: bool \ \2 c \; map_spmf((=) guess) coin_spmf} ELSE coin_spmf" by(simp add: map_spmf_conv_bind_spmf) also have "... = coin_spmf" by(simp add: map_eq_const_coin_spmf bind_spmf_const try_bind_spmf_lossless2' scale_bind_spmf weight_spmf_le_1 scale_scale_spmf) ultimately show ?thesis by(simp add: spmf_of_set) qed lemma rivest_perfect_hiding: "rivest_commit.perfect_hiding_ind_cpa \" unfolding abstract_commitment.perfect_hiding_ind_cpa_def abstract_commitment.hiding_advantage_ind_cpa_def by(simp add: rivest_hiding) lemma samp_uni_break': assumes fst_cond: "m \ m' \ valid_msg m \ valid_msg m'" and c: "c = (m + a) mod q \ y1 = (a * x1 + b) mod q" and c': "c = (m' + a') mod q \ y1 = (a' * x1 + b') mod q" and x1: "x1 < q" shows "x1 = (if (a mod q > a' mod q) then nat ((int b'- int b) * (inverse (nat ((int a mod q - int a' mod q) mod q)) q) mod q) else nat ((int b- int b') * (inverse (nat ((int a' mod q - int a mod q) mod q)) q) mod q))" proof- have m: "m < q \ m' < q" using fst_cond valid_msg_def by simp have a_a': "\ [a = a'] (mod q)" proof- have "[m + a = m' + a'] (mod q)" using assms cong_def by blast thus ?thesis by (metis m fst_cond c c' add.commute cong_less_modulus_unique_nat cong_add_rcancel_nat cong_mod_right) qed have cong_y1: "[int a * int x1 + int b = int a' * int x1 + int b'] (mod q)" by (metis c c' cong_def Num.of_nat_simps(4) Num.of_nat_simps(5) cong_int_iff) show ?thesis proof(cases "a mod q > a' mod q") case True hence gcd: "gcd (nat ((int a mod q - int a' mod q) mod q)) q = 1" proof- have "((int a mod q - int a' mod q) mod q) \ 0" by (metis True comm_monoid_add_class.add_0 diff_add_cancel mod_add_left_eq mod_diff_eq nat_mod_as_int order_less_irrefl) moreover have "((int a mod q - int a' mod q) mod q) < q" by simp ultimately show ?thesis using prime_field[of q "nat ((int a mod int q - int a' mod int q) mod int q)"] prime_q by (smt Euclidean_Division.pos_mod_sign coprime_imp_gcd_eq_1 int_nat_eq nat_less_iff of_nat_0_less_iff q_gt_0) qed hence "[int a * int x1 - int a' * int x1 = int b'- int b] (mod q)" by (smt cong_diff_iff_cong_0 cong_y1 cong_diff cong_diff) hence "[int a mod q * int x1 - int a' mod q * int x1 = int b'- int b] (mod q)" proof - have "[int x1 * (int a mod int q - int a' mod int q) = int x1 * (int a - int a')] (mod int q)" by (meson cong_def cong_mult cong_refl mod_diff_eq) then show ?thesis by (metis (no_types, hide_lams) Groups.mult_ac(2) \[int a * int x1 - int a' * int x1 = int b' - int b] (mod int q)\ cong_def mod_diff_left_eq mod_diff_right_eq mod_mult_right_eq) qed hence "[int x1 * (int a mod q - int a' mod q) = int b'- int b] (mod q)" by(metis int_distrib(3) mult.commute) hence "[int x1 * (int a mod q - int a' mod q) mod q = int b'- int b] (mod q)" using cong_def by simp hence "[int x1 * nat ((int a mod q - int a' mod q) mod q) = int b'- int b] (mod q)" by (simp add: True cong_def mod_mult_right_eq) hence "[int x1 * nat ((int a mod q - int a' mod q) mod q) * inverse (nat ((int a mod q - int a' mod q) mod q)) q = (int b'- int b) * inverse (nat ((int a mod q - int a' mod q) mod q)) q] (mod q)" using cong_scalar_right by blast hence "[int x1 * (nat ((int a mod q - int a' mod q) mod q) * inverse (nat ((int a mod q - int a' mod q) mod q)) q) = (int b'- int b) * inverse (nat ((int a mod q - int a' mod q) mod q)) q] (mod q)" by (simp add: more_arith_simps(11)) hence "[int x1 * 1 = (int b'- int b) * inverse (nat ((int a mod q - int a' mod q) mod q)) q] (mod q)" using inverse gcd by (meson cong_scalar_left cong_sym_eq cong_trans) hence "[int x1 = (int b'- int b) * inverse (nat ((int a mod q - int a' mod q) mod q)) q] (mod q)" by simp hence "int x1 mod q = ((int b'- int b) * inverse (nat ((int a mod q - int a' mod q) mod q)) q) mod q" using cong_def by fast thus ?thesis using x1 True by simp next case False hence aa': "a mod q < a' mod q" using a_a' cong_refl nat_neq_iff by (simp add: cong_def) hence gcd: "gcd (nat ((int a' mod q - int a mod q) mod q)) q = 1" proof- have "((int a' mod q - int a mod q) mod q) \ 0" by (metis aa' comm_monoid_add_class.add_0 diff_add_cancel mod_add_left_eq mod_diff_eq nat_mod_as_int order_less_irrefl) moreover have "((int a' mod q - int a mod q) mod q) < q" by simp ultimately show ?thesis using prime_field[of q "nat ((int a' mod int q - int a mod int q) mod int q)"] prime_q by (smt Euclidean_Division.pos_mod_sign coprime_imp_gcd_eq_1 int_nat_eq nat_less_iff of_nat_0_less_iff q_gt_0) qed have "[int b - int b' = int a' * int x1 - int a * int x1] (mod q)" by (smt cong_diff_iff_cong_0 cong_y1 cong_diff cong_diff) hence "[int b - int b' = int x1 * (int a' - int a)] (mod q)" using int_distrib mult.commute by metis hence "[int b - int b' = int x1 * (int a' mod q - int a mod q)] (mod q)" by (metis (no_types, lifting) cong_def mod_diff_eq mod_mult_right_eq) hence "[int b - int b' = int x1 * (int a' mod q - int a mod q) mod q] (mod q)" using cong_def by simp hence "[(int b - int b') * inverse (nat ((int a' mod q - int a mod q) mod q)) q = int x1 * (int a' mod q - int a mod q) mod q * inverse (nat ((int a' mod q - int a mod q) mod q)) q ] (mod q)" using cong_scalar_right by blast hence "[(int b - int b') * inverse (nat ((int a' mod q - int a mod q) mod q)) q = int x1 * ((int a' mod q - int a mod q) mod q * inverse (nat ((int a' mod q - int a mod q) mod q)) q)] (mod q)" by (metis (mono_tags, lifting) cong_def mod_mult_left_eq mod_mult_right_eq more_arith_simps(11)) hence *: "[int x1 * ((int a' mod q - int a mod q) mod q * inverse (nat ((int a' mod q - int a mod q) mod q)) q) = (int b - int b') * inverse (nat ((int a' mod q - int a mod q) mod q)) q] (mod q)" using cong_sym_eq by auto hence "[int x1 * 1 = (int b - int b') * inverse (nat ((int a' mod q - int a mod q) mod q)) q] (mod q)" proof - have "[(int a' mod int q - int a mod int q) mod int q * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q = 1] (mod int q)" by (metis (no_types) Euclidean_Division.pos_mod_sign inverse gcd int_nat_eq of_nat_0_less_iff q_gt_0) then show ?thesis by (meson * cong_scalar_left cong_sym_eq cong_trans) qed hence "[int x1 = (int b - int b') * inverse (nat ((int a' mod q - int a mod q) mod q)) q] (mod q)" by simp hence "int x1 mod q = (int b - int b') * (inverse (nat ((int a' mod q - int a mod q) mod q)) q) mod q" using cong_def by auto thus ?thesis using x1 aa' by simp qed qed lemma samp_uni_spmf_mod_q: shows "spmf (sample_uniform q) (x mod q) = 1/q" proof- have "indicator {..< q} (x mod q) = 1" using q_gt_0 by auto moreover have "real (card {..< q}) = q" by simp ultimately show ?thesis by(auto simp add: spmf_of_set sample_uniform_def) qed lemma spmf_samp_uni_eq_return_bool_mod: shows "spmf (do { x1 \ sample_uniform q; return_spmf (int x1 = y mod q)}) True = 1/q" proof- have "spmf (do { x1 \ sample_uniform q; return_spmf (x1 = y mod q)}) True = spmf (sample_uniform q \ (\ x1. return_spmf x1)) (y mod q)" apply(simp only: spmf_bind) apply(rule Bochner_Integration.integral_cong[OF refl])+ proof - fix x :: nat have "y mod q = x \ indicator {True} (x = (y mod q)) = (indicator {(y mod q)} x::real)" by simp then have "indicator {True} (x = y mod q) = (indicator {y mod q} x::real)" by fastforce then show "spmf (return_spmf (x = y mod q)) True = spmf (return_spmf x) (y mod q)" by (metis pmf_return spmf_of_pmf_return_pmf spmf_spmf_of_pmf) qed thus ?thesis using samp_uni_spmf_mod_q by simp qed lemma bind_game_le_inv_q: shows "spmf (rivest_commit.bind_game \) True \ 1 / q" proof - let ?eq = "\a a' b b'. (=) (if (a mod q > a' mod q) then nat ((int b'- int b) * (inverse (nat ((int a mod q - int a' mod q) mod q)) q) mod q) else nat ((int b - int b') * (inverse (nat ((int a' mod q - int a mod q) mod q)) q) mod q))" have "spmf (rivest_commit.bind_game \) True = spmf (do { (ck,(x1,y1)) \ key_gen; (c, m, (a,b), m', (a',b')) \ \ ck; _ :: unit \ assert_spmf(m \ m' \ valid_msg m \ valid_msg m'); let b = verify (x1,y1) m c (a,b); let b' = verify (x1,y1) m' c (a',b'); _ :: unit \ assert_spmf (b \ b'); return_spmf True}) True" by(simp add: abstract_commitment.bind_game_alt_def split_def spmf_try_spmf del: verify.simps) also have "... = spmf (do { a' :: nat \ sample_uniform q; b' :: nat \ sample_uniform q; x1 :: nat \ sample_uniform q; let y1 = (a' * x1 + b') mod q; (c, m, (a,b), m', (a',b')) \ \ (a',b'); _ :: unit \ assert_spmf (m \ m' \ valid_msg m \ valid_msg m'); _ :: unit \ assert_spmf (c = (m + a) mod q \ y1 = (a * x1 + b) mod q \ c = (m' + a') mod q \ y1 = (a' * x1 + b') mod q); return_spmf True}) True" by(simp add: key_gen_def Let_def) also have "... = spmf (do { a'' :: nat \ sample_uniform q; b'' :: nat \ sample_uniform q; x1 :: nat \ sample_uniform q; let y1 = (a'' * x1 + b'') mod q; (c, m, (a,b), m', (a',b')) \ \ (a'',b''); _ :: unit \ assert_spmf (m \ m' \ valid_msg m \ valid_msg m'); _ :: unit \ assert_spmf (c = (m + a) mod q \ y1 = (a * x1 + b) mod q \ c = (m' + a') mod q \ y1 = (a' * x1 + b') mod q); return_spmf (?eq a a' b b' x1)}) True" unfolding split_def Let_def by(rule arg_cong2[where f=spmf, OF _ refl] bind_spmf_cong[OF refl])+ (auto simp add: eq_commute samp_uni_break' Let_def split_def valid_msg_def cong: bind_spmf_cong_simp) also have "... \ spmf (do { a'' :: nat \ sample_uniform q; b'' :: nat \ sample_uniform q; (c, m, (a,(b::nat)), m', (a',b')) \ \ (a'',b''); map_spmf (?eq a a' b b') (sample_uniform q)}) True" including monad_normalisation unfolding split_def Let_def assert_spmf_def apply(simp add: map_spmf_conv_bind_spmf) apply(rule ord_spmf_eq_leD ord_spmf_bind_reflI)+ apply auto done also have "... \ 1/q" proof((rule spmf_bind_leI)+, clarify) fix a a' b b' define A where "A = Collect (?eq a a' b b')" define x1 where "x1 = The (?eq a a' b b')" note q_gt_0[simp del] have "A \ {x1}" by(auto simp add: A_def x1_def) hence "card (A \ {.. card {x1}" by(intro card_mono) auto also have "\ = 1" by simp finally have "spmf (map_spmf (\x. x \ A) (sample_uniform q)) True \ 1 / q" using q_gt_0 unfolding sample_uniform_def by(subst map_mem_spmf_of_set)(auto simp add: field_simps) then show "spmf (map_spmf (?eq a a' b b') (sample_uniform q)) True \ 1 / q" unfolding A_def mem_Collect_eq . qed auto finally show ?thesis . qed lemma rivest_bind: shows "rivest_commit.bind_advantage \ \ 1 / q" using bind_game_le_inv_q rivest_commit.bind_advantage_def by simp end locale rivest_asymp = fixes q :: "nat \ nat" assumes rivest: "\\. rivest (q \)" begin sublocale rivest "q \" for \ by(simp add: rivest) theorem rivest_correct: shows "rivest_commit.correct n" using abstract_correct by simp theorem rivest_perfect_hiding_asym: assumes lossless_\: "rivest_commit.lossless (\ n)" shows "rivest_commit.perfect_hiding_ind_cpa n (\ n)" by (simp add: lossless_\ rivest_perfect_hiding) theorem rivest_binding_asym: assumes "negligible (\n. 1 / (q n))" shows "negligible (\n. rivest_commit.bind_advantage n (\ n))" using negligible_le rivest_bind assms rivest_commit.bind_advantage_def by auto end end diff --git a/thys/Sigma_Commit_Crypto/Schnorr_Sigma_Commit.thy b/thys/Sigma_Commit_Crypto/Schnorr_Sigma_Commit.thy --- a/thys/Sigma_Commit_Crypto/Schnorr_Sigma_Commit.thy +++ b/thys/Sigma_Commit_Crypto/Schnorr_Sigma_Commit.thy @@ -1,401 +1,401 @@ subsection\Schnorr \\\-protocol\ text\In this section we show the Schnoor protocol \cite{DBLP:journals/joc/Schnorr91} is a \\\-protocol and then use it to construct a commitment scheme. The security statements for the resulting commitment scheme come for free from our general proof of the construction.\ theory Schnorr_Sigma_Commit imports Commitment_Schemes Sigma_Protocols Cyclic_Group_Ext Discrete_Log Number_Theory_Aux Uniform_Sampling "HOL-Number_Theory.Cong" begin locale schnorr_base = fixes \ :: "'grp cyclic_group" (structure) assumes prime_order: "prime (order \)" begin lemma order_gt_0 [simp]: "order \ > 0" using prime_order prime_gt_0_nat by blast text\The types for the \\\-protocol.\ type_synonym witness = "nat" type_synonym rand = nat type_synonym 'grp' msg = "'grp'" type_synonym response = nat type_synonym challenge = nat type_synonym 'grp' pub_in = "'grp'" definition R_DL :: "('grp pub_in \ witness) set" where "R_DL = {(h, w). h = \<^bold>g [^] w}" definition init :: "'grp pub_in \ witness \ (rand \ 'grp msg) spmf" where "init h w = do { r \ sample_uniform (order \); return_spmf (r, \<^bold>g [^] r)}" lemma lossless_init: "lossless_spmf (init h w)" by(simp add: init_def) definition "response r w c = return_spmf ((w*c + r) mod (order \))" lemma lossless_response: "lossless_spmf (response r w c)" by(simp add: response_def) definition G :: "('grp pub_in \ witness) spmf" where "G = do { w \ sample_uniform (order \); return_spmf (\<^bold>g [^] w, w)}" lemma lossless_G: "lossless_spmf G" by(simp add: G_def) definition "challenge_space = {..< order \}" definition check :: "'grp pub_in \ 'grp msg \ challenge \ response \ bool" where "check h a e z = (a \ (h [^] e) = \<^bold>g [^] z \ a \ carrier \)" definition S2 :: "'grp \ challenge \ ('grp msg, response) sim_out spmf" where "S2 h e = do { c \ sample_uniform (order \); let a = \<^bold>g [^] c \ (inv (h [^] e)); return_spmf (a, c)}" definition ss_adversary :: "'grp \ ('grp msg, challenge, response) conv_tuple \ ('grp msg, challenge, response) conv_tuple \ nat spmf" where "ss_adversary x c1 c2 = do { let (a, e, z) = c1; let (a', e', z') = c2; return_spmf (if (e > e') then (nat ((int z - int z') * inverse ((e - e')) (order \) mod order \)) else (nat ((int z' - int z) * inverse ((e' - e)) (order \) mod order \)))}" definition "valid_pub = carrier \" text\We now use the Schnorr \\\-protocol use Schnorr to construct a commitment scheme.\ type_synonym 'grp' ck = "'grp'" type_synonym 'grp' vk = "'grp' \ nat" type_synonym plain = "nat" type_synonym 'grp' commit = "'grp'" -type_synonym opening = "nat" +type_synonym "opening" = "nat" text\The adversary we use in the discrete log game to reduce the binding property to the discrete log assumption.\ definition dis_log_\ :: "('grp ck, plain, 'grp commit, opening) bind_adversary \ 'grp ck \ nat spmf" where "dis_log_\ \ h = do { (c, e, z, e', z') \ \ h; _ :: unit \ assert_spmf (e > e' \ \ [e = e'] (mod order \) \ (gcd (e - e') (order \) = 1) \ c \ carrier \); _ :: unit \ assert_spmf (((c \ h [^] e) = \<^bold>g [^] z) \ (c \ h [^] e') = \<^bold>g [^] z'); return_spmf (nat ((int z - int z') * inverse ((e - e')) (order \) mod order \))}" sublocale discrete_log: dis_log \ unfolding dis_log_def by simp end locale schnorr_sigma_protocol = schnorr_base + cyclic_group \ begin sublocale Schnorr_\: \_protocols_base init response check R_DL S2 ss_adversary challenge_space valid_pub apply unfold_locales by(simp add: R_DL_def valid_pub_def; blast) text\The Schnorr \\\-protocol is complete.\ lemma completeness: "Schnorr_\.completeness" proof- have "\<^bold>g [^] y \ (\<^bold>g [^] w') [^] e = \<^bold>g [^] (y + w' * e)" for y e w' :: nat using nat_pow_pow nat_pow_mult by simp then show ?thesis unfolding Schnorr_\.completeness_game_def Schnorr_\.completeness_def by(auto simp add: init_def response_def check_def pow_generator_mod R_DL_def add.commute bind_spmf_const) qed text\The next two lemmas help us rewrite terms in the proof of honest verfier zero knowledge.\ lemma zr_rewrite: assumes z: "z = (x*c + r) mod (order \)" and r: "r < order \" shows "(z + (order \)*x*c - x*c) mod (order \) = r" proof(cases "x = 0") case True then show ?thesis using assms by simp next case x_neq_0: False then show ?thesis proof(cases "c = 0") case True then show ?thesis by (simp add: assms) next case False have cong: "[z + (order \)*x*c = x*c + r] (mod (order \))" by (simp add: cong_def mult.assoc z) hence "[z + (order \)*x*c - x*c = r] (mod (order \))" proof- have "z + (order \)*x*c > x*c" by (metis One_nat_def mult_less_cancel2 n_less_m_mult_n neq0_conv prime_gt_1_nat prime_order trans_less_add2 x_neq_0 False) then show ?thesis by (metis cong add_diff_inverse_nat cong_add_lcancel_nat less_imp_le linorder_not_le) qed then show ?thesis by(simp add: cong_def r) qed qed lemma h_sub_rewrite: assumes "h = \<^bold>g [^] x" and z: "z < order \" shows "\<^bold>g [^] ((z + (order \)*x*c - x*c)) = \<^bold>g [^] z \ inv (h [^] c)" (is "?lhs = ?rhs") proof(cases "x = 0") case True then show ?thesis using assms by simp next case x_neq_0: False then show ?thesis proof- have "(z + order \ * x * c - x * c) = (z + (order \ * x * c - x * c))" using z by (simp add: less_imp_le_nat mult_le_mono) then have lhs: "?lhs = \<^bold>g [^] z \ \<^bold>g [^] ((order \)*x*c - x*c)" by(simp add: nat_pow_mult) have " \<^bold>g [^] ((order \)*x*c - x*c) = inv (h [^] c)" proof(cases "c = 0") case True then show ?thesis by simp next case False hence bound: "((order \)*x*c - x*c) > 0" using assms x_neq_0 prime_gt_1_nat prime_order by auto then have "\<^bold>g [^] ((order \)*x*c- x*c) = \<^bold>g [^] int ((order \)*x*c - x*c)" by (simp add: int_pow_int) also have "... = \<^bold>g [^] int ((order \)*x*c) \ inv (\<^bold>g [^] (x*c))" by (metis bound generator_closed int_ops(6) int_pow_int of_nat_eq_0_iff of_nat_less_0_iff of_nat_less_iff int_pow_diff) also have "... = \<^bold>g [^] ((order \)*x*c) \ inv (\<^bold>g [^] (x*c))" by (metis int_pow_int) also have "... = \<^bold>g [^] ((order \)*x*c) \ inv ((\<^bold>g [^] x) [^] c)" by(simp add: nat_pow_pow) also have "... = \<^bold>g [^] ((order \)*x*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_R_rewrite_grp: fixes x c r :: nat assumes "r < order \" shows "\<^bold>g [^] (((x * c + order \ - r) mod order \ + order \ * x * c - x * c) mod order \) = inv \<^bold>g [^] r" (is "?lhs = ?rhs") proof- have "[(x * c + order \ - r) mod order \ + order \ * x * c - x * c = order \ - r] (mod order \)" proof- have "[(x * c + order \ - r) mod order \ + order \ * x * c - x * c = x * c + order \ - r + order \ * x * c - x * c] (mod order \)" by (smt cong_def One_nat_def add_diff_inverse_nat cong_diff_nat less_imp_le_nat linorder_not_less mod_add_left_eq mult.assoc n_less_m_mult_n prime_gt_1_nat prime_order trans_less_add2 zero_less_diff) hence "[(x * c + order \ - r) mod order \ + order \ * x * c - x * c = order \ - r + order \ * x * c] (mod order \)" using assms by auto thus ?thesis by (simp add: cong_def mult.assoc) qed hence "\<^bold>g [^] ((x * c + order \ - r) mod order \ + order \ * x * c - x * c) = \<^bold>g [^] (order \ - r)" using finite_carrier pow_generator_eq_iff_cong by blast thus ?thesis using neg_power_inverse by (simp add: assms inverse_pow_pow pow_generator_mod) qed lemma hv_zk: assumes "(h,x) \ R_DL" shows "Schnorr_\.R h x c = Schnorr_\.S h c" including monad_normalisation proof- have "Schnorr_\.R h x c = do { r \ sample_uniform (order \); let z = (x*c + r) mod (order \); let a = \<^bold>g [^] ((z + (order \)*x*c - x*c) mod (order \)); return_spmf (a,c,z)}" apply(simp add: Let_def Schnorr_\.R_def init_def response_def) using assms zr_rewrite R_DL_def by(simp cong: bind_spmf_cong_simp) also have "... = do { z \ map_spmf (\ r. (x*c + r) mod (order \)) (sample_uniform (order \)); let a = \<^bold>g [^] ((z + (order \)*x*c - x*c) mod (order \)); return_spmf (a,c,z)}" by(simp add: bind_map_spmf o_def Let_def) also have "... = do { z \ (sample_uniform (order \)); let a = \<^bold>g [^] ((z + (order \)*x*c - x*c)); return_spmf (a,c,z)}" by(simp add: samp_uni_plus_one_time_pad pow_generator_mod) also have "... = do { z \ (sample_uniform (order \)); let a = \<^bold>g [^] z \ inv (h [^] c); return_spmf (a,c,z)}" using h_sub_rewrite assms R_DL_def by(simp cong: bind_spmf_cong_simp) ultimately show ?thesis by(simp add: Schnorr_\.S_def S2_def map_spmf_conv_bind_spmf) qed text\We can now prove that honest verifier zero knowledge holds for the Schnorr \\\-protocol.\ lemma honest_verifier_ZK: shows "Schnorr_\.HVZK" unfolding Schnorr_\.HVZK_def by(auto simp add: hv_zk R_DL_def S2_def check_def valid_pub_def challenge_space_def cyclic_group_assoc) text\It is left to prove the special soundness property. First we prove a lemma we use to rewrite a term in the special soundness proof and then prove the property itself.\ lemma ss_rewrite: assumes "e' < e" and "e < order \" and a_mem:"a \ carrier \" and h_mem: "h \ carrier \" and a: "a \ h [^] e = \<^bold>g [^] z" and a': "a \ h [^] e' = \<^bold>g [^] z'" shows "h = \<^bold>g [^] ((int z - int z') * inverse ((e - e')) (order \) mod int (order \))" proof- have gcd: "gcd (nat (int e - int e') mod (order \)) (order \) = 1" using prime_field by (metis Primes.prime_nat_def assms(1) assms(2) coprime_imp_gcd_eq_1 diff_is_0_eq less_imp_diff_less mod_less nat_minus_as_int not_less schnorr_base.prime_order schnorr_base_axioms) have "a = \<^bold>g [^] z \ inv (h [^] e)" using a a_mem by (simp add: h_mem group.inv_solve_right) moreover have "a = \<^bold>g [^] z' \ inv (h [^] e')" using a' a_mem by (simp add: h_mem group.inv_solve_right) ultimately have "\<^bold>g [^] z \ h [^] e' = \<^bold>g [^] z' \ h [^] e" using h_mem by (metis (no_types, lifting) a a' h_mem a_mem cyclic_group_assoc cyclic_group_commute nat_pow_closed) moreover obtain t :: nat where t: "h = \<^bold>g [^] t" using h_mem generatorE by blast ultimately have "\<^bold>g [^] (z + t * e') = \<^bold>g [^] (z' + t * e) " by (simp add: monoid.nat_pow_mult nat_pow_pow) hence "[z + t * e' = z' + t * e] (mod order \)" using group_eq_pow_eq_mod order_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_iff_lin) hence "[int z - int z' = int t * (int e - int e')] (mod order \)" by (simp add: \[int z - int z' = int t * int e - int t * int e'] (mod int (order \))\ right_diff_distrib) hence "[int z - int z' = int t * (int e - int e')] (mod order \)" by (meson cong_diff cong_mod_left cong_mult cong_refl cong_trans) hence *: "[int z - int z' = int t * (int e - int e')] (mod order \)" using assms by (simp add: int_ops(9) of_nat_diff) hence "[int z - int z' = int t * nat (int e - int e')] (mod order \)" using assms by auto hence **: "[(int z - int z') * fst (bezw ((nat (int e - int e'))) (order \)) = int t * (nat (int e - int e') * fst (bezw ((nat (int e - int e'))) (order \)))] (mod order \)" by (smt \[int z - int z' = int t * (int e - int e')] (mod int (order \))\ assms(1) assms(2) cong_scalar_right int_nat_eq less_imp_of_nat_less mod_less more_arith_simps(11) nat_less_iff of_nat_0_le_iff) hence "[(int z - int z') * fst (bezw ((nat (int e - int e'))) (order \)) = int t * 1] (mod order \)" by (metis (no_types, hide_lams) gcd inverse assms(2) cong_scalar_left cong_trans less_imp_diff_less mod_less mult.comm_neutral nat_minus_as_int) hence "[(int z - int z') * fst (bezw ((nat (int e - int e'))) (order \)) = t] (mod order \)" by simp hence "[ ((int z - int z') * fst (bezw ((nat (int e - int e'))) (order \)))mod order \ = t] (mod order \)" using cong_mod_left by blast hence **: "[nat (((int z - int z') * fst (bezw ((nat (int e - int e'))) (order \)))mod order \) = t] (mod order \)" by (metis Euclidean_Division.pos_mod_sign cong_int_iff int_nat_eq of_nat_0_less_iff order_gt_0) hence "\<^bold>g [^] (nat (((int z - int z') * fst (bezw ((nat (int e - int e'))) (order \)))mod order \)) = \<^bold>g [^] t" using cyclic_group.pow_generator_eq_iff_cong cyclic_group_axioms order_gt_0 order_gt_0_iff_finite by blast thus ?thesis using t by (smt Euclidean_Division.pos_mod_sign discrete_log.order_gt_0 int_pow_def2 nat_minus_as_int of_nat_0_less_iff) qed text\The special soundness property for the Schnorr \\\-protocol.\ lemma special_soundness: shows "Schnorr_\.special_soundness" unfolding Schnorr_\.special_soundness_def by(auto simp add: valid_pub_def ss_rewrite challenge_space_def split_def ss_adversary_def check_def R_DL_def Let_def) text\We are now able to prove that the Schnorr \\\-protocol is a \\\-protocol, the proof comes from the properties of completeness, HVZK and special soundness we have previously proven.\ theorem sigma_protocol: shows "Schnorr_\.\_protocol" by(simp add: Schnorr_\.\_protocol_def completeness honest_verifier_ZK special_soundness) text\Having proven the \\\-protocol property is satisfied we can show the commitment scheme we construct from the Schnorr \\\-protocol has the desired properties. This result comes with very little proof effort as we can instantiate our general proof.\ sublocale Schnorr_\_commit: \_protocols_to_commitments init response check R_DL S2 ss_adversary challenge_space valid_pub G unfolding \_protocols_to_commitments_def \_protocols_to_commitments_axioms_def apply(auto simp add: \_protocols_base_def) apply(simp add: R_DL_def valid_pub_def) apply(auto simp add: sigma_protocol lossless_G lossless_init lossless_response) by(simp add: R_DL_def G_def) lemma "Schnorr_\_commit.abstract_com.correct" by(fact Schnorr_\_commit.commit_correct) lemma "Schnorr_\_commit.abstract_com.perfect_hiding_ind_cpa \" by(fact Schnorr_\_commit.perfect_hiding) lemma rel_adv_eq_dis_log_adv: "Schnorr_\_commit.rel_advantage \ = discrete_log.advantage \" proof- have "Schnorr_\_commit.rel_game \ = discrete_log.dis_log \" unfolding Schnorr_\_commit.rel_game_def discrete_log.dis_log_def by(auto intro: try_spmf_cong bind_spmf_cong[OF refl] simp add: G_def R_DL_def cong_less_modulus_unique_nat group_eq_pow_eq_mod finite_carrier pow_generator_eq_iff_cong) thus ?thesis using Schnorr_\_commit.rel_advantage_def discrete_log.advantage_def by simp qed lemma bind_advantage_bound_dis_log: "Schnorr_\_commit.abstract_com.bind_advantage \ \ discrete_log.advantage (Schnorr_\_commit.adversary \)" using Schnorr_\_commit.bind_advantage rel_adv_eq_dis_log_adv by simp end locale schnorr_asymp = fixes \ :: "nat \ 'grp cyclic_group" assumes schnorr: "\\. schnorr_sigma_protocol (\ \)" begin sublocale schnorr_sigma_protocol "\ \" for \ by(simp add: schnorr) text\The \\\-protocol statement comes easily in the asymptotic setting.\ theorem sigma_protocol: shows "Schnorr_\.\_protocol n" by(simp add: sigma_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: "Schnorr_\_commit.abstract_com.correct n" using Schnorr_\_commit.commit_correct by simp lemma asymp_perfect_hiding: "Schnorr_\_commit.abstract_com.perfect_hiding_ind_cpa n (\ n)" using Schnorr_\_commit.perfect_hiding by blast lemma asymp_computational_binding: assumes "negligible (\ n. discrete_log.advantage n (Schnorr_\_commit.adversary n (\ n)))" shows "negligible (\ n. Schnorr_\_commit.abstract_com.bind_advantage n (\ n))" using Schnorr_\_commit.bind_advantage assms Schnorr_\_commit.abstract_com.bind_advantage_def negligible_le bind_advantage_bound_dis_log by auto end end