aboutsummaryrefslogtreecommitdiff
path: root/src/Spec
diff options
context:
space:
mode:
Diffstat (limited to 'src/Spec')
-rw-r--r--src/Spec/Ed25519.v91
-rw-r--r--src/Spec/EdDSA.v82
2 files changed, 0 insertions, 173 deletions
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.
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-07 19:53:17 +0000