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 (simp add: 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