Theory Schnorr_Sigma_Commit
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 = ❙g [^] w}"
definition init :: "'grp pub_in ⇒ witness ⇒ (rand × 'grp msg) spmf"
where "init h w = do {
r ← sample_uniform (order 𝒢);
return_spmf (r, ❙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 (❙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) = ❙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 = ❙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"
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) = ❙g [^] z) ∧ (c ⊗ h [^] e') = ❙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 "❙g [^] y ⊗ (❙g [^] w') [^] e = ❙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 = ❙g [^] x"
and z: "z < order 𝒢"
shows "❙g [^] ((z + (order 𝒢)*x*c - x*c)) = ❙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 = ❙g [^] z ⊗ ❙g [^] ((order 𝒢)*x*c - x*c)"
by(simp add: nat_pow_mult)
have " ❙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 "❙g [^] ((order 𝒢)*x*c- x*c) = ❙g [^] int ((order 𝒢)*x*c - x*c)"
by (metis int_pow_int)
also have "... = ❙g [^] int ((order 𝒢)*x*c) ⊗ inv (❙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 "... = ❙g [^] ((order 𝒢)*x*c) ⊗ inv (❙g [^] (x*c))"
by (metis int_pow_int)
also have "... = ❙g [^] ((order 𝒢)*x*c) ⊗ inv ((❙g [^] x) [^] c)"
by(simp add: nat_pow_pow)
also have "... = ❙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 "❙g [^] (((x * c + order 𝒢 - r) mod order 𝒢 + order 𝒢 * x * c - x * c) mod order 𝒢) = inv ❙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 "❙g [^] ((x * c + order 𝒢 - r) mod order 𝒢 + order 𝒢 * x * c - x * c) = ❙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 = ❙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 = ❙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 = ❙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 = ❙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 = ❙g [^] z"
and a': "a ⊗ h [^] e' = ❙g [^] z'"
shows "h = ❙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 = ❙g [^] z ⊗ inv (h [^] e)"
using a a_mem
by (simp add: h_mem group.inv_solve_right)
moreover have "a = ❙g [^] z' ⊗ inv (h [^] e')"
using a' a_mem
by (simp add: h_mem group.inv_solve_right)
ultimately have "❙g [^] z ⊗ h [^] e' = ❙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 = ❙g [^] t"
using h_mem generatorE by blast
ultimately have "❙g [^] (z + t * e') = ❙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, opaque_lifting) 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 cong_def mod_mod_trivial nat_int of_nat_mod)
hence "❙g [^] (nat (((int z - int z') * fst (bezw ((nat (int e - int e'))) (order 𝒢)))mod order 𝒢)) = ❙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 (simp add: nat_minus_as_int)
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