Session Sigma_Commit_Crypto

Theory Commitment_Schemes

sectionβ€ΉCommitment Schemesβ€Ί

textβ€ΉA commitment scheme is a two party Cryptographic protocol run between a committer and a verifier.
They allow the committer to commit to a chosen value while at a later time reveal the value. A commitment
scheme is composed of three algorithms, the key generation, the commitment and the verification algorithms.
 
The two main properties of commitment schemes are hiding and binding.β€Ί


textβ€ΉHiding is the property that the commitment leaks no information about the committed value, and 
binding is the property that the committer cannot reveal their a different message to the one they
committed to; that is they are bound to their commitment. We follow the game based approach \cite{DBLP:journals/iacr/Shoup04} to
define security. A game is played between an adversary and a challenger.β€Ί

theory Commitment_Schemes imports
  CryptHOL.CryptHOL
begin

subsectionβ€ΉDefining securityβ€Ί
textβ€ΉHere we define the hiding, binding and correctness properties of commitment schemes.β€Ί 

textβ€ΉWe provide the types of the adversaries that take part in the hiding and binding games. We consider 
two variants of the hiding property, one stronger than the other --- thus we provide two hiding adversaries.
The first hiding property we consider is analogous to the IND-CPA property for encryption schemes, the second, 
weaker notion, does not allow the adversary to choose the messages used in the game, instead they are sampled 
from a set distribution.β€Ί

type_synonym ('vk', 'plain', 'commit', 'state) hid_adv = 
  "('vk' β‡’ (('plain' Γ— 'plain') Γ— 'state) spmf)
   Γ— ('commit' β‡’ 'state β‡’ bool spmf)"

type_synonym 'commit' hid = "'commit' β‡’ bool spmf"

type_synonym ('ck', 'plain', 'commit', 'opening')  bind_adversary = 
  "'ck' β‡’ ('commit' Γ— 'plain' Γ— 'opening' Γ— 'plain' Γ— 'opening') spmf"

textβ€ΉWe fix the algorithms that make up a commitment scheme in the locale.β€Ί

locale abstract_commitment =
  fixes key_gen :: "('ck Γ— 'vk) spmf" ― β€Ήoutputs the keys received by the two partiesβ€Ί
    and commit :: "'ck β‡’ 'plain β‡’ ('commit Γ— 'opening) spmf" ― β€Ήoutputs the commitment as well as the opening values sent by the committer in the reveal phaseβ€Ί
    and verify :: "'vk β‡’ 'plain β‡’ 'commit β‡’ 'opening β‡’ bool" 
    and valid_msg :: "'plain β‡’ bool" ― β€Ήchecks whether a message is valid, used in the hiding gameβ€Ί
begin

definition "valid_msg_set = {m. valid_msg m}"

definition lossless :: "('pub_key, 'plain, 'commit, 'state) hid_adv β‡’ bool"
  where "lossless π’œ ⟷
   ((βˆ€pk. lossless_spmf (fst π’œ pk)) ∧
        (βˆ€commit Οƒ. lossless_spmf (snd π’œ commit Οƒ)))"

textβ€ΉThe correct game runs the three algorithms that make up commitment schemes and outputs the output
of the verification algorithm.β€Ί

definition correct_game :: "'plain β‡’ bool spmf"
  where "correct_game m = do {
  (ck, vk) ← key_gen;
  (c,d) ← commit ck m;
  return_spmf (verify vk m c d)}"

lemma   "⟦ lossless_spmf key_gen; lossless_spmf TI;
          β‹€pk m. valid_msg m ⟹ lossless_spmf (commit pk m) ⟧
              ⟹ valid_msg m ⟹ lossless_spmf (correct_game m)"
  by(simp add: lossless_def correct_game_def split_def Let_def)

definition correct where "correct ≑ (βˆ€m. valid_msg m ⟢ spmf (correct_game m) True = 1)"

textβ€ΉThe hiding property is defined using the hiding game. Here the adversary is asked to output two
messages, the challenger flips a coin to decide which message to commit and hand to the adversary.
The adversary's challenge is to guess which commitment it was handed. Note we must check the two 
messages outputted by the adversary are valid.β€Ί

primrec hiding_game_ind_cpa :: "('vk, 'plain, 'commit, 'state) hid_adv β‡’ bool spmf"
  where "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' :: bool ← π’œ2 c Οƒ;
  return_spmf (b' = b)} ELSE coin_spmf"

textβ€ΉThe adversary wins the game if β€Ήb = b'β€Ί.β€Ί

lemma lossless_hiding_game:
  "⟦ lossless π’œ; lossless_spmf key_gen;
     β‹€pk plain. valid_msg plain ⟹ lossless_spmf (commit pk plain) ⟧
  ⟹ lossless_spmf (hiding_game_ind_cpa π’œ)"
  by(auto simp add: lossless_def hiding_game_ind_cpa_def split_def Let_def)

textβ€ΉTo define security we consider the advantage an adversary has of winning the game over a tossing 
a coin to determine their output.β€Ί

definition hiding_advantage_ind_cpa :: "('vk, 'plain, 'commit, 'state) hid_adv β‡’ real"
  where "hiding_advantage_ind_cpa π’œ ≑ Β¦spmf (hiding_game_ind_cpa π’œ) True - 1/2Β¦"

definition perfect_hiding_ind_cpa :: "('vk, 'plain, 'commit, 'state) hid_adv β‡’ bool"
  where "perfect_hiding_ind_cpa π’œ ≑ (hiding_advantage_ind_cpa π’œ = 0)"

  textβ€ΉThe binding game challenges an adversary to bind two messages to the same committed value. Both
opening values and messages are verified with respect to the same committed value, the adversary wins
if the game outputs true. We must check some conditions of the adversaries output are met;
we will always require that β€Ήm β‰  m'β€Ί, other conditions will be dependent on the protocol for example 
we may require group or field membership.β€Ί

definition bind_game :: "('ck, 'plain, 'commit, 'opening) bind_adversary β‡’ bool spmf"
  where "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';
  return_spmf (b ∧ b')} ELSE return_spmf False"

textβ€ΉWe proof the binding game is equivalent to the following game which is easier to work with. In particular 
we assert b and b' in the game and return True.β€Ί

lemma bind_game_alt_def:
  "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"
  (is "?lhs = ?rhs")
proof -
  have "?lhs = TRY do {
      (ck, vk) ← key_gen;
      TRY do {
        (c, m, d, m', d') ← π’œ ck;
        TRY do {
          _ :: unit ← assert_spmf (m β‰  m' ∧ valid_msg m ∧ valid_msg m');
          TRY return_spmf (verify vk m c d ∧ verify vk m' c d') ELSE return_spmf False
        } ELSE return_spmf False
      } ELSE return_spmf False
    } ELSE return_spmf False"
    unfolding split_def bind_game_def
    by(fold try_bind_spmf_lossless2[OF lossless_return_spmf]) simp
  also have "… = TRY do {
      (ck, vk) ← key_gen;
      TRY do {
        (c, m, d, m', d') ← π’œ ck;
        TRY do {
          _ :: unit ← assert_spmf (m β‰  m' ∧ valid_msg m ∧ valid_msg m');
          TRY do {
            _ :: unit ← assert_spmf (verify vk m c d ∧ verify vk m' c d');
            return_spmf True
          } ELSE return_spmf False
        } ELSE return_spmf False
      } ELSE return_spmf False
    } ELSE return_spmf False"
    by(auto simp add: try_bind_assert_spmf try_spmf_return_spmf1 intro!: try_spmf_cong bind_spmf_cong)
  also have "… = ?rhs"
    unfolding split_def Let_def
    by(fold try_bind_spmf_lossless2[OF lossless_return_spmf]) simp
  finally show ?thesis .
qed

lemma lossless_binding_game: "lossless_spmf (bind_game π’œ)" 
  by (simp add: bind_game_def)

definition bind_advantage :: "('ck, 'plain, 'commit, 'opening) bind_adversary β‡’ real"
  where "bind_advantage π’œ ≑ spmf (bind_game π’œ) True"

end

end

Theory Cyclic_Group_Ext

theory Cyclic_Group_Ext imports 
  CryptHOL.CryptHOL
  "HOL-Number_Theory.Cong"
begin

context cyclic_group begin

lemma generator_pow_order: "g [^] order G = 𝟭"
proof(cases "order G > 0")
  case True
  hence fin: "finite (carrier G)" by(simp add: order_gt_0_iff_finite)
  then have [symmetric]: "(Ξ»x. x βŠ— g) ` carrier G = carrier G"
    by(rule endo_inj_surj)(auto simp add: inj_on_multc)
  then have "carrier G = (Ξ» n. g [^] Suc n) ` {..<order G}" using fin 
    by(simp add: carrier_conv_generator image_image)
  then obtain n where n: "𝟭 = g [^] Suc n" "n < order G" by auto
  have "n = order G - 1" using n inj_onD[OF inj_on_generator, of 0 "Suc n"] by fastforce
  with True n show ?thesis by auto
qed simp

lemma generator_pow_mult_order: "g [^] (order G * order G) = 𝟭"
  using generator_pow_order 
  by (metis generator_closed nat_pow_one nat_pow_pow)

lemma pow_generator_mod: "g [^] (k mod order G) = g [^] k"
proof(cases "order G > 0")
  case True
  obtain n where n: "k = n * order G + k mod order G" by (metis div_mult_mod_eq)
  have "g [^] k = (g [^] order G) [^] n βŠ— g [^] (k mod order G)" 
    by(subst n)(simp add: nat_pow_mult nat_pow_pow mult_ac)
  then show ?thesis by(simp add: generator_pow_order)
qed simp

lemma pow_carrier_mod: 
  assumes "g ∈ carrier G"
  shows "g [^] (k mod order G) = g [^] k"
  using assms pow_generator_mod 
  by (metis generatorE generator_closed mod_mult_right_eq nat_pow_pow)

lemma pow_generator_mod_int: "g [^] ((k::int) mod order G) = g [^] k"
proof(cases "order G > 0")
  case True
  obtain n :: int where n: "k = n * order G + k mod order G"   
    by (metis div_mult_mod_eq)
  have "g [^] k = (g [^] order G) [^] n βŠ— g [^] (k mod order G)" 
    apply(subst n)apply(simp add: int_pow_mult int_pow_pow mult_ac)
    by (metis generator_closed int_pow_int int_pow_pow mult.commute)
  then show ?thesis by(simp add: generator_pow_order)
qed simp

lemma pow_generator_eq_iff_cong:
  "finite (carrier G) ⟹ g [^] x = g [^] y ⟷ [x = y] (mod order G)"
  apply(subst (1 2) pow_generator_mod[symmetric])
  by(auto simp add: cong_def order_gt_0_iff_finite intro: inj_onD[OF inj_on_generator])

lemma power_distrib: 
  assumes "h ∈ carrier G" 
  shows "g [^] (e :: nat) βŠ— h [^] e = (g βŠ— h ) [^] e"
(is "?lhs = ?rhs")
proof-
  obtain x :: nat where x: "h = g [^] x" 
    using assms generatorE by blast
  hence "?lhs = g [^] (e * (1 + x))" 
    by (simp add: nat_pow_mult mult.commute nat_pow_pow)
  also have "... = (g [^] (1 + x)) [^] e" 
    by (metis generator_closed mult.commute nat_pow_pow)
  ultimately show ?thesis 
    by (metis x One_nat_def generator_closed l_one monoid.nat_pow_Suc monoid_axioms nat_pow_0 nat_pow_mult)
qed

lemma neg_power_inverse:
  assumes "g ∈ carrier G" 
    and "x < order G"
  shows "g [^] (order G - (x :: nat)) = inv (g [^] x)"
proof-
  have "inv (g [^] x) = g [^] (- int x)"  
    by (simp add: int_pow_int int_pow_neg assms)
  moreover have "g [^] (order G - (x :: nat)) = g [^] (- int x)"
  proof-
    have "g [^] ((order G - (x :: nat)) mod (order G)) = g [^] ((- int x) mod (order G))" 
    proof-
      have "(order G - (x :: nat)) mod (order G) = (- int x) mod (order G)" 
        using assms(2) zmod_zminus1_eq_if by auto
      thus ?thesis 
        by (metis int_pow_int)
    qed
    thus ?thesis 
    proof -
      have f1: "βˆ€a. a [^] int 0 = 𝟭"
        by simp
      have f2: "βˆ€n na. ((na::nat) + n) mod na = n mod na"
        by simp
        have f3: "βˆ€a aa. aa βŠ— a [^] int 0 = aa ∨ aa βˆ‰ carrier G"
          by force
        have f4: "βˆ€i a aa. a [^] int 0 βŠ— aa [^] i = aa [^] (int 0 + i) ∨ aa βˆ‰ carrier G"
          by force
        have "βˆ€n a. a [^] int (n * 0) = a [^] (int 0 + int 0) ∨ a βˆ‰ carrier G"
          by simp
        then have f5: "βˆ€a aa. aa [^] int (order G) = a [^] int 0 ∨ aa βˆ‰ carrier G"
          using f4 f3 f2 f1 by (metis int_pow_closed int_pow_int mod_mult_self2 pow_carrier_mod)
        have "βˆ€n na. int (n - na) = - int na + int n ∨ Β¬ na ≀ n"
          by auto
        then show ?thesis
          using f5 f3 by (metis assms(1) assms(2) int_pow_closed int_pow_int int_pow_mult less_imp_le_nat)
      qed
    qed
  ultimately show ?thesis by simp
qed

lemma int_nat_pow: assumes "a β‰₯ 0" shows "(g [^] (int (a ::nat))) [^] (b::int)  = g [^] (a*b)"
  using assms 
proof(cases "a >0")
  case True 
  show ?thesis
    using int_pow_pow by blast
next case False
  have "(g [^] (int (a ::nat))) [^] (b::int) = 𝟭" using False by simp
  also have "g [^] (a*b) = 𝟭" using False by simp
  ultimately show ?thesis by simp
qed

lemma pow_gen_mod_mult:
  shows"(g [^] (a::nat) βŠ— g [^] (b::nat)) [^] ((c::int)*int (d::nat)) = (g [^] a βŠ— g [^] b) [^] ((c*int d) mod (order G))"
proof-
  have "(g [^] (a::nat) βŠ— g [^] (b::nat)) ∈ carrier G" by simp
  then obtain n :: nat where n: "g [^] n = (g [^] (a::nat) βŠ— g [^] (b::nat))" 
    by (simp add: monoid.nat_pow_mult)
  also obtain r where r: "r = c*int d" by simp
  have 1: "(g [^] (a::nat) βŠ— g [^] (b::nat)) [^] ((c::int)*int (d::nat)) = (g [^] n) [^] r" using n r by simp
  also have 2:"... = (g [^] n) [^] (r mod (order G))" using pow_generator_mod_int pow_generator_mod 
    by (metis int_nat_pow int_pow_int mod_mult_right_eq zero_le)
  also have 3:"... =  (g [^] a βŠ— g [^] b) [^] ((c*int d) mod (order G))" using r n by simp
  ultimately show ?thesis using 1 2 3 by simp
qed

lemma cyclic_group_commute: assumes "a ∈ carrier G" "b ∈ carrier G" shows "a βŠ— b = b βŠ— a"
(is "?lhs = ?rhs")
proof-
  obtain n :: nat where n: "a = g [^] n" using generatorE assms by auto
  also  obtain k :: nat where k: "b = g [^] k" using generatorE assms by auto
  ultimately have "?lhs =  g [^] n βŠ— g [^] k" by simp
  then have "... = g [^] (n + k)" by(simp add: nat_pow_mult)
  then have "... = g [^] (k + n)" by(simp add: add.commute)
  then show ?thesis by(simp add: nat_pow_mult n k)
qed

lemma cyclic_group_assoc: 
  assumes "a ∈ carrier G" "b ∈ carrier G" "c ∈ carrier G"
  shows "(a βŠ— b) βŠ— c = a βŠ— (b βŠ— c)"
(is "?lhs = ?rhs")
proof-
  obtain n :: nat where n: "a = g [^] n" using generatorE assms by auto
  obtain k :: nat where k: "b = g [^] k" using generatorE assms by auto
  obtain j :: nat where j: "c = g [^] j" using generatorE assms by auto 
  have "?lhs = (g [^] n βŠ— g [^] k) βŠ— g [^] j" using n k j by simp
  then have "... = g [^] (n + (k + j))" by(simp add: nat_pow_mult add.assoc)
  then show ?thesis by(simp add: nat_pow_mult n k j)
qed
 
lemma l_cancel_inv: 
  assumes "h ∈ carrier G" 
  shows "(g [^] (a :: nat) βŠ— inv (g [^] a)) βŠ— h = h"
(is "?lhs = ?rhs")
proof-
  have "?lhs = (g [^] int a βŠ— inv (g [^] int a)) βŠ— h" by simp
  then have "... = (g [^] int a βŠ— (g [^] (- a))) βŠ— h" using int_pow_neg[symmetric] by simp
  then have "... = g [^] (int a - a)  βŠ— h" by(simp add: int_pow_mult)
  then have "... = g [^] ((0:: int)) βŠ— h" by simp
  then show ?thesis by (simp add: assms)
qed

lemma inverse_split: 
  assumes "a ∈ carrier G" and "b ∈ carrier G"
  shows "inv (a βŠ— b) = inv a βŠ— inv b"
  by (simp add:  assms comm_group.inv_mult cyclic_group_commute group_comm_groupI)

lemma inverse_pow_pow:
  assumes "a ∈ carrier G"
  shows "inv (a [^] (r::nat)) = (inv a) [^] r"
proof -
  have "a [^] r ∈ carrier G"
    using assms by blast
  then show ?thesis
    by (simp add: assms nat_pow_inv)
qed

lemma l_neq_1_exp_neq_0:
  assumes "l ∈ carrier G" 
    and "l β‰  𝟭" 
    and "l = g [^] (t::nat)" 
  shows "t β‰  0"
proof(rule ccontr)
  assume "Β¬ (t β‰  0)"
  hence "t = 0" by simp
  hence "g [^] t = 𝟭" by simp
  then show "False" using assms by simp
qed

lemma order_gt_1_gen_not_1:
  assumes "order G > 1"
  shows "g β‰  𝟭"
proof(rule ccontr)
  assume "Β¬ g β‰  𝟭"
  hence "g = 𝟭" by simp
  hence g_pow_eq_1: "g [^] n = 𝟭" for n :: nat by simp
  hence "range (λn :: nat. g [^] n) = {𝟭}" by auto
  hence "carrier G βŠ† {𝟭}" using generator by auto
  hence "order G < 1" 
    by (metis inj_onD inj_on_generator lessThan_iff g_pow_eq_1 assms less_one neq0_conv)
  with assms show "False" by simp
qed

lemma power_swap: "((g [^] (Ξ±0::nat)) [^] (r::nat)) = ((g [^] r) [^] Ξ±0)"
(is "?lhs = ?rhs")
proof-
  have "?lhs = g [^] (Ξ±0 * r)" using nat_pow_pow mult.commute by auto
  hence "... = g [^] (r * Ξ±0)" by(metis mult.commute)
  thus ?thesis using nat_pow_pow by auto
qed

lemma gen_power_0:
  fixes r :: nat 
  assumes "g [^] r = 𝟭" 
    and "r < order G"
  shows "r = 0" 
  using assms inj_onD inj_on_generator by fastforce

lemma group_eq_pow_eq_mod: 
  fixes a b :: nat 
  assumes "g [^] a = g [^] b" 
    and "order G > 0"
  shows "[a = b] (mod order G)"
proof(cases "a > b")
  case True
  have "g [^] a βŠ— inv (g [^] b) = 𝟭"
    using assms by simp
  hence "g [^] (a - b) = 𝟭" 
    by (smt True add_Suc_right assms diff_add_inverse generator_closed group.l_cancel_one' group_l_invI l_inv_ex less_imp_Suc_add nat_pow_closed nat_pow_mult)
  hence "g [^] ((a - b) mod (order G)) = 𝟭" using pow_generator_mod by auto
  thus ?thesis using gen_power_0 
    using assms(1) assms(2) order_gt_0_iff_finite pow_generator_eq_iff_cong by blast
next
  case False
  have "g [^] a βŠ— inv (g [^] b) = 𝟭"
    using assms by simp
  hence "g [^] (b - a) = 𝟭" 
    by (metis (no_types, lifting) False Group.group.axioms(1) Units_eq add_diff_inverse_nat assms(1) generator_closed group_l_invI l_inv_ex l_neq_1_exp_neq_0 monoid.Units_l_cancel nat_pow_closed nat_pow_mult r_one)
  hence "g [^] ((b - a) mod (order G)) = 𝟭" using pow_generator_mod by simp
  thus ?thesis using gen_power_0 
    using assms(1) assms(2) order_gt_0_iff_finite pow_generator_eq_iff_cong by blast
qed


end 

end

Theory Discrete_Log

theory Discrete_Log imports 
  CryptHOL.CryptHOL
  Cyclic_Group_Ext
begin 

locale dis_log = 
  fixes 𝒒 :: "'grp cyclic_group" (structure)
  assumes order_gt_0 [simp]: "order 𝒒 > 0"
begin

type_synonym 'grp' dislog_adv = "'grp' β‡’ nat spmf"

type_synonym 'grp' dislog_adv' = "'grp' β‡’ (nat Γ— nat) spmf"

type_synonym 'grp' dislog_adv2 = "'grp' Γ— 'grp' β‡’ nat spmf"

definition dis_log :: "'grp dislog_adv β‡’ bool spmf"
where "dis_log π’œ = TRY do {
  x ← sample_uniform (order 𝒒);
  let h = g [^] x; 
  x'← π’œ h;
  return_spmf ([x = x'] (mod order 𝒒))} ELSE return_spmf False"

definition advantage :: "'grp dislog_adv β‡’ real"
where "advantage π’œ ≑ spmf (dis_log π’œ) True" 

lemma lossless_dis_log: "⟦0 < order 𝒒; βˆ€ h. lossless_spmf (π’œ h)⟧ ⟹ lossless_spmf (dis_log π’œ)"
by(auto simp add:  dis_log_def)

end 

locale dis_log_alt = 
  fixes 𝒒 :: "'grp cyclic_group" (structure)
    and x :: nat
  assumes order_gt_0 [simp]: "order 𝒒 > 0"
begin

sublocale dis_log: dis_log 𝒒
  unfolding dis_log_def by simp

definition "g' = g [^] x"

definition dis_log2 :: "'grp dis_log.dislog_adv' β‡’ bool spmf"
where "dis_log2 π’œ = TRY do {
    w ← sample_uniform (order 𝒒);
    let h = g [^] w;
    (w1',w2') ← π’œ h;
    return_spmf ([w = (w1' + x * w2')]  (mod (order 𝒒)))} ELSE return_spmf False"

definition advantage2 :: "'grp dis_log.dislog_adv' β‡’ real"
where "advantage2 π’œ ≑ spmf (dis_log2 π’œ) True" 

definition adversary2 :: "('grp β‡’ (nat Γ— nat) spmf) β‡’ 'grp β‡’ nat spmf"
  where "adversary2 π’œ h = do {
    (w1,w2) ← π’œ h;
    return_spmf (w1 + x * w2)}"

definition dis_log3 :: "'grp dis_log.dislog_adv2 β‡’ bool spmf"
where "dis_log3 π’œ = TRY do {
    w ← sample_uniform (order 𝒒);
    let (h,w) = ((g [^] w, g' [^] w), w);
    w' ← π’œ h;
    return_spmf ([w = w'] (mod (order 𝒒)))} ELSE return_spmf False"

definition advantage3 :: "'grp dis_log.dislog_adv2 β‡’ real"
  where "advantage3 π’œ ≑ spmf (dis_log3 π’œ) True" 

definition adversary3:: "'grp dis_log.dislog_adv2 β‡’ 'grp β‡’ nat spmf"
  where "adversary3 π’œ g = do {
    π’œ (g, g [^] x)}"

end 

locale dis_log_alt_reductions = dis_log_alt + cyclic_group 𝒒 
begin

lemma dis_log_adv3:
  shows "advantage3 π’œ = dis_log.advantage (adversary3 π’œ)"
  unfolding dis_log_alt.advantage3_def
  by(simp add: advantage3_def dis_log.advantage_def adversary3_def dis_log.dis_log_def dis_log3_def Let_def g'_def power_swap)

lemma dis_log_adv2:
  shows  "advantage2 π’œ = dis_log.advantage (adversary2 π’œ)"
  unfolding dis_log_alt.advantage2_def
  by(simp add: advantage2_def dis_log2_def dis_log.advantage_def dis_log.dis_log_def adversary2_def split_def)

end 

end

Theory Number_Theory_Aux

theory Number_Theory_Aux imports
  "HOL-Number_Theory.Cong"
  "HOL-Number_Theory.Residues"
begin

abbreviation inverse where "inverse x q ≑ (fst (bezw x q))"

lemma inverse: assumes "gcd x q = 1" 
  shows "[x * inverse x q = 1] (mod q)"
proof-
  have 2: "fst (bezw x q) * x + snd (bezw x q) * int q = 1" 
    using bezw_aux assms int_minus 
    by (metis Num.of_nat_simps(2)) 
  hence 3: "(fst (bezw x q) * x + snd (bezw x q) * int q) mod q = 1 mod q" 
    by (metis assms bezw_aux of_nat_mod)
  hence 4: "(fst (bezw x q) * x) mod q = 1 mod q"
    by simp 
  hence 5:  "[(fst (bezw x q)) * x  = 1] (mod q)" 
    using 2 3 cong_def by force 
  then show ?thesis by(simp add: mult.commute) 
qed

lemma prod_not_prime: 
  assumes "prime (x::nat)" 
    and "prime y" 
    and "x > 2" 
    and "y > 2" 
  shows "Β¬ prime ((x-1)*(y-1))"
  by (metis assms One_nat_def Suc_diff_1 nat_neq_iff numeral_2_eq_2 prime_gt_0_nat prime_product)

lemma ex_inverse:
  assumes coprime: "coprime (e :: nat) ((P-1)*(Q-1))" 
    and "prime P" 
    and "prime Q"   
    and "P β‰  Q" 
  shows "βˆƒ d. [e*d = 1] (mod (P-1)) ∧ d β‰  0"
proof-
  have "coprime e (P-1)" 
    using assms(1) by simp 
  then obtain d where d: "[e*d = 1] (mod (P-1))" 
    using cong_solve_coprime_nat by auto
  then show ?thesis by (metis cong_0_1_nat cong_1 mult_0_right zero_neq_one)
qed

lemma ex_k1_k2:
  assumes coprime: "coprime (e :: nat) ((P-1)*(Q-1))" 
    and " [e*d = 1] (mod (P-1))"
  shows "βˆƒ k1 k2. e*d + k1*(P-1) = 1 + k2*(P-1)"
  by (metis assms(2) cong_iff_lin_nat)
lemma "a > b ⟹int a - int b = int (a - b)" 
  by simp

lemma ex_k_mod:
  assumes coprime: "coprime (e :: nat) ((P-1)*(Q-1))" 
    and "P β‰  Q"
    and "prime P"
    and "prime Q"
    and "d β‰  0"
    and " [e*d = 1] (mod (P-1))"
  shows "βˆƒ k. e*d = 1 + k*(P-1)"
proof-
  have "e > 0"  
    using assms(1) assms(2) prime_gt_0_nat by fastforce
  then have "e*d β‰₯ 1" using assms by simp
  then obtain k where k: "e*d = 1 + k*(P-1)" 
    using assms(6) cong_to_1'_nat by auto
  then show ?thesis
    by simp
qed

lemma fermat_little_theorem:
  assumes "prime (P :: nat)" 
  shows "[x^P = x] (mod P)" 
proof(cases "P dvd x")
  case True
  hence "x mod P = 0" by simp
  moreover have "x ^ P mod P = 0" 
    by (simp add: True assms prime_dvd_power_nat_iff prime_gt_0_nat)
  ultimately show ?thesis 
    by (simp add: cong_def)
next
  case False
  hence "[x ^ (P - 1) = 1] (mod P)" using fermat_theorem assms by blast
  then show ?thesis  
    by (metis Suc_diff_1 assms cong_scalar_left nat_mult_1_right not_gr_zero not_prime_0 power_Suc)
qed

lemma prime_field:
  assumes "prime (q::nat)" 
    and "a < q" 
    and "a β‰  0"
  shows "coprime a q"
  by (meson assms coprime_commute dvd_imp_le linorder_not_le neq0_conv prime_imp_coprime)

end

Theory Uniform_Sampling

theory Uniform_Sampling imports 
  CryptHOL.CryptHOL
  "HOL-Number_Theory.Cong"
begin 

definition sample_uniform_units :: "nat β‡’ nat spmf"
  where "sample_uniform_units q = spmf_of_set ({..< q} - {0})"

lemma set_spmf_sample_uniform_units [simp]:
  "set_spmf (sample_uniform_units q) = {..< q} - {0}" 
  by(simp add: sample_uniform_units_def)

lemma lossless_sample_uniform_units:
  assumes "(p::nat) > 1" 
  shows "lossless_spmf (sample_uniform_units p)" 
  unfolding sample_uniform_units_def
  using assms by auto

lemma weight_sample_uniform_units:
  assumes "(p::nat) > 1" 
  shows "weight_spmf (sample_uniform_units p) = 1"
  using assms lossless_sample_uniform_units 
  by (simp add: lossless_weight_spmfD)

(*General lemma for mapping using sample_uniform*)

lemma one_time_pad': 
  assumes inj_on: "inj_on f ({..<q} - {0})" 
    and sur: "f ` ({..<q} - {0}) = ({..<q} - {0})"  
  shows "map_spmf f (sample_uniform_units q) = (sample_uniform_units q)"
(is "?lhs = ?rhs")
proof-
  have rhs: "?rhs = spmf_of_set (({..<q} - {0}))" 
    by(auto simp add: sample_uniform_units_def)
  also have "map_spmf(Ξ»s. f s) (spmf_of_set ({..<q} - {0})) = spmf_of_set ((Ξ»s. f s) ` ({..<q} - {0}))"
    by(simp add: inj_on)
  also have "f ` ({..<q} - {0}) = ({..<q} - {0})"
    apply(rule endo_inj_surj) by(simp, simp add: sur, simp add: inj_on)
  ultimately show ?thesis using rhs by simp
qed

lemma one_time_pad: 
  assumes inj_on: "inj_on f {..<q}" 
    and sur: "f ` {..<q} = {..<q}"  
  shows "map_spmf f (sample_uniform q) = (sample_uniform q)"
(is "?lhs = ?rhs")
proof-
  have rhs: "?rhs = spmf_of_set ({..< q})" 
    by(auto simp add: sample_uniform_def)
  also have "map_spmf(Ξ»s. f s) (spmf_of_set {..<q}) = spmf_of_set ((Ξ»s. f s) ` {..<q})"
    by(simp add: inj_on)
  also have "f ` {..<q} = {..<q}"
    apply(rule endo_inj_surj) by(simp, simp add: sur, simp add: inj_on)
  ultimately show ?thesis using rhs by simp
qed

(*(y + b)*)

lemma plus_inj_eq: 
  assumes x: "x < q"
    and x': "x' < q" 
    and map: "((y :: nat) + x) mod q = (y + x') mod q"  
shows "x = x'"
proof-
  have "((y :: nat) + x) mod q = (y + x') mod q ⟹ x mod q = x' mod q"
  proof-
    have "((y:: nat) + x) mod q = (y + x') mod q ⟹ [((y:: nat) + x) = (y + x')] (mod q)"
      by(simp add: cong_def)
    moreover have "[((y:: nat) + x) = (y + x')] (mod q) ⟹ [x = x'] (mod q)"
      by (simp add: cong_add_lcancel_nat)
    moreover have "[x = x'] (mod q) ⟹ x mod q = x' mod q"
      by(simp add: cong_def)
    ultimately show ?thesis by(simp add: map)
  qed
  moreover have "x mod q = x' mod q ⟹ x = x'"
    by(simp add: x x')
  ultimately show ?thesis by(simp add: map) 
qed

lemma inj_uni_samp_plus: "inj_on  (Ξ»(b :: nat). (y + b) mod q ) {..<q}" 
  by(simp add: inj_on_def)(auto simp only: plus_inj_eq)

lemma surj_uni_samp_plus: 
  assumes inj: "inj_on  (Ξ»(b :: nat). (y + b) mod q ) {..<q}" 
  shows "(Ξ»(b :: nat). (y + b) mod q) ` {..< q} =  {..< q}" 
  apply(rule endo_inj_surj) using inj by auto

lemma samp_uni_plus_one_time_pad: 
shows "map_spmf (Ξ»b. (y + b) mod q) (sample_uniform q) = sample_uniform q"
  using inj_uni_samp_plus surj_uni_samp_plus one_time_pad by simp

(*x*b*) 

lemma mult_inj_eq: 
  assumes coprime: "coprime x (q::nat)" 
    and y: "y < q" 
    and y': "y' < q" 
    and map: "x * y mod q = x * y' mod q" 
  shows "y = y'"
proof-
  have "x*y mod q = x*y' mod q ⟹ y mod q = y' mod q"
  proof-
    have "x*y mod q = x*y' mod q ⟹ [x*y = x*y'] (mod q)"
      by(simp add: cong_def)
    moreover have "[x*y = x*y'] (mod q) = [y = y'] (mod q)"
      by(simp add: cong_mult_lcancel_nat coprime)
    moreover have "[y = y'] (mod q) ⟹ y mod q = y' mod q"
      by(simp add: cong_def)
    ultimately show ?thesis by(simp add: map)
  qed
  moreover have "y mod q = y' mod q ⟹ y = y'"
    by(simp add: y y')
  ultimately show ?thesis by(simp add: map) 
qed

lemma inj_on_mult: 
  assumes coprime: "coprime x (q::nat)" 
  shows "inj_on (Ξ» b. x*b mod q) {..<q}"
  apply(auto simp add: inj_on_def)
  using coprime by(simp only: mult_inj_eq)

lemma surj_on_mult: 
  assumes coprime: "coprime x (q::nat)" 
    and inj: "inj_on (Ξ» b. x*b mod q) {..<q}"
  shows "(Ξ» b. x*b mod q) ` {..< q} = {..< q}"
  apply(rule endo_inj_surj) using coprime inj by auto

lemma mult_one_time_pad: 
  assumes coprime: "coprime x q" 
  shows "map_spmf (Ξ» b. x*b mod q) (sample_uniform q) = sample_uniform q"
  using inj_on_mult surj_on_mult one_time_pad coprime by simp


lemma inj_on_mult':
  assumes coprime: "coprime x (q::nat)" 
  shows "inj_on (Ξ» b. x*b mod q) ({..<q} - {0})"
  apply(auto simp add: inj_on_def)
  using coprime by(simp only: mult_inj_eq)

lemma surj_on_mult': 
  assumes coprime: "coprime x (q::nat)" 
    and inj: "inj_on (Ξ» b. x*b mod q) ({..<q} - {0})"
  shows "(Ξ» b. x*b mod q) ` ({..<q} - {0}) = ({..<q} - {0})"
proof(rule endo_inj_surj) 
  show " finite ({..<q} - {0})" by auto
  show "(Ξ»b. x * b mod q) ` ({..<q} - {0}) βŠ† {..<q} - {0}"  
  proof-
    obtain nn :: "nat set β‡’ (nat β‡’ nat) β‡’ nat set β‡’ nat" where
      "βˆ€x0 x1 x2. (βˆƒv3. v3 ∈ x2 ∧ x1 v3 βˆ‰ x0) = (nn x0 x1 x2 ∈ x2 ∧ x1 (nn x0 x1 x2) βˆ‰ x0)"
        by moura
    hence 1: "βˆ€N f Na. nn Na f N ∈ N ∧ f (nn Na f N) βˆ‰ Na ∨ f ` N βŠ† Na"
      by (meson image_subsetI)
    have 2: "x * nn ({..<q} - {0}) (Ξ»n. x * n mod q) ({..<q} - {0}) mod q βˆ‰ {..<q} ∨ x * nn ({..<q} - {0}) (Ξ»n. x * n mod q) ({..<q} - {0}) mod q ∈ insert 0 {..<q}"
      by force
    have 3: "(x * nn ({..<q} - {0}) (λn. x * n mod q) ({..<q} - {0}) mod q ∈ insert 0 {..<q} - {0}) = (x * nn ({..<q} - {0}) (λn. x * n mod q) ({..<q} - {0}) mod q ∈ {..<q} - {0})"
      by simp 
    { assume "x * nn ({..<q} - {0}) (Ξ»n. x * n mod q) ({..<q} - {0}) mod q = x * 0 mod q" 
      hence "(0 ≀ q) = (0 = q) ∨ (nn ({..<q} - {0}) (Ξ»n. x * n mod q) ({..<q} - {0}) βˆ‰ {..<q} ∨ nn ({..<q} - {0}) (Ξ»n. x * n mod q) ({..<q} - {0}) ∈ {0}) ∨ nn ({..<q} - {0}) (Ξ»n. x * n mod q) ({..<q} - {0}) βˆ‰ {..<q} - {0} ∨ x * nn ({..<q} - {0}) (Ξ»n. x * n mod q) ({..<q} - {0}) mod q ∈ {..<q} - {0}"
        by (metis antisym_conv1 insertCI lessThan_iff local.coprime mult_inj_eq) } 
    moreover
    { assume "0 β‰  x * nn ({..<q} - {0}) (Ξ»n. x * n mod q) ({..<q} - {0}) mod q"
      moreover 
      { assume "x * nn ({..<q} - {0}) (Ξ»n. x * n mod q) ({..<q} - {0}) mod q ∈ insert 0 {..<q} ∧ x * nn ({..<q} - {0}) (Ξ»n. x * n mod q) ({..<q} - {0}) mod q βˆ‰ {0}"
        hence "(Ξ»n. x * n mod q) ` ({..<q} - {0}) βŠ† {..<q} - {0}"
          using 3 1 by (meson Diff_iff) } 
      ultimately have "(Ξ»n. x * n mod q) ` ({..<q} - {0}) βŠ† {..<q} - {0} ∨ (0 ≀ q) = (0 = q)"
        using 2 by (metis antisym_conv1 lessThan_iff mod_less_divisor singletonD) } 
    ultimately have "(Ξ»n. x * n mod q) ` ({..<q} - {0}) βŠ† {..<q} - {0} ∨ nn ({..<q} - {0}) (Ξ»n. x * n mod q) ({..<q} - {0}) βˆ‰ {..<q} - {0} ∨ x * nn ({..<q} - {0}) (Ξ»n. x * n mod q) ({..<q} - {0}) mod q ∈ {..<q} - {0}"
      by force 
    thus "(Ξ»n. x * n mod q) ` ({..<q} - {0}) βŠ† {..<q} - {0}"
      using 1 by meson 
  qed
  show "inj_on (Ξ»b. x * b mod q) ({..<q} - {0})" 
    using inj by blast
qed

lemma mult_one_time_pad':
  assumes coprime: "coprime x q" 
  shows "map_spmf (Ξ» b. x*b mod q) (sample_uniform_units q) = sample_uniform_units q"
  using inj_on_mult' surj_on_mult' one_time_pad' coprime by simp

(*y + x*b*)

lemma samp_uni_add_mult: 
  assumes coprime: "coprime x (q::nat)" 
    and x': "x' < q" 
    and y': "y' < q" 
    and map: "(y + x * x') mod q = (y + x * y') mod q" 
  shows "x' = y'"
proof-
  have "(y + x * x') mod q = (y + x * y') mod q ⟹ x' mod q = y' mod q"
  proof-
  have "(y + x * x') mod q = (y + x * y') mod q ⟹ [y + x*x' = y + x *y'] (mod q)"
    using cong_def by blast
  moreover have "[y + x*x' = y + x *y'] (mod q) ⟹ [x' = y'] (mod q)"
    by(simp add: cong_add_lcancel_nat)(simp add: coprime cong_mult_lcancel_nat)
  ultimately show ?thesis by(simp add: cong_def map)
  qed
  moreover have "x' mod q = y' mod q ⟹ x' = y'"
    by(simp add: x' y')
  ultimately show ?thesis by(simp add: map)
qed

lemma inj_on_add_mult: 
  assumes coprime: "coprime x (q::nat)" 
  shows "inj_on (Ξ» b. (y + x*b) mod q) {..<q}"
  apply(auto simp add: inj_on_def)
  using coprime by(simp only: samp_uni_add_mult)

lemma surj_on_add_mult: 
  assumes coprime: "coprime x (q::nat)" 
    and inj: "inj_on (Ξ» b. (y + x*b) mod q) {..<q}" 
  shows "(Ξ» b. (y + x*b) mod q) ` {..< q} = {..< q}" 
  apply(rule endo_inj_surj) using coprime inj by auto

lemma add_mult_one_time_pad: 
  assumes coprime: "coprime x q" 
  shows "map_spmf (Ξ» b. (y + x*b) mod q) (sample_uniform q) = (sample_uniform q)"
  using inj_on_add_mult surj_on_add_mult one_time_pad coprime by simp

(*(y - b) *)

lemma inj_on_minus: "inj_on  (Ξ»(b :: nat). (y + (q - b)) mod q ) {..<q}"
proof(unfold inj_on_def; auto)
  fix x :: nat and y' :: nat
  assume x: "x < q"
  assume y': "y' < q"
  assume map: "(y + q - x) mod q = (y + q - y') mod q"
  have "βˆ€n na p. βˆƒnb. βˆ€nc nd pa. (Β¬ (nc::nat) < nd ∨ Β¬ pa (nc - nd) ∨ pa 0) ∧ (Β¬ p (0::nat) ∨ p (n - na) ∨ na + nb = n)"
    by (metis (no_types) nat_diff_split)
  hence "¬ y < y' - q ∧ ¬ y < x - q"
    using y' x by (metis add.commute less_diff_conv not_add_less2)
  hence "βˆƒn. (y' + n) mod q = (n + x) mod q"
    using map by (metis add.commute add_diff_inverse_nat less_diff_conv mod_add_left_eq)
  thus "x = y'" 
    by (metis plus_inj_eq  x y' add.commute)
qed

lemma surj_on_minus: 
  assumes inj: "inj_on  (Ξ»(b :: nat). (y + (q - b)) mod q ) {..<q}" 
  shows "(Ξ»(b :: nat). (y + (q - b)) mod q) ` {..< q} = {..< q}"
  apply(rule endo_inj_surj) using inj by auto

lemma samp_uni_minus_one_time_pad: 
  shows "map_spmf(Ξ» b. (y + (q - b)) mod q) (sample_uniform q) = sample_uniform q"
  using inj_on_minus surj_on_minus one_time_pad by simp

lemma not_coin_spmf: "map_spmf (Ξ» a. Β¬ a) coin_spmf = coin_spmf" 
proof-
  have "inj_on Not {True, False}" 
    by simp
  moreover have  "Not ` {True, False} = {True, False}" 
    by auto 
  ultimately show ?thesis using one_time_pad 
    by (simp add: UNIV_bool)
qed

lemma xor_uni_samp: "map_spmf(Ξ» b. y βŠ• b) (coin_spmf) = map_spmf(Ξ» b. b) (coin_spmf)"
  (is "?lhs = ?rhs")
proof-
  have rhs: "?rhs = spmf_of_set {True, False}"
    by (simp add: UNIV_bool insert_commute)
  also have "map_spmf(Ξ» b. y βŠ• b) (spmf_of_set {True, False}) = spmf_of_set((Ξ» b. y βŠ• b) ` {True, False})"
    by (simp add: xor_def)
  also have "(Ξ» b. xor y b) ` {True, False} = {True, False}"
    using xor_def by auto
  finally show ?thesis using rhs by(simp)
qed

lemma ped_inv_mapping:
  assumes "(a::nat) < q"
    and "[m β‰  0] (mod q)"
  shows "map_spmf (Ξ» d. (d + a * (m::nat)) mod q) (sample_uniform q) = map_spmf (Ξ» d. (d + q * m - a * m) mod q) (sample_uniform q)"
(is "?lhs = ?rhs")
proof-
  have ineq: "q * m - a * m > 0" 
    using assms gr0I by force
  have "?lhs = map_spmf (Ξ» d. (a * m + d) mod q) (sample_uniform q)" 
    using add.commute by metis
  also have "... = sample_uniform q"
    using samp_uni_plus_one_time_pad by simp
  also have "... = map_spmf (Ξ» d. ((q * m - a * m) + d) mod q) (sample_uniform q)"
    using ineq samp_uni_plus_one_time_pad by metis
  ultimately show ?thesis 
    using add.commute ineq  
    by (simp add: Groups.add_ac(2))
qed

end

Theory Pedersen

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"

definition key_gen :: "('grp ck Γ— 'grp vk) spmf"
where 
  "key_gen = do {
    x :: nat ← sample_uniform (order 𝒒);
    let h = 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 = (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 = (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 = (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 = g [^] d βŠ— h [^] m ∧ c = 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: " g [^] d' βŠ— (g [^] y) [^] m' = g [^] d βŠ— (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 "g [^] (d + y * m) = 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 "g [^] d βŠ— (g [^] y) [^] m = g [^] d' βŠ— (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 = 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 = ((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 = (g [^] x);
    ((m0, m1), Οƒ) ← π’œ1 h;
    _ :: unit ← assert_spmf (valid_msg m0 ∧ valid_msg m1);
    b ← coin_spmf;  
    z ← map_spmf (Ξ»z.  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 = (g [^] x);
    ((m0, m1), Οƒ) ← π’œ1 h;
    _ :: unit ← assert_spmf (valid_msg m0 ∧ valid_msg m1);
    b ← coin_spmf;  
    z ← map_spmf (Ξ»z. 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 = (g [^] x);
    ((m0, m1), Οƒ) ← π’œ1 h;
    _ :: unit ← assert_spmf (valid_msg m0 ∧ valid_msg m1);
    z ← map_spmf (Ξ»z.  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') ← π’œ (g [^] x);
    _ :: unit ← assert_spmf (m β‰  m' ∧ valid_msg m ∧ valid_msg m'); 
    _ :: unit ← assert_spmf (c = g [^] d βŠ—  (g [^] x) [^] m ∧ c = g [^] d' βŠ— (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') ← π’œ (g [^] x);
    _ :: unit ← assert_spmf (m β‰  m' ∧ valid_msg m ∧ valid_msg m'); 
    _ :: unit ← assert_spmf (c = g [^] d βŠ—  (g [^] x) [^] m ∧ c = g [^] d' βŠ— (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

Theory Rivest

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"

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 ∩ {..<q}) ≀ 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

Theory Sigma_Protocols

sectionβ€Ήβ€ΉΞ£β€Ί-Protocolsβ€Ί

textβ€Ήβ€ΉΞ£β€Ί-protocols were first introduced as an abstract notion by Cramer \cite{Cramerthesis}. 
We point the reader to \cite{sigma_protocols} for a good introduction to the primitive as well as informal proofs
of many of the constructions we formalise in this work. In particular the construction of commitment schemes from 
β€ΉΞ£β€Ί-protocols and the construction of compound AND and OR statements.

In this section we define β€ΉΞ£β€Ί-protocols then provide a general proof that they can be used to construct commitment schemes.
Defining security for β€ΉΞ£β€Ί-protocols uses a mixture of the game-based and simulation-based paradigms. The honest verifier 
zero knowledge property is considered using simulation-based proof, thus we follow the follow the simulation-based formalisation 
of \cite{DBLP:journals/afp/AspinallB19} and \cite{DBLP:conf/itp/Butler0G17}.β€Ί

subsectionβ€ΉDefining β€ΉΞ£β€Ί-protocolsβ€Ί

theory Sigma_Protocols imports
  CryptHOL.CryptHOL
  Commitment_Schemes
begin

type_synonym ('msg', 'challenge', 'response') conv_tuple = "('msg' Γ— 'challenge' Γ— 'response')"

type_synonym ('msg','response') sim_out = "('msg' Γ— 'response')"

type_synonym ('pub_input', 'msg', 'challenge', 'response', 'witness') prover_adversary 
                  = "'pub_input' β‡’ ('msg', 'challenge', 'response') conv_tuple 
                        β‡’ ('msg', 'challenge', 'response') conv_tuple β‡’ 'witness' spmf"

locale Ξ£_protocols_base =
  fixes init :: "'pub_input β‡’ 'witness β‡’ ('rand Γ— 'msg) spmf" ― β€Ήinitial message in β€ΉΞ£β€Ί-protocolβ€Ί
    and response :: "'rand β‡’ 'witness β‡’ 'challenge  β‡’ 'response spmf" 
    and check :: "'pub_input β‡’ 'msg β‡’ 'challenge β‡’ 'response β‡’ bool"
    and Rel :: "('pub_input Γ— 'witness) set" ― β€ΉThe relation the β€ΉΞ£β€Ί protocol is considered overβ€Ί
    and S_raw :: "'pub_input β‡’ 'challenge β‡’ ('msg, 'response) sim_out spmf" ― β€ΉSimulator for the HVZK propertyβ€Ί
    and π’œss :: "('pub_input, 'msg, 'challenge, 'response, 'witness) prover_adversary" ― β€ΉSpecial soundness adversaryβ€Ί
    and challenge_space :: "'challenge set" ― β€ΉThe set of valid challengesβ€Ί
    and valid_pub :: "'pub_input set"
  assumes domain_subset_valid_pub: "Domain Rel βŠ† valid_pub"
begin

lemma assumes "x ∈ Domain Rel" shows "βˆƒ w. (x,w) ∈ Rel"
  using assms by auto

textβ€ΉThe language defined by the relation is the set of all public inputs such that there exists a witness that satisfies the relation.β€Ί 

definition "L ≑ {x. βˆƒ w. (x, w) ∈ Rel}"

textβ€ΉThe first property of β€ΉΞ£β€Ί-protocols we consider is completeness, we define a probabilistic programme 
that runs the components of the protocol and outputs the boolean defined by the check algorithm.β€Ί

definition completeness_game :: "'pub_input β‡’ 'witness β‡’ 'challenge β‡’ bool spmf"
  where "completeness_game h w e = do {
    (r, a) ← init h w;
    z ← response r w e;
    return_spmf (check h a e z)}" 

textβ€ΉWe define completeness as the probability that the completeness-game returns true for all challenges assuming the relation holds on β€Ήhβ€Ί and β€Ήwβ€Ί.β€Ί

definition "completeness ≑ (βˆ€ h w e . (h,w) ∈ Rel ⟢ e ∈ challenge_space ⟢ spmf (completeness_game h w e) True = 1)"

textβ€ΉSecond we consider the honest verifier zero knowledge property (HVZK). To reason about this we construct the real view of the 
β€ΉΞ£β€Ί-protocol given a challenge β€Ήeβ€Ί as input.β€Ί

definition R :: "'pub_input β‡’ 'witness β‡’ 'challenge β‡’ ('msg, 'challenge, 'response) conv_tuple spmf"
  where "R h w e = do { 
    (r,a) ← init h w;
    z ← response r w e;
    return_spmf (a,e,z)}"

definition S where "S h e = map_spmf (Ξ» (a, z). (a, e, z)) (S_raw h e)"

lemma lossless_S_raw_imp_lossless_S: "lossless_spmf (S_raw h e) ⟢ lossless_spmf (S h e)"
  by(simp add: S_def)

textβ€ΉThe HVZK property requires that the simulator's output distribution is equal to the real views output distribution.β€Ί 

definition "HVZK ≑ (βˆ€e ∈ challenge_space. 
                      (βˆ€(h, w)∈Rel. R h w e = S h e)
                        ∧ (βˆ€h ∈ valid_pub. βˆ€(a, z) ∈ set_spmf (S_raw h e). check h a e z))"

textβ€ΉThe final property to consider is that of special soundness. This says that given two valid transcripts such that the challenges 
are not equal there exists an adversary β€Ήπ’œssβ€Ί that can output the witness.β€Ί  

definition "special_soundness ≑ (βˆ€ h e e' a z z'. h ∈ valid_pub ⟢ e ∈ challenge_space ⟢ e' ∈ challenge_space ⟢  e β‰  e' 
              ⟢ check h a e z ⟢ check h a e' z' ⟢ (lossless_spmf (π’œss h (a,e,z) (a, e', z')) ∧ 
                  (βˆ€w'∈set_spmf (π’œss h (a,e,z) (a,e',z')). (h,w') ∈ Rel)))"

lemma special_soundness_alt:
  "special_soundness ⟷
      (βˆ€ h a e z e' z'. e ∈ challenge_space ⟢ e' ∈ challenge_space ⟢ h ∈ valid_pub 
          ⟢ e β‰  e' ⟢ check h a e z ∧ check h a e' z' 
              ⟢ bind_spmf (π’œss h (a,e,z) (a,e',z')) (Ξ» w'. return_spmf ((h,w') ∈ Rel)) = return_spmf True)"
  apply(auto simp add: special_soundness_def map_spmf_conv_bind_spmf[symmetric] map_pmf_eq_return_pmf_iff in_set_spmf lossless_iff_set_pmf_None)
  apply(metis Domain.DomainI in_set_spmf not_Some_eq)
  using Domain.intros by blast +

definition "Ξ£_protocol ≑ completeness ∧ special_soundness ∧ HVZK"

textβ€ΉGeneral lemmasβ€Ί

lemma lossless_complete_game: 
  assumes lossless_init: "βˆ€ h w. lossless_spmf (init h w)"
    and lossless_response: "βˆ€ r w e. lossless_spmf (response r w e)"
  shows "lossless_spmf (completeness_game h w e)"
  by(simp add: completeness_game_def lossless_init lossless_response split_def)

lemma complete_game_return_true:
  assumes "(h,w) ∈ Rel" 
    and "completeness"
    and lossless_init: "βˆ€ h w. lossless_spmf (init h w)"
    and lossless_response: "βˆ€ r w e. lossless_spmf (response r w e)"
    and "e ∈ challenge_space"
  shows "completeness_game h w e = return_spmf True"  
proof -
  have "spmf (completeness_game h w e) True = spmf (return_spmf True) True"
    using assms Ξ£_protocol_def completeness_def by fastforce
  then have "completeness_game h w e = return_spmf True"
    by (metis (full_types) lossless_complete_game lossless_init lossless_response lossless_return_spmf spmf_False_conv_True spmf_eqI)
  then show ?thesis 
    by (simp add: completeness_game_def)
qed 

lemma HVZK_unfold1:
  assumes "Ξ£_protocol" 
  shows "βˆ€ h w e. (h,w) ∈ Rel ⟢ e ∈ challenge_space ⟢ R h w e = S h e" 
  using assms by(auto simp add: Ξ£_protocol_def HVZK_def)

lemma HVZK_unfold2:
  assumes "Ξ£_protocol" 
  shows "βˆ€ h e out. e ∈ challenge_space ⟢ h ∈ valid_pub ⟢ out ∈ set_spmf (S_raw h e) ⟢ check h (fst out) e (snd out)"
  using assms by(auto simp add: Ξ£_protocol_def HVZK_def split_def)

lemma HVZK_unfold2_alt:
  assumes "Ξ£_protocol" 
  shows "βˆ€ h a e z. e ∈ challenge_space ⟢ h ∈ valid_pub ⟢ (a,z) ∈ set_spmf (S_raw h e) ⟢ check h a e z"
  using assms by(fastforce simp add: Ξ£_protocol_def HVZK_def)

end

subsectionβ€ΉCommitments from β€ΉΞ£β€Ί-protocolsβ€Ί

textβ€ΉIn this section we provide a general proof that β€ΉΞ£β€Ί-protocols can be used to construct commitment schemes. 
We follow  the construction given by Damgard in \cite{sigma_protocols}.β€Ί

locale Ξ£_protocols_to_commitments = Ξ£_protocols_base init response check Rel S_raw π’œss challenge_space valid_pub
  for init :: "'pub_input β‡’ 'witness β‡’ ('rand Γ— 'msg) spmf"
    and response :: "'rand β‡’ 'witness β‡’ 'challenge β‡’ 'response spmf"
    and check :: "'pub_input β‡’ 'msg β‡’ 'challenge β‡’ 'response β‡’ bool"
    and Rel :: "('pub_input Γ— 'witness) set"
    and S_raw :: "'pub_input β‡’ 'challenge β‡’ ('msg, 'response) sim_out spmf"
    and π’œss :: "('pub_input, 'msg, 'challenge, 'response, 'witness) prover_adversary"
    and challenge_space :: "'challenge set"
    and valid_pub :: "'pub_input set"
    and G :: "('pub_input Γ— 'witness) spmf" ― β€Ήgenerates pairs that satisfy the relationβ€Ί
    +
  assumes Ξ£_prot: "Ξ£_protocol" ― β€Ήassume we have a β€ΉΞ£β€Ί-protocolβ€Ί
    and set_spmf_G_rel [simp]: "(h,w) ∈ set_spmf G ⟹ (h,w) ∈ Rel" ― β€Ήthe generator has the desired propertyβ€Ί  
    and lossless_G: "lossless_spmf G"
    and lossless_init: "lossless_spmf (init h w)"
    and lossless_response: "lossless_spmf (response r w e)"
begin

lemma set_spmf_G_domain_rel [simp]: "(h,w) ∈ set_spmf G ⟹ h ∈ Domain Rel" 
  using set_spmf_G_rel by fast

lemma set_spmf_G_L [simp]: "(h,w) ∈ set_spmf G ⟹ h ∈ L"
  by (metis mem_Collect_eq set_spmf_G_rel L_def)

textβ€ΉWe define the advantage associated with the hard relation, this is used in the proof of the binding property where
we reduce the binding advantage to the relation advantage.β€Ί

definition rel_game :: "('pub_input β‡’ 'witness spmf) β‡’ bool spmf"
  where "rel_game π’œ = TRY do {
    (h,w) ← G;
    w' ← π’œ h;
    return_spmf ((h,w') ∈ Rel)} ELSE return_spmf False"

definition rel_advantage :: "('pub_input β‡’ 'witness spmf) β‡’ real"
  where "rel_advantage π’œ ≑ spmf (rel_game π’œ) True"

textβ€ΉWe now define the algorithms that define the commitment scheme constructed from a β€ΉΞ£β€Ί-protocol.β€Ί

definition key_gen :: "('pub_input Γ—  ('pub_input Γ— 'witness)) spmf"
  where 
   "key_gen = do {
    (x,w) ← G;
    return_spmf (x, (x,w))}"

definition commit :: "'pub_input β‡’ 'challenge β‡’ ('msg Γ—  'response) spmf"
  where
    "commit x e = do {
    (a,e,z) ← S x e;
    return_spmf (a, z)}"

definition verify :: "('pub_input Γ— 'witness) β‡’ 'challenge β‡’ 'msg β‡’  'response β‡’ bool"
  where "verify x e a z = (check (fst x) a e z)"

textβ€ΉWe allow the adversary to output any message, so this means the type constraint is enoughβ€Ί

definition "valid_msg m = (m ∈ challenge_space)"

textβ€ΉShowing the construction of a commitment scheme from a β€ΉΞ£β€Ί-protocol is a  valid commitment scheme is trivial.β€Ί

sublocale abstract_com: abstract_commitment key_gen commit verify valid_msg .

paragraphβ€ΉCorrectnessβ€Ί

lemma commit_correct:
  shows "abstract_com.correct"
  including monad_normalisation
proof-
  have "βˆ€ m ∈ challenge_space. abstract_com.correct_game m = return_spmf True"
  proof
    fix m
    assume m: "m ∈ challenge_space"
    show "abstract_com.correct_game m = return_spmf True"
    proof-
    have "abstract_com.correct_game m = do {
      (ck, (vk1,vk2)) ← key_gen;
      (a,e,z) ← S ck m;
      return_spmf (check vk1 a m z)}" 
      unfolding abstract_com.correct_game_def
      by(simp add: commit_def verify_def split_def)
    also have "... = do { 
      (x,w) ← G;
      let (ck, (vk1,vk2)) = (x,(x,w));
      (a,e,z) ← S ck m;
      return_spmf (check vk1 a m z)}"
      by(simp add: key_gen_def split_def)
    also have "... = do {
      (x,w) ← G;
      (a,e,z) ← S x m;
      return_spmf (check x a m z)}"
      by(simp add: Let_def)
    also have "... = do {
      (x,w) ← G;
      (a, e,z) ← R x w m;
      return_spmf (check x a m z)}"
      using Ξ£_prot HVZK_unfold1 m
      by(intro bind_spmf_cong bind_spmf_cong[OF refl]; clarsimp?)
    also have "... = do {
      (x,w) ← G;
      (r, a) ← init x w;
      z ← response r w m;
      return_spmf (check x a m z)}"
      by(simp add: R_def split_def)
    also have "... = do {
      (x,w) ← G;
      return_spmf True}"
      apply(intro bind_spmf_cong bind_spmf_cong[OF refl]; clarsimp?)
      using complete_game_return_true lossless_init lossless_response Ξ£_prot Ξ£_protocol_def
      by(simp add: split_def completeness_game_def Ξ£_protocols_base.Ξ£_protocol_def m cong: bind_spmf_cong_simp)
    ultimately show "abstract_com.correct_game m = return_spmf True"
      by(simp add: bind_spmf_const lossless_G lossless_weight_spmfD split_def)
  qed
qed
  thus ?thesis 
    using abstract_com.correct_def abstract_com.valid_msg_set_def valid_msg_def by simp
qed

paragraphβ€ΉThe hiding propertyβ€Ί

textβ€ΉWe first show we have perfect hiding with respect to the hiding game that allows the adversary to choose
the messages that are committed to, this is akin to the ind-cpa game for encryption schemes.β€Ί

lemma perfect_hiding:
  shows "abstract_com.perfect_hiding_ind_cpa π’œ"
  including monad_normalisation
proof-
  obtain π’œ1 π’œ2 where [simp]: "π’œ = (π’œ1, π’œ2)" by(cases π’œ)
  have "abstract_com.hiding_game_ind_cpa (π’œ1, π’œ2) = TRY do {
    (x,w) ← G;
    ((m0, m1), Οƒ) ← π’œ1 (x,w);
    _ :: unit ← assert_spmf (valid_msg m0 ∧ valid_msg m1);
    b ← coin_spmf; 
    (a,e,z) ← S x (if b then m0 else m1);
    b' ← π’œ2 a Οƒ;
    return_spmf (b' = b)} ELSE coin_spmf"
    by(simp add: abstract_com.hiding_game_ind_cpa_def commit_def; simp add: key_gen_def split_def)
  also have "... = TRY do {
    (x,w) ← G;
    ((m0, m1), Οƒ) ← π’œ1 (x,w);
    _ :: unit ← assert_spmf (valid_msg m0 ∧ valid_msg m1);
    b :: bool ← coin_spmf; 
    (a,e,z) ← R x w (if b then m0 else m1);
    b' :: bool ← π’œ2 a Οƒ;
    return_spmf (b' = b)} ELSE coin_spmf"
    apply(intro try_spmf_cong bind_spmf_cong[OF refl]; clarsimp?)+
    by(simp add: Ξ£_prot  HVZK_unfold1 valid_msg_def)
  also have "... = TRY do {
    (x,w) ← G;
    ((m0, m1), Οƒ) ← π’œ1 (x,w);
    _ :: unit ← assert_spmf (valid_msg m0 ∧ valid_msg m1);
    b ← coin_spmf; 
    (r,a) ← init x w;
    z :: 'response ← response r w (if b then m0 else m1);
    guess :: bool ← π’œ2 a Οƒ;
    return_spmf(guess = b)} ELSE coin_spmf"
    using Ξ£_protocols_base.R_def 
    by(simp add: bind_map_spmf o_def R_def split_def)
  also have  "... = TRY do {
    (x,w) ← G;
    ((m0, m1), Οƒ) ← π’œ1 (x,w);
    _ :: unit ← assert_spmf (valid_msg m0 ∧ valid_msg m1);
    b ← coin_spmf; 
    (r,a) ← init x w;
    guess :: bool ← π’œ2 a Οƒ;
    return_spmf(guess = b)} ELSE coin_spmf"
    by(simp add: bind_spmf_const lossless_response lossless_weight_spmfD)
  also have  "... = TRY do {
    (x,w) ← G;
    ((m0, m1), Οƒ) ← π’œ1 (x,w);
    _ :: unit ← assert_spmf (valid_msg m0 ∧ valid_msg m1);
    (r,a) ← init x w;
    guess :: bool ← π’œ2 a Οƒ;
    map_spmf( (=) guess) coin_spmf} ELSE coin_spmf"
    apply(simp add: map_spmf_conv_bind_spmf)
    by(simp add: split_def)
  also have "... = coin_spmf" 
    by(auto simp add: map_eq_const_coin_spmf try_bind_spmf_lossless2' Let_def split_def bind_spmf_const scale_bind_spmf weight_spmf_le_1 scale_scale_spmf)
  ultimately have "spmf (abstract_com.hiding_game_ind_cpa π’œ) True = 1/2"
    by(simp add: spmf_of_set)
  thus ?thesis
    by (simp add: abstract_com.perfect_hiding_ind_cpa_def abstract_com.hiding_advantage_ind_cpa_def)
qed

textβ€ΉWe reduce the security of the binding property to the relation advantage. To do this we first construct 
an adversary that interacts with the relation game. This adversary succeeds if the binding adversary succeeds.β€Ί

definition adversary :: "('pub_input β‡’ ('msg Γ— 'challenge Γ— 'response Γ— 'challenge Γ— 'response) spmf) β‡’ 'pub_input β‡’ 'witness spmf"
  where "adversary π’œ x = do {
    (c, e, ez, e', ez') ← π’œ x;
    π’œss x (c,e,ez) (c,e',ez')}"

lemma bind_advantage:
  shows "abstract_com.bind_advantage π’œ ≀ rel_advantage (adversary π’œ)"
proof-
  have "abstract_com.bind_game π’œ = TRY do {
  (x,w) ← G;
  (c, m, d, m', d') ← π’œ x;
  _ :: unit ← assert_spmf (m β‰  m' ∧ m ∈ challenge_space ∧ m' ∈ challenge_space);
  let b = check x c m d;
  let b' = check x c m' d';
  _ :: unit ← assert_spmf (b ∧ b'); 
  w' ← π’œss x (c,m, d) (c,m', d');
  return_spmf ((x,w') ∈ Rel)} ELSE return_spmf False"
    unfolding abstract_com.bind_game_alt_def 
    apply(simp add:  key_gen_def verify_def Let_def split_def valid_msg_def)
    apply(intro try_spmf_cong bind_spmf_cong[OF refl]; clarsimp?)+
    using special_soundness_def Ξ£_prot Ξ£_protocol_def special_soundness_alt special_soundness_def set_spmf_G_rel set_spmf_G_domain_rel 
    by (smt basic_trans_rules(31) bind_spmf_cong domain_subset_valid_pub)
  hence "abstract_com.bind_advantage π’œ ≀ spmf (TRY do {
  (x,w) ← G;
  (c, m, d, m', d') ← π’œ x;
  w' ← π’œss x (c,m, d) (c,m', d');
  return_spmf ((x,w') ∈ Rel)} ELSE return_spmf False) True"
    unfolding abstract_com.bind_advantage_def
    apply(simp add: spmf_try_spmf)
    apply(rule ord_spmf_eq_leD)
    apply(rule ord_spmf_bind_reflI;clarsimp)+
    by(simp add: assert_spmf_def)
  thus ?thesis
    by(simp add: rel_game_def adversary_def split_def rel_advantage_def)
qed

end

end

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, 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 "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 (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

Theory Chaum_Pedersen_Sigma_Commit

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' = 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 ((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, 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) = 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 = 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 = 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 "g [^] y βŠ— (g [^] w') [^] e = 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 = 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
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 = g [^] z βŠ— g [^] ((order 𝒒) * w *c - w*c)" 
      by(simp add: nat_pow_mult)
    have " 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 " 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"] * generator_closed int_ops(6) int_pow_neg int_pow_neg_int by presburger

      also have "... = g [^] ((order 𝒒)*w*c) βŠ— inv (g [^] (w*c))"
        by (metis int_pow_int) 
      also have "... = g [^] ((order 𝒒)*w*c) βŠ— inv ((g [^] w) [^] c)"
        by(simp add: nat_pow_pow)
      also have "... = 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' = 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) - 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 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 = (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 = 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 = 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 = 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 = 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 = 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 = 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 = g [^] z"  
    and e': "e' < e"
    and "a βŠ— fst h [^] e' = g [^] z'"
  shows "fst h = 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 = g [^] z βŠ— inv (fst h [^] e)" 
    using assms
    by (simp add: assms inv_solve_right)
  moreover have "a = g [^] z' βŠ— inv (fst h [^] e')" 
    using assms
    by (simp add: assms inv_solve_right)
  ultimately have "g [^] z βŠ— fst h [^] e' = 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 = g [^] t"
    using assms generatorE by blast
  ultimately have "g [^] (z + t * e') = 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 "g [^] (nat ((int z - int z') * fst (bezw (e - e') (order 𝒒)) mod order 𝒒))  = 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 = g [^] z" 
    and "b βŠ— snd h [^] e = g' [^] z"
    and "e' < e" 
    and "a βŠ— fst h [^] e' = 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 = g [^] t"
    using assms(2) generatorE by blast
  ultimately have "g [^] (x * z + t * e') = 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 "g [^] (nat ((int x * (int z - int z')) * fst (bezw (e - e') (order 𝒒)) mod order 𝒒)) = 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 = g [^] t"
    using assms(2) generatorE by blast
  ultimately have "g [^] (x * z + t * e') = 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 "g [^] (int x * (int z - int z') * fst (bezw ((e mod order 𝒒 - e' mod order 𝒒) mod order 𝒒) (order 𝒒))) = 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) = ((g [^] w, g' [^] w), w);
    w' ← π’œ h;
    return_spmf ((fst h = 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) = ((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

Theory Okamoto_Sigma_Commit

subsectionβ€ΉOkamoto β€ΉΞ£β€Ί-protocolβ€Ί

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

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

definition "g' = g [^] x"

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

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

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

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

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

definition init :: "'grp pub_in β‡’ witness β‡’ (rand Γ— 'grp msg) spmf"
  where "init y w = do {
    let (x1,x2) = w; 
    r1 ← sample_uniform (order 𝒒);
    r2 ← sample_uniform (order 𝒒);
    return_spmf ((r1,r2), g [^] r1 βŠ— g' [^] r2)}"

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

definition check :: "'grp pub_in β‡’ 'grp msg β‡’ challenge β‡’ response β‡’ bool"
  where "check h a e z = (g [^] (fst z) βŠ— g' [^] (snd z) = a βŠ— (h [^] e) ∧ a ∈ carrier 𝒒)"

definition R :: "('grp pub_in Γ— witness) set"
  where "R ≑ {(h, w). (h = g [^] (fst w) βŠ— g' [^] (snd w))}"

definition G :: "('grp pub_in Γ— witness) spmf"
  where "G = do {
    w1 ← sample_uniform (order 𝒒);
    w2 ← sample_uniform (order 𝒒);
    return_spmf (g [^] w1 βŠ— g' [^] w2 , (w1,w2))}"

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

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

definition S2 :: "'grp pub_in β‡’ challenge β‡’ ('grp msg, response) sim_out spmf"
  where "S2 h c = do {
    z1 ← sample_uniform  (order 𝒒);
    z2 ← sample_uniform  (order 𝒒);
  let a =  (g [^] z1 βŠ— g' [^] z2) βŠ— (inv h [^] c); 
  return_spmf (a, (z1,z2))}"

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

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

definition "valid_pub = carrier 𝒒"
end

locale okamoto = okamoto_base + cyclic_group 𝒒
begin

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

sublocale Ξ£_protocols_base: Ξ£_protocols_base init response check R S2 ss_adversary challenge_space valid_pub 
  by unfold_locales (auto simp add: R_def valid_pub_def)

lemma "Ξ£_protocols_base.R h w c = R2 h w c"
  by(simp add: Ξ£_protocols_base.R_def R2_def; simp add: init_def split_def response_def)

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

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

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

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

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

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

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

lemma ss_rewrite:
  assumes "h ∈ carrier 𝒒"
    and "a ∈ carrier 𝒒"
    and "e < order 𝒒" 
    and "g [^] z1 βŠ— g' [^] z1' = a βŠ— h [^] e"
    and "e' < e"
    and "g [^] z2 βŠ— g' [^] z2' = a βŠ— h [^] e' "
  shows "h = g [^] ((int z1 - int z2) * fst (bezw (e - e') (order 𝒒)) mod int (order 𝒒)) βŠ— g' [^] ((int z1' - int z2') * fst (bezw (e - e') (order 𝒒)) mod int (order 𝒒))"
proof-
  have gcd: "gcd (e - e') (order 𝒒) = 1"
    using prime_field assms prime_order by simp 
  have "g [^] z1 βŠ— g' [^] z1' βŠ— inv (h [^] e) = a" 
    by (simp add: inv_solve_right' assms)
  moreover have "g [^] z2 βŠ— g' [^] z2' βŠ— inv (h [^] e') = a" 
    by (simp add: assms inv_solve_right')
  ultimately have "g [^] z2 βŠ— g' [^] z2' βŠ— inv (h [^] e') = g [^] z1 βŠ— g' [^] z1' βŠ— inv (h [^] e)"
    using g'_def by (simp add: nat_pow_pow)
  moreover obtain t :: nat where t: "h = g [^] t" 
    using assms generatorE by blast
  ultimately have "g [^] z2 βŠ— g [^] (x * z2') βŠ— g [^] (t * e) = g [^] z1 βŠ— g [^] (x * z1') βŠ— (g [^] (t * e'))" 
    using assms(2) assms(4) cyclic_group_commute m_assoc g'_def nat_pow_pow by auto
  hence "g [^] (z2 + x * z2' + t * e) = g [^] (z1 + x * z1' + t * e')"  
    by (simp add: nat_pow_mult)
  hence "[z2 + x * z2' + t * e = z1 + x * z1' + t * e'] (mod order 𝒒)"
    using group_eq_pow_eq_mod order_gt_0 by blast
  hence "[int z2 + int x * int z2' + int t * int e = int z1 + int x * int z1' + int t * int e'] (mod order 𝒒)"
    using cong_int_iff by force
  hence "[int z1 + int x * int z1' - int z2 - int x * int z2' = int t * int e - int t * int e'] (mod order 𝒒)"
    by (smt cong_diff_iff_cong_0 cong_sym)
  hence "[int z1 + int x * int z1' - int z2 - int x * int z2' = int t * (e - e')] (mod order 𝒒)"
    using int_distrib(4) assms by (simp add: of_nat_diff)
  hence "[(int z1 + int x * int z1' - int z2 - int x * int z2') * fst (bezw (e - e') (order 𝒒)) = int t * (e - e') * fst (bezw (e - e') (order 𝒒))] (mod order 𝒒)"
    using cong_scalar_right by blast
  hence "[(int z1 + int x * int z1' - int z2 - int x * int z2') * fst (bezw (e - e') (order 𝒒)) = int t * ((e - e') * fst (bezw (e - e') (order 𝒒)))] (mod order 𝒒)"
    by (simp add: mult.assoc)
  hence "[(int z1 + int x * int z1' - int z2 - int x * int z2') * fst (bezw (e - e') (order 𝒒)) = int t * 1] (mod order 𝒒)"
    by (metis (no_types, hide_lams) cong_scalar_left cong_trans inverse gcd)
  hence "[(int z1 - int z2 + int x * int z1' - int x * int z2') * fst (bezw (e - e') (order 𝒒)) = int t] (mod order 𝒒)"
    by smt
  hence "[(int z1 - int z2 + int x * (int z1' - int z2')) * fst (bezw (e - e') (order 𝒒)) = int t] (mod order 𝒒)"
    by (simp add: Rings.ring_distribs(4) add_diff_eq)
  hence "[nat ((int z1 - int z2 + int x * (int z1' - int z2')) * fst (bezw (e - e') (order 𝒒)) mod (order 𝒒)) = int t] (mod order 𝒒)"
    by auto
  hence "g [^] (nat ((int z1 - int z2 + int x * (int z1' - int z2')) * fst (bezw (e - e') (order 𝒒)) mod (order 𝒒))) = g [^] t"
    using cong_int_iff finite_carrier pow_generator_eq_iff_cong by blast
  hence "g [^] ((int z1 - int z2 + int x * (int z1' - int z2')) * fst (bezw (e - e') (order 𝒒))) = g [^] t"
    using pow_generator_mod_int by auto
  hence "g [^] ((int z1 - int z2) * fst (bezw (e - e') (order 𝒒)) + int x * (int z1' - int z2') * fst (bezw (e - e') (order 𝒒))) = g [^] t"
    by (metis Rings.ring_distribs(2) t)
  hence "g [^] ((int z1 - int z2) * fst (bezw (e - e') (order 𝒒))) βŠ— g [^] (int x * (int z1' - int z2') * fst (bezw (e - e') (order 𝒒))) = g [^] t"
    using int_pow_mult by auto
  thus ?thesis 
    by (metis (mono_tags, hide_lams) g'_def generator_closed int_pow_int int_pow_pow mod_mult_right_eq more_arith_simps(11) pow_generator_mod_int t)
qed

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

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

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

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

sublocale dis_log: dis_log 𝒒 
  unfolding dis_log_def by simp

sublocale dis_log_alt: dis_log_alt 𝒒 x 
  unfolding dis_log_alt_def 
  by(simp add:)

lemma reduction_to_dis_log:
  shows "okamoto_Ξ£_commit.rel_advantage π’œ = dis_log.advantage (dis_log_alt.adversary2 π’œ)"
proof-
  have exp_rewrite: "g [^] w1 βŠ— g' [^] w2 =  g [^] (w1 + x * w2)" for w1 w2 :: nat
    by (simp add: nat_pow_mult nat_pow_pow g'_def)
  have "okamoto_Ξ£_commit.rel_game π’œ = TRY do {
    w1 ← sample_uniform (order 𝒒);
    w2 ← sample_uniform (order 𝒒);
    let h = (g [^] w1 βŠ— g' [^] w2);
    (w1',w2') ← π’œ h;
    return_spmf (h = g [^] w1' βŠ— g' [^] w2')} ELSE return_spmf False"
    unfolding okamoto_Ξ£_commit.rel_game_def
    by(simp add: Let_def split_def R_def G_def)
  also have "... = TRY do {
    w1 ← sample_uniform (order 𝒒);
    w2 ← sample_uniform (order 𝒒);
    let w = (w1 + x * w2) mod (order 𝒒);
    let h = g [^] w;
    (w1',w2') ← π’œ h;
    return_spmf (h = g [^] w1' βŠ— g' [^] w2')} ELSE return_spmf False"
    using g'_def exp_rewrite pow_generator_mod by simp
  also have "... = TRY do {
    w2 ← sample_uniform (order 𝒒);
    w ← map_spmf (Ξ» w1. (x * w2 + w1) mod (order 𝒒)) (sample_uniform (order 𝒒));
    let h = g [^] w;
    (w1',w2') ← π’œ h;
    return_spmf (h = g [^] w1' βŠ— g' [^] w2')} ELSE return_spmf False"
    including monad_normalisation
    by(simp add: bind_map_spmf o_def Let_def add.commute)
  also have "... = TRY do {
    w2 :: nat ← sample_uniform (order 𝒒);
    w ← sample_uniform (order 𝒒);
    let h = g [^] w;
    (w1',w2') ← π’œ h;
    return_spmf (h = g [^] w1' βŠ— g' [^] w2')} ELSE return_spmf False"
    using samp_uni_plus_one_time_pad add.commute by simp
  also have "... = TRY do {
    w ← sample_uniform (order 𝒒);
    let h = g [^] w;
    (w1',w2') ← π’œ h;
    return_spmf (h = g [^] w1' βŠ— g' [^] w2')} ELSE return_spmf False"
    by(simp add: bind_spmf_const)
  also