Library SSProve.Crypt.examples.Schnorr
From Stdlib Require Import Utf8.
Set Warnings "-notation-overridden,-ambiguous-paths".
From mathcomp Require Import all_ssreflect all_algebra reals distr realsum
fingroup solvable.cyclic prime ssrnat ssreflect ssrfun ssrbool ssrnum
eqtype choice seq.
Set Warnings "notation-overridden,ambiguous-paths".
Unset SsrOldRewriteGoalsOrder. (* remove the line when requiring MathComp >= 2.6 *)
From extructures Require Import ord fset fmap.
From SSProve.Crypt Require Import Package SigmaProtocol.
Set Bullet Behavior "Strict Subproofs".
Set Default Goal Selector "!".
Set Primitive Projections.
Local Open Scope ring_scope.
Local Open Scope group_scope.
Import GRing.Theory.
Import Num.Def.
Import Num.Theory.
Import Order.POrderTheory.
Import PackageNotation.
Module Type GroupParam.
Parameter gT : finGroupType.
Definition ζ : {set gT} := [set : gT].
Parameter g : gT.
Parameter g_gen : ζ = <[g]>.
Parameter prime_order : prime #[g].
End GroupParam.
Module Schnorr (GP : GroupParam).
Import GP.
(* order of g *)
Definition q : nat := #[g].
Module MyParam <: SigmaProtocolParams.
Definition Witness : finType := Finite.clone _ 'Z_q.
Definition Statement : finType := gT.
Definition Message : finType := gT.
Definition Challenge : finType := Finite.clone _ 'Z_q.
Definition Response : finType := Finite.clone _ 'Z_q.
Definition Transcript : finType :=
prod (prod Message Challenge) Response.
Definition w0 : Witness := 0.
Definition R : Statement → Witness → bool :=
(λ (h : Statement) (w : Witness), h == (g ^+ w)).
End MyParam.
Module MyAlg <: SigmaProtocolAlgorithms MyParam.
Import MyParam.
Definition choiceWitness : choice_type := 'fin #|Witness|.
Definition choiceStatement : choice_type := 'fin #|Statement|.
Definition choiceMessage : choice_type := 'fin #|Message|.
Definition choiceChallenge : choice_type := 'fin #|Challenge|.
Definition choiceResponse : choice_type := 'fin #|Response|.
Definition choiceTranscript : choice_type :=
chProd
(chProd (chProd choiceStatement choiceMessage) choiceChallenge)
choiceResponse.
Definition choiceBool := 'fin #|'bool|.
Definition i_witness := #|Witness|.
Definition commit_loc := mkloc 2 (fto 1 : choiceWitness).
Definition Sigma_locs : Locations := [fmap commit_loc].
Definition Simulator_locs : Locations := emptym.
Definition Commit (h : choiceStatement) (w : choiceWitness):
code Sigma_locs [interface] choiceMessage :=
{code
r ← sample uniform i_witness ;;
#put commit_loc := r ;;
ret (fto (g ^+ (otf r)))
}.
Definition Response (h : choiceStatement) (w : choiceWitness) (a : choiceMessage) (e : choiceChallenge) :
code Sigma_locs [interface] choiceResponse :=
{code
r ← get commit_loc ;;
ret (fto (otf r + otf e × otf w))
}.
Definition Simulate (h : choiceStatement) (e : choiceChallenge) :
code Simulator_locs [interface] choiceTranscript :=
{code
z ← sample uniform i_witness ;;
ret (h, fto (g ^+ (otf z) × (otf h ^- (otf e))), e, z)
}.
Definition Verify (h : choiceStatement) (a : choiceMessage)
(e : choiceChallenge) (z : choiceResponse) : choiceBool :=
fto (g ^+ (otf z) == (otf a) × (otf h) ^+ (otf e)).
Definition Extractor (h : choiceStatement) (a : choiceMessage)
(e : choiceChallenge) (e' : choiceChallenge)
(z : choiceResponse) (z' : choiceResponse) : 'option choiceWitness :=
Some (fto ((otf z - otf z') / (otf e - otf e'))%R).
Definition KeyGen (w : choiceWitness) := fto (g ^+ w).
End MyAlg.
#[local] Open Scope package_scope.
Module Sigma := SigmaProtocol MyParam MyAlg.
Import MyParam MyAlg Sigma.
Lemma cyclic_zeta: cyclic ζ.
Proof.
apply /cyclicP. ∃ g. exact: g_gen.
Qed.
Lemma group_prodC :
∀ (x y : gT), x × y = y × x.
Proof.
move ⇒ x y.
have Hx: ∃ ix, x = g^+ix.
{ apply /cycleP. rewrite -g_gen.
apply: in_setT.
}
have Hy: ∃ iy, y = g^+iy.
{ apply /cycleP. rewrite -g_gen.
apply: in_setT.
}
destruct Hx as [ix Hx].
destruct Hy as [iy Hy].
subst.
repeat rewrite -expgD addnC. reflexivity.
Qed.
Lemma group_prodA :
∀ (x y z : gT), x × (y × z) = (x × y) × z.
Proof.
move ⇒ x y z.
have Hx: ∃ ix, x = g^+ix.
{ apply /cycleP. rewrite -g_gen.
apply: in_setT.
}
have Hy: ∃ iy, y = g^+iy.
{ apply /cycleP. rewrite -g_gen.
apply: in_setT.
}
have Hz: ∃ iz, z = g^+iz.
{ apply /cycleP. rewrite -g_gen.
apply: in_setT.
}
destruct Hx as [ix Hx].
destruct Hy as [iy Hy].
subst.
repeat rewrite -expgD addnC addnA.
rewrite mulgA.
reflexivity.
Qed.
#[local] Definition f (e w : Witness) :
Arit (uniform i_witness) → Arit (uniform i_witness) :=
λ z, fto (otf z + e × w).
Lemma order_ge1 : succn (succn (Zp_trunc q)) = q.
Proof.
apply Zp_cast, prime_gt1, prime_order.
Qed.
Lemma bij_f w e : bijective (f w e).
Proof.
unfold f.
∃ (λ x, fto (otf x - w × e)).
all: intro x ; unfold fto, otf ; rewrite !enum_rankK.
- by rewrite addrK enum_valK.
- by rewrite subrK enum_valK.
Qed.
(* Main theorem. *)
(* Proves that Schnorr is a ∑-protocol with perfect special honest-verifier
zero-knowledge *)
Theorem schnorr_SHVZK :
∀ LA A,
ValidPackage LA [interface
#val #[ TRANSCRIPT ] : chInput → chTranscript
] A_export A →
fseparate LA Sigma_locs →
ɛ_SHVZK A = 0.
Proof.
intros LA A Va Hdisj.
eapply (eq_rel_perf_ind _ _ (heap_ignore Sigma_locs)).
3,4,5: ssprove_valid.
1: ssprove_invariant.
simplify_eq_rel hwe.
(* Programming logic part *)
destruct hwe as [[h w] e].
(* We can only simulate if the relation is valid *)
ssprove_sync_eq. intros rel.
(* When relation holds we can reconstruct the first message from the response *)
move⇒ /eqP in rel.
eapply r_uniform_bij with (1 := bij_f (otf w) (otf e)). intros z_val.
ssprove_contract_put_get_lhs.
apply r_put_lhs.
ssprove_restore_pre.
1: ssprove_invariant.
apply r_ret.
(* Ambient logic proof of post condition *)
intros s₀ s₁ Hs.
unfold f.
rewrite rel.
split.
2: apply Hs.
simpl.
rewrite otf_fto expg_mod.
1: rewrite order_ge1 ; apply expg_order.
rewrite expgD - !expgVn.
rewrite group_prodC group_prodA group_prodC group_prodA /=.
rewrite expg_mod.
1: rewrite order_ge1 ; apply expg_order.
rewrite -expgM -expgMn.
1: apply group_prodC.
rewrite mulgV expg1n mul1g.
cbn. rewrite Zp_mulC.
reflexivity.
Qed.
Lemma otf_neq :
∀ (a b : choiceChallenge),
a != b → otf a != otf b.
Proof.
intros a b.
apply: contra ⇒ H.
rewrite bij_eq in H.
- apply enum_val_bij.
- assumption.
Qed.
Lemma neq_pos :
∀ (q : nat) (a b : ('Z_q:finZmodType)),
a != b →
a - b != 0.
Proof.
intros q a b.
apply contraPneq ⇒ H_eq.
assert (H : (a - b == 0)).
{ by rewrite H_eq. }
rewrite subr_eq0 in H.
move⇒ /eqP in H.
rewrite H.
unfold not ⇒ contra.
rewrite eq_refl in contra.
discriminate.
Qed.
(* Lemma proving that the output of the extractor defined for Schnorr's
protocol is perfectly indistinguishable from real protocol execution.
*)
Lemma extractor_success:
∀ LA A,
ValidPackage LA [interface
#val #[ SOUNDNESS ] : chSoundness → 'bool
] A_export A →
ɛ_soundness A = 0.
Proof.
intros LA A VA.
apply: eq_rel_perf_ind_eq.
2,3: apply fseparatem0.
simplify_eq_rel h.
destruct h as [? [? [? [? [? ?]]]]].
destruct s1.
case [&& _ & _] eqn:e.
all: apply r_ret; auto.
intros h1 h2 →.
(* Algebraic proof that the produced witness satisfies the relation. *)
unfold R.
unfold "&&" in e.
inversion e.
repeat match goal with
| |- context [ if ?b then _ else _ ] ⇒ case b eqn:?
end.
2,3: discriminate.
rewrite otf_fto in Heqs4.
rewrite otf_fto in e.
move⇒ /eqP in e.
move⇒ /eqP in Heqs4.
rewrite H0.
rewrite otf_fto expg_mod.
1: rewrite order_ge1 ; apply expg_order.
rewrite expgM expg_mod.
1: rewrite order_ge1 ; apply expg_order.
rewrite expgD -FinRing.zmodVgE expg_zneg.
1: apply cycle_id.
rewrite Heqs4 e !expgMn.
1-2: apply group_prodC.
rewrite invMg !expgMn.
1: apply group_prodC.
rewrite !group_prodA.
rewrite group_prodC 2!group_prodA -expgMn.
1: apply group_prodC.
rewrite mulVg expg1n mul1g -expg_zneg.
{
have Hx : ∃ ix, otf s = g ^+ ix.
{ apply /cycleP. rewrite -g_gen. apply: in_setT. }
destruct Hx as [ix ->].
apply mem_cycle.
}
rewrite expgAC.
rewrite [otf s ^+ (- otf s2) ^+ _] expgAC.
rewrite -expgD -expgM.
have <- := @expg_mod _ q.
{
have Hx : ∃ ix, otf s = g ^+ ix.
{ apply /cycleP. rewrite -g_gen. apply: in_setT. }
destruct Hx as [ix ->].
rewrite expgAC /q.
rewrite expg_order.
apply expg1n.
}
rewrite -modnMmr.
have → :
(modn
(addn (@nat_of_ord (S (S (Zp_trunc q))) (@otf Challenge s1))
(@nat_of_ord (S (S (Zp_trunc q)))
(GRing.opp
(@otf Challenge s2))))
q) =
(@nat_of_ord (S (S (Zp_trunc q)))
(@Zp_add _ (@otf Challenge s1) (@Zp_opp _ (@otf Challenge s2)))).
{ simpl.
rewrite modnDmr.
destruct (otf s2) as [a Ha].
destruct a as [| Pa].
- simpl.
rewrite subn0 modnn addn0 modnDr.
rewrite → order_ge1 at 3.
rewrite modn_small.
+ rewrite <- order_ge1 at 2. apply ltn_ord.
+ reflexivity.
- simpl.
rewrite <- order_ge1 at 4.
rewrite modnDmr.
reflexivity.
}
have → :
(modn
(muln (@nat_of_ord (S (S (Zp_trunc q)))
(GRing.inv
(GRing.add
(@otf Challenge s1)
(GRing.opp
(@otf Challenge s2)))))
(@nat_of_ord (S (S (Zp_trunc q)))
(@Zp_add _ (@otf Challenge s1) (@Zp_opp _ (@otf Challenge s2))))) q) =
(Zp_mul
(GRing.inv
(GRing.add
(@otf Challenge s1)
(GRing.opp
(@otf Challenge s2))))
(@Zp_add _ (@otf Challenge s1) (@Zp_opp _ (@otf Challenge s2)))).
{ simpl.
rewrite modnDmr.
rewrite <- order_ge1 at 9.
rewrite modnMmr.
reflexivity.
}
rewrite Zp_mulVz.
2: cbn ; by rewrite eq_refl.
rewrite → order_ge1 at 1.
apply otf_neq in Heqb.
rewrite prime_coprime.
1: apply prime_order.
rewrite gtnNdvd.
- rewrite lt0n.
apply neq_pos.
assumption.
- destruct (otf s1 - otf s2) as [k Hk].
simpl.
rewrite order_ge1 in Hk.
apply Hk.
- done.
Qed.
Lemma compat : fcompat Com_locs Simulator_locs.
Proof. fmap_solve. Qed.
(* Main theorem proving that the Schnorr protocol has perfect hiding. *)
Theorem schnorr_com_hiding :
∀ LA A,
ValidPackage LA [interface
#val #[HIDING] : (chChallenge) × (chChallenge) → chMessage
] A_export (A ∘ par KEY (ID Hiding_E)) →
fseparate LA KEY_locs →
fseparate LA Sigma_to_Com_locs →
fseparate LA [fmap setup_loc] →
fseparate LA Sigma_locs →
fseparate LA Simulator_locs →
ɛ_hiding compat A ≤ 0.
Proof.
intros LA A VA Hd1 Hd2 Hd3 Hd4 Hd5.
eapply le_trans.
1: eapply commitment_hiding with (LA := LA).
all: try assumption.
1-3: fmap_solve.
rewrite addr0 add0r.
erewrite schnorr_SHVZK by ssprove_valid.
rewrite Advantage_sym.
erewrite schnorr_SHVZK by ssprove_valid.
rewrite addr0 add0r.
apply eq_ler.
eapply eq_rel_perf_ind.
1,2: exact _.
1:{
instantiate (1 := (heap_ignore Com_locs)).
ssprove_invariant.
}
2: apply VA.
2,3: fmap_solve.
simplify_eq_rel hwe.
ssprove_code_simpl.
simplify_linking.
destruct hwe as [e e'].
apply r_const_sample_R; [ exact _ |].
intros e_rand.
ssprove_code_simpl.
ssprove_code_simpl_more.
apply r_const_sample_L; [ exact _ |].
intros b.
simpl.
case (Nat.even b).
- ssprove_code_simpl.
ssprove_code_simpl_more.
ssprove_code_simpl.
ssprove_code_simpl_more.
ssprove_sync⇒setup.
apply r_assertD.
1: done.
intros _ _.
ssprove_sync⇒ w.
apply r_assertD.
1: done.
intros _ _.
ssprove_sync.
apply r_assertD.
1: done.
intros _ rel.
ssprove_sync⇒x.
ssprove_contract_put_get_lhs.
ssprove_contract_put_get_rhs.
eapply r_put_vs_put.
eapply r_put_vs_put.
eapply r_put_vs_put.
ssprove_restore_pre. 1: ssprove_invariant.
apply r_ret. intuition auto.
- ssprove_code_simpl.
ssprove_code_simpl_more.
ssprove_code_simpl.
ssprove_code_simpl_more.
ssprove_sync⇒setup.
apply r_assertD.
1: done.
intros _ _.
ssprove_sync⇒ w.
apply r_assertD.
1: done.
intros _ _.
ssprove_sync.
apply r_assertD.
1: done.
intros _ rel.
ssprove_sync⇒x.
ssprove_contract_put_get_lhs.
ssprove_contract_put_get_rhs.
eapply r_put_vs_put.
eapply r_put_vs_put.
eapply r_put_vs_put.
ssprove_restore_pre. 1: ssprove_invariant.
apply r_ret. intuition auto.
Qed.
(* Main theorem *)
(* The commitment scheme instantiated from Schnorr' protocol *)
(* is binding equal to the hardness of the relation *)
(* (I.e. how hard is it to produce a valid witness for a fixed public input)*)
Theorem schnorr_com_binding :
∀ LA A,
ValidPackage LA [interface
#val #[ SOUNDNESS ] : chSoundness → 'bool
] A_export A →
fseparate LA Sigma_to_Com_locs →
fseparate LA KEY_locs →
AdvantageE (Com_Binding ∘ Sigma_to_Com compat ∘ KEY) (Special_Soundness_f) A ≤ 0.
Proof.
intros LA A VA Hd1 Hd2.
eapply le_trans.
1: apply Advantage_triangle.
instantiate (1 := Special_Soundness_t).
rewrite → (commitment_binding compat LA A VA) by fmap_solve.
setoid_rewrite (extractor_success LA A VA).
rewrite GRing.add0r.
apply le_refl.
Qed.
End Schnorr.
Module GP_Z3 <: GroupParam.
Definition gT : finGroupType := 'Z_2.
Definition ζ : {set gT} := [set : gT].
Definition g : gT := Zp1.
Lemma g_gen : ζ = <[g]>.
Proof.
unfold ζ, g. apply Zp_cycle.
Qed.
Lemma prime_order : prime #[g].
Proof.
unfold g.
rewrite order_Zp1.
reflexivity.
Qed.
End GP_Z3.
Module Schnorr_Z3 := Schnorr GP_Z3.
Set Warnings "-notation-overridden,-ambiguous-paths".
From mathcomp Require Import all_ssreflect all_algebra reals distr realsum
fingroup solvable.cyclic prime ssrnat ssreflect ssrfun ssrbool ssrnum
eqtype choice seq.
Set Warnings "notation-overridden,ambiguous-paths".
Unset SsrOldRewriteGoalsOrder. (* remove the line when requiring MathComp >= 2.6 *)
From extructures Require Import ord fset fmap.
From SSProve.Crypt Require Import Package SigmaProtocol.
Set Bullet Behavior "Strict Subproofs".
Set Default Goal Selector "!".
Set Primitive Projections.
Local Open Scope ring_scope.
Local Open Scope group_scope.
Import GRing.Theory.
Import Num.Def.
Import Num.Theory.
Import Order.POrderTheory.
Import PackageNotation.
Module Type GroupParam.
Parameter gT : finGroupType.
Definition ζ : {set gT} := [set : gT].
Parameter g : gT.
Parameter g_gen : ζ = <[g]>.
Parameter prime_order : prime #[g].
End GroupParam.
Module Schnorr (GP : GroupParam).
Import GP.
(* order of g *)
Definition q : nat := #[g].
Module MyParam <: SigmaProtocolParams.
Definition Witness : finType := Finite.clone _ 'Z_q.
Definition Statement : finType := gT.
Definition Message : finType := gT.
Definition Challenge : finType := Finite.clone _ 'Z_q.
Definition Response : finType := Finite.clone _ 'Z_q.
Definition Transcript : finType :=
prod (prod Message Challenge) Response.
Definition w0 : Witness := 0.
Definition R : Statement → Witness → bool :=
(λ (h : Statement) (w : Witness), h == (g ^+ w)).
End MyParam.
Module MyAlg <: SigmaProtocolAlgorithms MyParam.
Import MyParam.
Definition choiceWitness : choice_type := 'fin #|Witness|.
Definition choiceStatement : choice_type := 'fin #|Statement|.
Definition choiceMessage : choice_type := 'fin #|Message|.
Definition choiceChallenge : choice_type := 'fin #|Challenge|.
Definition choiceResponse : choice_type := 'fin #|Response|.
Definition choiceTranscript : choice_type :=
chProd
(chProd (chProd choiceStatement choiceMessage) choiceChallenge)
choiceResponse.
Definition choiceBool := 'fin #|'bool|.
Definition i_witness := #|Witness|.
Definition commit_loc := mkloc 2 (fto 1 : choiceWitness).
Definition Sigma_locs : Locations := [fmap commit_loc].
Definition Simulator_locs : Locations := emptym.
Definition Commit (h : choiceStatement) (w : choiceWitness):
code Sigma_locs [interface] choiceMessage :=
{code
r ← sample uniform i_witness ;;
#put commit_loc := r ;;
ret (fto (g ^+ (otf r)))
}.
Definition Response (h : choiceStatement) (w : choiceWitness) (a : choiceMessage) (e : choiceChallenge) :
code Sigma_locs [interface] choiceResponse :=
{code
r ← get commit_loc ;;
ret (fto (otf r + otf e × otf w))
}.
Definition Simulate (h : choiceStatement) (e : choiceChallenge) :
code Simulator_locs [interface] choiceTranscript :=
{code
z ← sample uniform i_witness ;;
ret (h, fto (g ^+ (otf z) × (otf h ^- (otf e))), e, z)
}.
Definition Verify (h : choiceStatement) (a : choiceMessage)
(e : choiceChallenge) (z : choiceResponse) : choiceBool :=
fto (g ^+ (otf z) == (otf a) × (otf h) ^+ (otf e)).
Definition Extractor (h : choiceStatement) (a : choiceMessage)
(e : choiceChallenge) (e' : choiceChallenge)
(z : choiceResponse) (z' : choiceResponse) : 'option choiceWitness :=
Some (fto ((otf z - otf z') / (otf e - otf e'))%R).
Definition KeyGen (w : choiceWitness) := fto (g ^+ w).
End MyAlg.
#[local] Open Scope package_scope.
Module Sigma := SigmaProtocol MyParam MyAlg.
Import MyParam MyAlg Sigma.
Lemma cyclic_zeta: cyclic ζ.
Proof.
apply /cyclicP. ∃ g. exact: g_gen.
Qed.
Lemma group_prodC :
∀ (x y : gT), x × y = y × x.
Proof.
move ⇒ x y.
have Hx: ∃ ix, x = g^+ix.
{ apply /cycleP. rewrite -g_gen.
apply: in_setT.
}
have Hy: ∃ iy, y = g^+iy.
{ apply /cycleP. rewrite -g_gen.
apply: in_setT.
}
destruct Hx as [ix Hx].
destruct Hy as [iy Hy].
subst.
repeat rewrite -expgD addnC. reflexivity.
Qed.
Lemma group_prodA :
∀ (x y z : gT), x × (y × z) = (x × y) × z.
Proof.
move ⇒ x y z.
have Hx: ∃ ix, x = g^+ix.
{ apply /cycleP. rewrite -g_gen.
apply: in_setT.
}
have Hy: ∃ iy, y = g^+iy.
{ apply /cycleP. rewrite -g_gen.
apply: in_setT.
}
have Hz: ∃ iz, z = g^+iz.
{ apply /cycleP. rewrite -g_gen.
apply: in_setT.
}
destruct Hx as [ix Hx].
destruct Hy as [iy Hy].
subst.
repeat rewrite -expgD addnC addnA.
rewrite mulgA.
reflexivity.
Qed.
#[local] Definition f (e w : Witness) :
Arit (uniform i_witness) → Arit (uniform i_witness) :=
λ z, fto (otf z + e × w).
Lemma order_ge1 : succn (succn (Zp_trunc q)) = q.
Proof.
apply Zp_cast, prime_gt1, prime_order.
Qed.
Lemma bij_f w e : bijective (f w e).
Proof.
unfold f.
∃ (λ x, fto (otf x - w × e)).
all: intro x ; unfold fto, otf ; rewrite !enum_rankK.
- by rewrite addrK enum_valK.
- by rewrite subrK enum_valK.
Qed.
(* Main theorem. *)
(* Proves that Schnorr is a ∑-protocol with perfect special honest-verifier
zero-knowledge *)
Theorem schnorr_SHVZK :
∀ LA A,
ValidPackage LA [interface
#val #[ TRANSCRIPT ] : chInput → chTranscript
] A_export A →
fseparate LA Sigma_locs →
ɛ_SHVZK A = 0.
Proof.
intros LA A Va Hdisj.
eapply (eq_rel_perf_ind _ _ (heap_ignore Sigma_locs)).
3,4,5: ssprove_valid.
1: ssprove_invariant.
simplify_eq_rel hwe.
(* Programming logic part *)
destruct hwe as [[h w] e].
(* We can only simulate if the relation is valid *)
ssprove_sync_eq. intros rel.
(* When relation holds we can reconstruct the first message from the response *)
move⇒ /eqP in rel.
eapply r_uniform_bij with (1 := bij_f (otf w) (otf e)). intros z_val.
ssprove_contract_put_get_lhs.
apply r_put_lhs.
ssprove_restore_pre.
1: ssprove_invariant.
apply r_ret.
(* Ambient logic proof of post condition *)
intros s₀ s₁ Hs.
unfold f.
rewrite rel.
split.
2: apply Hs.
simpl.
rewrite otf_fto expg_mod.
1: rewrite order_ge1 ; apply expg_order.
rewrite expgD - !expgVn.
rewrite group_prodC group_prodA group_prodC group_prodA /=.
rewrite expg_mod.
1: rewrite order_ge1 ; apply expg_order.
rewrite -expgM -expgMn.
1: apply group_prodC.
rewrite mulgV expg1n mul1g.
cbn. rewrite Zp_mulC.
reflexivity.
Qed.
Lemma otf_neq :
∀ (a b : choiceChallenge),
a != b → otf a != otf b.
Proof.
intros a b.
apply: contra ⇒ H.
rewrite bij_eq in H.
- apply enum_val_bij.
- assumption.
Qed.
Lemma neq_pos :
∀ (q : nat) (a b : ('Z_q:finZmodType)),
a != b →
a - b != 0.
Proof.
intros q a b.
apply contraPneq ⇒ H_eq.
assert (H : (a - b == 0)).
{ by rewrite H_eq. }
rewrite subr_eq0 in H.
move⇒ /eqP in H.
rewrite H.
unfold not ⇒ contra.
rewrite eq_refl in contra.
discriminate.
Qed.
(* Lemma proving that the output of the extractor defined for Schnorr's
protocol is perfectly indistinguishable from real protocol execution.
*)
Lemma extractor_success:
∀ LA A,
ValidPackage LA [interface
#val #[ SOUNDNESS ] : chSoundness → 'bool
] A_export A →
ɛ_soundness A = 0.
Proof.
intros LA A VA.
apply: eq_rel_perf_ind_eq.
2,3: apply fseparatem0.
simplify_eq_rel h.
destruct h as [? [? [? [? [? ?]]]]].
destruct s1.
case [&& _ & _] eqn:e.
all: apply r_ret; auto.
intros h1 h2 →.
(* Algebraic proof that the produced witness satisfies the relation. *)
unfold R.
unfold "&&" in e.
inversion e.
repeat match goal with
| |- context [ if ?b then _ else _ ] ⇒ case b eqn:?
end.
2,3: discriminate.
rewrite otf_fto in Heqs4.
rewrite otf_fto in e.
move⇒ /eqP in e.
move⇒ /eqP in Heqs4.
rewrite H0.
rewrite otf_fto expg_mod.
1: rewrite order_ge1 ; apply expg_order.
rewrite expgM expg_mod.
1: rewrite order_ge1 ; apply expg_order.
rewrite expgD -FinRing.zmodVgE expg_zneg.
1: apply cycle_id.
rewrite Heqs4 e !expgMn.
1-2: apply group_prodC.
rewrite invMg !expgMn.
1: apply group_prodC.
rewrite !group_prodA.
rewrite group_prodC 2!group_prodA -expgMn.
1: apply group_prodC.
rewrite mulVg expg1n mul1g -expg_zneg.
{
have Hx : ∃ ix, otf s = g ^+ ix.
{ apply /cycleP. rewrite -g_gen. apply: in_setT. }
destruct Hx as [ix ->].
apply mem_cycle.
}
rewrite expgAC.
rewrite [otf s ^+ (- otf s2) ^+ _] expgAC.
rewrite -expgD -expgM.
have <- := @expg_mod _ q.
{
have Hx : ∃ ix, otf s = g ^+ ix.
{ apply /cycleP. rewrite -g_gen. apply: in_setT. }
destruct Hx as [ix ->].
rewrite expgAC /q.
rewrite expg_order.
apply expg1n.
}
rewrite -modnMmr.
have → :
(modn
(addn (@nat_of_ord (S (S (Zp_trunc q))) (@otf Challenge s1))
(@nat_of_ord (S (S (Zp_trunc q)))
(GRing.opp
(@otf Challenge s2))))
q) =
(@nat_of_ord (S (S (Zp_trunc q)))
(@Zp_add _ (@otf Challenge s1) (@Zp_opp _ (@otf Challenge s2)))).
{ simpl.
rewrite modnDmr.
destruct (otf s2) as [a Ha].
destruct a as [| Pa].
- simpl.
rewrite subn0 modnn addn0 modnDr.
rewrite → order_ge1 at 3.
rewrite modn_small.
+ rewrite <- order_ge1 at 2. apply ltn_ord.
+ reflexivity.
- simpl.
rewrite <- order_ge1 at 4.
rewrite modnDmr.
reflexivity.
}
have → :
(modn
(muln (@nat_of_ord (S (S (Zp_trunc q)))
(GRing.inv
(GRing.add
(@otf Challenge s1)
(GRing.opp
(@otf Challenge s2)))))
(@nat_of_ord (S (S (Zp_trunc q)))
(@Zp_add _ (@otf Challenge s1) (@Zp_opp _ (@otf Challenge s2))))) q) =
(Zp_mul
(GRing.inv
(GRing.add
(@otf Challenge s1)
(GRing.opp
(@otf Challenge s2))))
(@Zp_add _ (@otf Challenge s1) (@Zp_opp _ (@otf Challenge s2)))).
{ simpl.
rewrite modnDmr.
rewrite <- order_ge1 at 9.
rewrite modnMmr.
reflexivity.
}
rewrite Zp_mulVz.
2: cbn ; by rewrite eq_refl.
rewrite → order_ge1 at 1.
apply otf_neq in Heqb.
rewrite prime_coprime.
1: apply prime_order.
rewrite gtnNdvd.
- rewrite lt0n.
apply neq_pos.
assumption.
- destruct (otf s1 - otf s2) as [k Hk].
simpl.
rewrite order_ge1 in Hk.
apply Hk.
- done.
Qed.
Lemma compat : fcompat Com_locs Simulator_locs.
Proof. fmap_solve. Qed.
(* Main theorem proving that the Schnorr protocol has perfect hiding. *)
Theorem schnorr_com_hiding :
∀ LA A,
ValidPackage LA [interface
#val #[HIDING] : (chChallenge) × (chChallenge) → chMessage
] A_export (A ∘ par KEY (ID Hiding_E)) →
fseparate LA KEY_locs →
fseparate LA Sigma_to_Com_locs →
fseparate LA [fmap setup_loc] →
fseparate LA Sigma_locs →
fseparate LA Simulator_locs →
ɛ_hiding compat A ≤ 0.
Proof.
intros LA A VA Hd1 Hd2 Hd3 Hd4 Hd5.
eapply le_trans.
1: eapply commitment_hiding with (LA := LA).
all: try assumption.
1-3: fmap_solve.
rewrite addr0 add0r.
erewrite schnorr_SHVZK by ssprove_valid.
rewrite Advantage_sym.
erewrite schnorr_SHVZK by ssprove_valid.
rewrite addr0 add0r.
apply eq_ler.
eapply eq_rel_perf_ind.
1,2: exact _.
1:{
instantiate (1 := (heap_ignore Com_locs)).
ssprove_invariant.
}
2: apply VA.
2,3: fmap_solve.
simplify_eq_rel hwe.
ssprove_code_simpl.
simplify_linking.
destruct hwe as [e e'].
apply r_const_sample_R; [ exact _ |].
intros e_rand.
ssprove_code_simpl.
ssprove_code_simpl_more.
apply r_const_sample_L; [ exact _ |].
intros b.
simpl.
case (Nat.even b).
- ssprove_code_simpl.
ssprove_code_simpl_more.
ssprove_code_simpl.
ssprove_code_simpl_more.
ssprove_sync⇒setup.
apply r_assertD.
1: done.
intros _ _.
ssprove_sync⇒ w.
apply r_assertD.
1: done.
intros _ _.
ssprove_sync.
apply r_assertD.
1: done.
intros _ rel.
ssprove_sync⇒x.
ssprove_contract_put_get_lhs.
ssprove_contract_put_get_rhs.
eapply r_put_vs_put.
eapply r_put_vs_put.
eapply r_put_vs_put.
ssprove_restore_pre. 1: ssprove_invariant.
apply r_ret. intuition auto.
- ssprove_code_simpl.
ssprove_code_simpl_more.
ssprove_code_simpl.
ssprove_code_simpl_more.
ssprove_sync⇒setup.
apply r_assertD.
1: done.
intros _ _.
ssprove_sync⇒ w.
apply r_assertD.
1: done.
intros _ _.
ssprove_sync.
apply r_assertD.
1: done.
intros _ rel.
ssprove_sync⇒x.
ssprove_contract_put_get_lhs.
ssprove_contract_put_get_rhs.
eapply r_put_vs_put.
eapply r_put_vs_put.
eapply r_put_vs_put.
ssprove_restore_pre. 1: ssprove_invariant.
apply r_ret. intuition auto.
Qed.
(* Main theorem *)
(* The commitment scheme instantiated from Schnorr' protocol *)
(* is binding equal to the hardness of the relation *)
(* (I.e. how hard is it to produce a valid witness for a fixed public input)*)
Theorem schnorr_com_binding :
∀ LA A,
ValidPackage LA [interface
#val #[ SOUNDNESS ] : chSoundness → 'bool
] A_export A →
fseparate LA Sigma_to_Com_locs →
fseparate LA KEY_locs →
AdvantageE (Com_Binding ∘ Sigma_to_Com compat ∘ KEY) (Special_Soundness_f) A ≤ 0.
Proof.
intros LA A VA Hd1 Hd2.
eapply le_trans.
1: apply Advantage_triangle.
instantiate (1 := Special_Soundness_t).
rewrite → (commitment_binding compat LA A VA) by fmap_solve.
setoid_rewrite (extractor_success LA A VA).
rewrite GRing.add0r.
apply le_refl.
Qed.
End Schnorr.
Module GP_Z3 <: GroupParam.
Definition gT : finGroupType := 'Z_2.
Definition ζ : {set gT} := [set : gT].
Definition g : gT := Zp1.
Lemma g_gen : ζ = <[g]>.
Proof.
unfold ζ, g. apply Zp_cycle.
Qed.
Lemma prime_order : prime #[g].
Proof.
unfold g.
rewrite order_Zp1.
reflexivity.
Qed.
End GP_Z3.
Module Schnorr_Z3 := Schnorr GP_Z3.