aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorBenjamin Barenblat <bbaren@google.com>2019-04-26 16:28:19 -0400
committerBenjamin Barenblat <bbaren@google.com>2019-04-26 16:28:19 -0400
commite93ec9a4112d2a6f78deb8fca10c5bd5c4b3c1cb (patch)
treec1241cf2a159b2eca5e3aa75379319b47f5de0d0
parent8a4d828e05bca153f12370d08d3b4ad404fbbee2 (diff)
Remove EdDSA
Remove Spec/EdDSA.v and its reverse dependencies Spec/Ed25519.v and Primitives/EdDSARepChange.v. This code is no longer in use.
-rw-r--r--_CoqProject3
-rw-r--r--src/Primitives/EdDSARepChange.v267
-rw-r--r--src/Spec/Ed25519.v91
-rw-r--r--src/Spec/EdDSA.v82
4 files changed, 0 insertions, 443 deletions
diff --git a/_CoqProject b/_CoqProject
index 8859f08ed..f8e005119 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -96,7 +96,6 @@ src/Fancy/Compiler.v
src/Fancy/Montgomery256.v
src/Fancy/Prod.v
src/Fancy/Spec.v
-src/Primitives/EdDSARepChange.v
src/Primitives/MxDHRepChange.v
src/PushButtonSynthesis/BarrettReduction.v
src/PushButtonSynthesis/BarrettReductionReificationCache.v
@@ -120,8 +119,6 @@ src/Rewriter/StripLiteralCasts.v
src/Rewriter/ToFancy.v
src/Rewriter/ToFancyWithCasts.v
src/Spec/CompleteEdwardsCurve.v
-src/Spec/Ed25519.v
-src/Spec/EdDSA.v
src/Spec/ModularArithmetic.v
src/Spec/MontgomeryCurve.v
src/Spec/MxDH.v
diff --git a/src/Primitives/EdDSARepChange.v b/src/Primitives/EdDSARepChange.v
deleted file mode 100644
index b7f4acd9b..000000000
--- a/src/Primitives/EdDSARepChange.v
+++ /dev/null
@@ -1,267 +0,0 @@
-Require Import Crypto.Util.FixCoqMistakes.
-Require Import Crypto.Spec.EdDSA bbv.WordScope.
-Require Import Coq.Classes.Morphisms Coq.Relations.Relation_Definitions.
-Require Import Crypto.Algebra.Monoid Crypto.Algebra.Group Crypto.Algebra.ScalarMult.
-Require Import Crypto.Util.Decidable Crypto.Util.Option.
-Require Import Crypto.Util.Tactics.SetEvars.
-Require Import Crypto.Util.Tactics.SubstEvars.
-Require Import Crypto.Util.Tactics.BreakMatch.
-Require Import Crypto.Util.Tactics.SpecializeBy.
-Require Import Coq.omega.Omega.
-Require Import Crypto.Util.Notations.
-Require Import Crypto.Util.Option Crypto.Util.Logic Crypto.Util.Relations Crypto.Util.WordUtil Util.LetIn Util.NatUtil.
-Require Import Crypto.Spec.ModularArithmetic Crypto.Arithmetic.PrimeFieldTheorems.
-Import NPeano.
-
-Import Notations.
-
-Section EdDSA.
- Context `{prm:EdDSA}.
- Local Infix "==" := Eeq. Local Infix "+" := Eadd. Local Infix "*" := ZEmul.
-
- Local Notation valid := (@valid E Eeq Eadd ZEmul b H l B Eenc Senc).
- Lemma sign_valid : forall A_ sk {n} (M:word n), A_ = public sk -> valid M A_ (sign A_ sk M).
- Proof using Type.
- cbv [sign public Spec.EdDSA.valid]; intros; subst;
- repeat match goal with
- | |- exists _, _ => eexists
- | |- _ /\ _ => eapply conj
- | |- _ => reflexivity
- end.
- rewrite F.to_Z_of_Z, scalarmult_mod_order, scalarmult_add_l, cancel_left, scalarmult_mod_order, Z.mul_comm, scalarmult_assoc;
- try solve [ reflexivity
- | setoid_rewrite (*unify 0*) (Z2Nat.inj_iff _ 0); pose proof EdDSA_l_odd; omega
- | pose proof EdDSA_l_odd; omega
- | apply EdDSA_l_order_B
- | rewrite scalarmult_assoc, Z.mul_comm, <-scalarmult_assoc,
- EdDSA_l_order_B, scalarmult_zero_r; reflexivity].
- Qed.
-
- Lemma solve_for_R_sig : forall s B R n A, { solution | s * B == R + n * A <-> R == solution }.
- Proof.
- eexists.
- set_evars.
- setoid_rewrite <-(symmetry_iff(R:=Eeq)) at 1.
- setoid_rewrite <-eq_r_opp_r_inv.
- setoid_rewrite <-scalarmult_opp_r.
- subst_evars.
- reflexivity.
- Defined.
- Definition solve_for_R := Eval cbv [proj2_sig solve_for_R_sig] in (fun s B R n A => proj2_sig (solve_for_R_sig s B R n A)).
-
- Context {Proper_Eenc : Proper (Eeq==>Logic.eq) Eenc}.
- Global Instance Proper_eq_Eenc ref : Proper (Eeq ==> iff) (fun P => Eenc P = ref).
- Proof using Proper_Eenc. intros ? ? Hx; rewrite Hx; reflexivity. Qed.
-
- Context {Edec:word b-> option E} {eq_enc_E_iff: forall P_ P, Eenc P = P_ <-> option_eq Eeq (Edec P_) (Some P)}.
- Context {Sdec:word b-> option (F l)} {eq_enc_S_iff: forall n_ n, Senc n = n_ <-> Sdec n_ = Some n}.
-
- Local Infix "++" := Word.combine.
- Definition verify'_sig : { verify | forall mlen (message:word mlen) (pk:word b) (sig:word (b+b)),
- verify mlen message pk sig = true <-> valid message pk sig }.
- Proof.
- eexists; intros mlen message pk sig; set_evars.
- unfold Spec.EdDSA.valid.
- setoid_rewrite solve_for_R.
- setoid_rewrite combine_eq_iff.
- setoid_rewrite and_comm at 4. setoid_rewrite and_assoc. repeat setoid_rewrite exists_and_indep_l.
- setoid_rewrite (and_rewrite_l Eenc (split1 b b sig)
- (fun x y => x == _ * B + Z.of_nat (wordToNat (H _ (y ++ Eenc _ ++ message))) mod _ * Eopp _)); setoid_rewrite eq_enc_S_iff.
- setoid_rewrite (@exists_and_equiv_r _ _ _ _ _ _).
- setoid_rewrite <- (fun A => and_rewriteleft_l (fun x => x) (Eenc A) (fun pk EencA => exists a,
- Sdec (split2 b b sig) = Some a /\
- Eenc (_ * B + Z.of_nat (wordToNat (H (b + (b + mlen)) (split1 b b sig ++ EencA ++ message))) mod _ * Eopp A)
- = split1 b b sig)). setoid_rewrite (eq_enc_E_iff pk).
- setoid_rewrite <-weqb_true_iff.
- setoid_rewrite <-option_rect_false_returns_true_iff_eq.
- rewrite <-option_rect_false_returns_true_iff by
- (intros ? ? Hxy; unfold option_rect; break_match; rewrite <-?Hxy; reflexivity).
-
- subst_evars.
- eapply reflexivity.
- Defined.
- Definition verify' {mlen} (message:word mlen) (pk:word b) (sig:word (b+b)) : bool :=
- Eval cbv [proj1_sig verify'_sig] in proj1_sig verify'_sig mlen message pk sig.
- Lemma verify'_correct : forall {mlen} (message:word mlen) pk sig,
- verify' message pk sig = true <-> valid message pk sig.
- Proof using Type*. exact (proj2_sig verify'_sig). Qed.
-
- Section ChangeRep.
- Context {Erep ErepEq ErepAdd ErepId ErepOpp} {Agroup:@Algebra.Hierarchy.group Erep ErepEq ErepAdd ErepId ErepOpp}.
- Context {EToRep} {Ahomom:@is_homomorphism E Eeq Eadd Erep ErepEq ErepAdd EToRep}.
-
- Context {ERepEnc : Erep -> word b}
- {ERepEnc_correct : forall P:E, Eenc P = ERepEnc (EToRep P)}
- {Proper_ERepEnc:Proper (ErepEq==>Logic.eq) ERepEnc}.
-
- Context {ERepDec : word b -> option Erep}
- {ERepDec_correct : forall w, option_eq ErepEq (ERepDec w) (option_map EToRep (Edec w)) }.
-
- Context {SRep SRepEq} `{@Equivalence SRep SRepEq} {S2Rep:F l->SRep}.
-
- Context {SRepDecModL} {SRepDecModL_correct: forall (w:word (b+b)), SRepEq (S2Rep (F.of_Z _ (Z.of_nat (wordToNat w)))) (SRepDecModL w)}.
-
- Context {SRepERepMul:SRep->Erep->Erep}
- {SRepERepMul_correct:forall n P, ErepEq (EToRep ((n mod l)*P)) (SRepERepMul (S2Rep (F.of_Z _ n)) (EToRep P))}
- {Proper_SRepERepMul: Proper (SRepEq==>ErepEq==>ErepEq) SRepERepMul}.
-
- Context {SRepDec: word b -> option SRep}
- {SRepDec_correct : forall w, option_eq SRepEq (option_map S2Rep (Sdec w)) (SRepDec w)}.
-
- Definition verify_using_representation
- {mlen} (message:word mlen) (pk:word b) (sig:word (b+b))
- : { answer | answer = verify' message pk sig }.
- Proof.
- eexists.
- pose proof EdDSA_l_odd.
- cbv [verify'].
-
- etransitivity. Focus 2. {
- eapply Proper_option_rect_nd_changebody; [intro|reflexivity].
- eapply Proper_option_rect_nd_changebody; [intro|reflexivity].
- rewrite <-F.mod_to_Z by omega.
- repeat (
- rewrite ERepEnc_correct
- || rewrite homomorphism
- || rewrite homomorphism_id
- || rewrite (homomorphism_inv(INV:=Eopp)(inv:=ErepOpp)(eq:=ErepEq)(phi:=EToRep))
- || rewrite SRepERepMul_correct
- || rewrite SdecS_correct
- || rewrite SRepDecModL_correct
- || rewrite (@F.of_Z_to_Z _ _)
- || rewrite (@F.mod_to_Z _ _)
- ).
- reflexivity.
- } Unfocus.
-
- (* lazymatch goal with |- _ _ (option_rect _ ?some _ _) => idtac some end. *)
- setoid_rewrite (option_rect_option_map EToRep
- (fun s =>
- option_rect (fun _ : option _ => bool)
- (fun s0 =>
- weqb
- (ERepEnc
- (ErepAdd (SRepERepMul (_ s0) (EToRep B))
- (SRepERepMul
- (SRepDecModL
- (H _ (split1 b b sig ++ pk ++ message)))
- (ErepOpp (s))))) (split1 b b sig)) false
- (Sdec (split2 b b sig)))
- false).
- (* rewrite with a complicated proper instance for inline code .. *)
- etransitivity;
- [| eapply Proper_option_rect_nd_changevalue;
- [
- | reflexivity
- | eapply ERepDec_correct
- ];
- [ repeat match goal with
- | |- _ => intro
- | |- _ => eapply Proper_option_rect_nd_changebody
- | |- ?R ?x ?x => reflexivity
- | H : _ |- _ => rewrite H; reflexivity
- end
- ]
- ].
-
- etransitivity. Focus 2. {
- eapply Proper_option_rect_nd_changebody; [intro|reflexivity].
- set_evars.
- setoid_rewrite (option_rect_option_map S2Rep
- (fun s0 =>
- weqb
- (ERepEnc
- (ErepAdd (SRepERepMul (s0) (EToRep B))
- (SRepERepMul
- (SRepDecModL (H _ (split1 b b sig ++ pk ++ message)))
- (ErepOpp _)))) (split1 b b sig))
-
- false).
- subst_evars.
-
- eapply Proper_option_rect_nd_changevalue;
- [repeat intro; repeat f_equiv; eassumption|reflexivity|..].
-
- symmetry.
- eapply SRepDec_correct.
- } Unfocus.
-
- reflexivity.
- Defined.
-
- Definition verify {mlen} (msg:word mlen) pk sig :=
- Eval cbv beta iota delta [proj1_sig verify_using_representation] in
- proj1_sig (verify_using_representation msg pk sig).
- Lemma verify_correct {mlen} (msg:word mlen) pk sig : verify msg pk sig = true <-> valid msg pk sig.
- Proof using Type*.
- etransitivity; [|eapply (verify'_correct msg pk sig)].
- eapply iff_R_R_same_r, (proj2_sig (verify_using_representation _ _ _)).
- Qed.
-
- Context {SRepEnc : SRep -> word b}
- {SRepEnc_correct : forall x, Senc x = SRepEnc (S2Rep x)}
- {Proper_SRepEnc:Proper (SRepEq==>Logic.eq) SRepEnc}.
- Context {SRepAdd : SRep -> SRep -> SRep}
- {SRepAdd_correct : forall x y, SRepEq (S2Rep (x+y)%F) (SRepAdd (S2Rep x) (S2Rep y)) }
- {Proper_SRepAdd:Proper (SRepEq==>SRepEq==>SRepEq) SRepAdd}.
- Context {SRepMul : SRep -> SRep -> SRep}
- {SRepMul_correct : forall x y, SRepEq (S2Rep (x*y)%F) (SRepMul (S2Rep x) (S2Rep y)) }
- {Proper_SRepMul:Proper (SRepEq==>SRepEq==>SRepEq) SRepMul}.
- Context {ErepB:Erep} {ErepB_correct:ErepEq ErepB (EToRep B)}.
-
- Context {SRepDecModLShort} {SRepDecModLShort_correct: forall (w:word (n+1)), SRepEq (S2Rep (F.of_nat _ (wordToNat w))) (SRepDecModLShort w)}.
-
- (* We would ideally derive the optimized implementations from
- specifications using `setoid_rewrite`, but doing this without
- inlining let-bound subexpressions turned out to be quite messy in
- the current state of Coq: <https://github.com/mit-plv/fiat-crypto/issues/64> *)
-
- Let n_le_bpb : (n <= b+b)%nat. destruct prm. omega. Qed.
-
- (* TODO: change impl to basesystem *)
- Context (splitSecretPrngCurve : forall (sk:word b), SRep * word b).
- Context (splitSecretPrngCurve_correct : forall sk,
- let (s, r) := splitSecretPrngCurve sk in
- SRepEq s (S2Rep (F.of_Z l (curveKey sk))) /\ r = prngKey (H:=H) sk).
-
- Definition sign (pk sk : word b) {mlen} (msg:word mlen) :=
- dlet sp := splitSecretPrngCurve sk in
- dlet s := fst sp in
- dlet p := snd sp in
- dlet r := SRepDecModL (H _ (p ++ msg)) in
- dlet R := SRepERepMul r ErepB in
- dlet S := SRepAdd r (SRepMul (SRepDecModL (H _ (ERepEnc R ++ pk ++ msg))) s) in
- ERepEnc R ++ SRepEnc S.
-
- Lemma Z_l_nonzero : Z.pos l <> 0%Z. discriminate. Qed.
-
- Lemma sign_correct (pk sk : word b) {mlen} (msg:word mlen)
- : sign pk sk msg = EdDSA.sign pk sk msg.
- Proof using Agroup Ahomom ERepEnc_correct ErepB_correct H0 Proper_ERepEnc Proper_SRepAdd Proper_SRepERepMul Proper_SRepEnc Proper_SRepMul SRepAdd_correct SRepDecModLShort_correct SRepDecModL_correct SRepERepMul_correct SRepEnc_correct SRepMul_correct splitSecretPrngCurve_correct.
- cbv [sign EdDSA.sign Let_In].
-
- let H := fresh "H" in
- pose proof (splitSecretPrngCurve_correct sk) as H;
- destruct (splitSecretPrngCurve sk);
- destruct H as [curveKey_correct prngKey_correct].
-
- repeat (
- reflexivity
- || rewrite ERepEnc_correct
- || rewrite SRepEnc_correct
- || rewrite SRepDecModL_correct
- || rewrite SRepERepMul_correct
- || rewrite (F.of_Z_add (m:=l))
- || rewrite (F.of_Z_mul (m:=l))
- || rewrite SRepAdd_correct
- || rewrite SRepMul_correct
- || rewrite ErepB_correct
- || rewrite <-prngKey_correct
- || rewrite <-curveKey_correct
- || eapply (f_equal2 (fun a b => a ++ b))
- || f_equiv
- || rewrite <-(scalarmult_mod_order l B Z_l_nonzero EdDSA_l_order_B), SRepERepMul_correct
- ).
- Qed.
- End ChangeRep.
-End EdDSA.
diff --git a/src/Spec/Ed25519.v b/src/Spec/Ed25519.v
deleted file mode 100644
index e0fba6e23..000000000
--- a/src/Spec/Ed25519.v
+++ /dev/null
@@ -1,91 +0,0 @@
-Require Import Crypto.Spec.ModularArithmetic.
-Require Import Coq.PArith.BinPosDef.
-Require Import Coq.ZArith.BinIntDef.
-Require Import Crypto.Spec.CompleteEdwardsCurve.
-Require Import Crypto.Spec.EdDSA.
-
-Require Crypto.Arithmetic.PrimeFieldTheorems. (* to know that Z mod p is a field *)
-Require Crypto.Curves.Edwards.AffineProofs.
-
-(* these 2 proofs can be generated using https://github.com/andres-erbsen/safecurves-primes *)
-Axiom prime_q : Znumtheory.prime (2^255-19). Global Existing Instance prime_q.
-Axiom prime_l : Znumtheory.prime (2^252 + 27742317777372353535851937790883648493). Global Existing Instance prime_l.
-
-Section Ed25519.
-
- Local Open Scope Z_scope.
-
- Definition q : BinPos.positive := 2^255 - 19.
- Definition Fq : Type := F q.
-
- Definition l : BinPos.positive := 2^252 + 27742317777372353535851937790883648493.
- Definition Fl : Type := F l.
-
- Local Open Scope F_scope.
-
- Definition a : Fq := F.opp 1.
- Definition d : Fq := F.opp (F.of_Z _ 121665) / (F.of_Z _ 121666).
-
- Local Open Scope nat_scope.
-
- Definition b : nat := 256.
- Definition n : nat := b - 2.
- Definition c : nat := 3.
-
- Context {SHA512: forall n : nat, Word.word n -> Word.word 512}.
-
- Local Instance char_gt_e :
- @Ring.char_ge (@F q) eq F.zero F.one F.opp F.add F.sub F.mul
- (BinNat.N.succ_pos BinNat.N.two).
- Proof. eapply Hierarchy.char_ge_weaken;
- [apply (_:Ring.char_ge q)|Decidable.vm_decide]. Qed.
-
-
- Definition E : Type := E.point
- (F:=Fq) (Feq:=Logic.eq) (Fone:=F.one) (Fadd:=F.add) (Fmul:=F.mul)
- (a:=a) (d:=d).
-
- Local Obligation Tactic := Decidable.vm_decide. (* to prove that B is on curve *)
-
- Program Definition B : E :=
- (F.of_Z q 15112221349535400772501151409588531511454012693041857206046113283949847762202,
- F.of_Z q 4 / F.of_Z q 5).
-
- Local Infix "++" := Word.combine.
- Local Notation bit b := (Word.WS b Word.WO : Word.word 1).
-
- Definition Fencode {len} {m} : F m -> Word.word len :=
- fun x : F m => (Word.NToWord _ (BinIntDef.Z.to_N (F.to_Z x))).
- Definition sign (x : F q) : bool := BinIntDef.Z.testbit (F.to_Z x) 0.
- Definition Eenc : E -> Word.word b := fun P =>
- let '(x,y) := E.coordinates P in Fencode (len:=b-1) y ++ bit (sign x).
- Definition Senc : Fl -> Word.word b := Fencode (len:=b).
-
- Lemma nonzero_a : a <> 0%F.
- Proof using Type. Crypto.Util.Decidable.vm_decide. Qed.
- Lemma square_a : exists sqrt_a : Fq, (sqrt_a * sqrt_a)%F = a.
- Proof using Type. pose (@PrimeFieldTheorems.F.Decidable_square q _ ltac:(Crypto.Util.Decidable.vm_decide) a); Crypto.Util.Decidable.vm_decide. Qed.
- Lemma nonsquare_d : forall x : Fq, (x * x)%F <> d.
- Proof using Type. pose (@PrimeFieldTheorems.F.Decidable_square q _ ltac:(Crypto.Util.Decidable.vm_decide) d); Crypto.Util.Decidable.vm_decide. Qed.
-
- Let add := E.add(nonzero_a:=nonzero_a)(square_a:=square_a)(nonsquare_d:=nonsquare_d).
- Let zero := E.zero(nonzero_a:=nonzero_a)(d:=d).
- (* TODO: move scalarmult_ref to Spec? *)
- Let mul := ScalarMult.scalarmult_ref(zero:=zero)(add:=add)(opp:=AffineProofs.E.opp(nonzero_a:=nonzero_a)).
-
- Definition ed25519 (l_order_B: (mul l B = zero)%E) :
- EdDSA (E:=E) (Eadd:=add) (Ezero:=zero) (ZEmul:=mul) (B:=B)
- (Eopp:=Crypto.Curves.Edwards.AffineProofs.E.opp(nonzero_a:=nonzero_a)) (* TODO: move defn *)
- (Eeq:=E.eq) (* TODO: move defn *)
- (l:=l) (b:=b) (n:=n) (c:=c)
- (Eenc:=Eenc) (Senc:=Senc) (H:=SHA512).
- Proof using Type.
- split; try exact _.
- Crypto.Util.Decidable.vm_decide.
- Crypto.Util.Decidable.vm_decide.
- Crypto.Util.Decidable.vm_decide.
- Crypto.Util.Decidable.vm_decide.
- Crypto.Util.Decidable.vm_decide.
- exact l_order_B.
- Qed.
-End Ed25519.
diff --git a/src/Spec/EdDSA.v b/src/Spec/EdDSA.v
deleted file mode 100644
index 268925167..000000000
--- a/src/Spec/EdDSA.v
+++ /dev/null
@@ -1,82 +0,0 @@
-Require bbv.WordScope Crypto.Util.WordUtil.
-Require Import Coq.ZArith.BinIntDef.
-Require Crypto.Algebra.Hierarchy Algebra.ScalarMult.
-Require Coq.ZArith.Znumtheory Coq.ZArith.BinInt.
-Require Coq.Numbers.Natural.Peano.NPeano.
-
-Require Import Crypto.Spec.ModularArithmetic.
-
-Local Infix "-" := BinInt.Z.sub.
-Local Infix "^" := BinInt.Z.pow.
-Local Infix "mod" := BinInt.Z.modulo.
-Local Infix "++" := Word.combine.
-Local Notation setbit := BinInt.Z.setbit.
-
-Section EdDSA.
- Class EdDSA (* <https://eprint.iacr.org/2015/677.pdf> *)
- {E Eeq Eadd Ezero Eopp} {ZEmul} (* the underllying elliptic curve operations *)
-
- {b : nat} (* public keys are k bits, signatures are 2*k bits *)
- {H : forall {n}, Word.word n -> Word.word (b + b)} (* main hash function *)
- {c : nat} (* cofactor E = 2^c *)
- {n : nat} (* secret keys are (n+1) bits *)
- {l : BinPos.positive} (* order of the subgroup of E generated by B *)
-
- {B : E} (* base point *)
-
- {Eenc : E -> Word.word b} (* normative encoding of elliptic cuve points *)
- {Senc : F l -> Word.word b} (* normative encoding of scalars *)
- :=
- {
- EdDSA_group:@Algebra.Hierarchy.group E Eeq Eadd Ezero Eopp;
- EdDSA_scalarmult:@Algebra.ScalarMult.is_scalarmult E Eeq Eadd Ezero Eopp ZEmul;
-
- EdDSA_c_valid : c = 2 \/ c = 3;
-
- EdDSA_n_ge_c : n >= c;
- EdDSA_n_le_b : n <= b;
-
- EdDSA_B_not_identity : not (Eeq B Ezero);
-
- EdDSA_l_prime : Znumtheory.prime l;
- EdDSA_l_odd : BinInt.Z.lt 2 l;
- EdDSA_l_order_B : Eeq (ZEmul l B) Ezero
- }.
- Global Existing Instance EdDSA_group.
- Global Existing Instance EdDSA_scalarmult.
-
- Context `{prm:EdDSA}.
-
- Local Coercion Word.wordToNat : Word.word >-> nat.
- Local Coercion BinInt.Z.of_nat : nat >-> BinInt.Z.
- Local Notation secretkey := (Word.word b) (only parsing).
- Local Notation publickey := (Word.word b) (only parsing).
- Local Notation signature := (Word.word (b + b)) (only parsing).
-
- Local Arguments H {n} _.
- Local Notation wfirstn n w := (@WordUtil.wfirstn n _ w _) (only parsing).
-
- Local Obligation Tactic := destruct prm; simpl; intros; Omega.omega.
-
- Program Definition curveKey (sk:secretkey) : BinInt.Z :=
- let x := wfirstn n (H sk) in (* hash the key, use first "half" for secret scalar *)
- let x := x - (x mod (2^c)) in (* it is implicitly 0 mod (2^c) *)
- setbit x n. (* and the high bit is always set *)
-
- Local Infix "+" := Eadd.
- Local Infix "*" := ZEmul.
-
- Definition prngKey (sk:secretkey) : Word.word b := Word.split2 b b (H sk).
- Definition public (sk:secretkey) : publickey := Eenc (curveKey sk*B).
-
- Program Definition sign (A_:publickey) sk {n} (M : Word.word n) :=
- let r := H (prngKey sk ++ M) in (* secret nonce *)
- let R := r * B in (* commitment to nonce *)
- let s := curveKey sk in (* secret scalar *)
- let S := F.of_Z l (r + H (Eenc R ++ A_ ++ M) * s) in
- Eenc R ++ Senc S.
-
- Definition valid {n} (message : Word.word n) pubkey signature :=
- exists A S R, Eenc A = pubkey /\ Eenc R ++ Senc S = signature /\
- Eeq (F.to_Z S * B) (R + (H (Eenc R ++ Eenc A ++ message) mod l) * A).
-End EdDSA.