diff options
| -rw-r--r-- | src/Curves/Curve25519.v | 68 | ||||
| -rw-r--r-- | src/Curves/PointFormats.v | 31 | ||||
| -rw-r--r-- | src/Galois/EdDSA.v | 11 | ||||
| -rw-r--r-- | src/Specific/EdDSA25519.v | 26 |
4 files changed, 30 insertions, 106 deletions
diff --git a/src/Curves/Curve25519.v b/src/Curves/Curve25519.v deleted file mode 100644 index 248e0af6e..000000000 --- a/src/Curves/Curve25519.v +++ /dev/null @@ -1,68 +0,0 @@ -Require Import Zpower ZArith Znumtheory. -Require Import Crypto.Galois.GaloisField. -Require Import Crypto.Curves.PointFormats. - -Definition two_255_19 := 2^255 - 19. (* <http://safecurves.cr.yp.to/primeproofs.html> *) -Fact two_255_19_prime : prime two_255_19. Admitted. -Module Modulus25519 <: Modulus. - Definition modulus := exist _ two_255_19 two_255_19_prime. -End Modulus25519. - -Module Curve25519Params <: TwistedEdwardsParams Modulus25519 <: Minus1Params Modulus25519. - Module Import GFDefs := GaloisField Modulus25519. - - Local Open Scope GF_scope. - - Definition a : GF := -1. - Definition d : GF := -121665 / 121666. - - Lemma a_nonzero : a <> 0. - Proof. - discriminate. - Qed. - - Definition sqrt_a: GF := 19681161376707505956807079304988542015446066515923890162744021073123829784752. - - Lemma a_square : sqrt_a^2 = a. - Proof. - (* An example of how to use ring properly *) - replace (sqrt_a ^ 2) with (sqrt_a * sqrt_a) by ring. - assert ((inject ((GFToZ sqrt_a) * (GFToZ sqrt_a)))%Z = a). - - - apply gf_eq. - (* vm_compute runs out of memory. *) - admit. - - - rewrite inject_distr_mul in H. - intuition. - - Admitted. - - Lemma d_nonsquare : forall x, x * x <> d. - (* <https://en.wikipedia.org/wiki/Euler%27s_criterion> *) - Admitted. - - Definition A : GF := 486662. - (* Definition montgomeryOnCurve25519 := montgomeryOnCurve 1 A. *) - - (* Module-izing Twisted was a breaking change - Definition m1TwistedOnCurve25519 := twistedOnCurve (0 -1) d. - - Definition identityTwisted : twisted := mkTwisted 0 1. - - Lemma identityTwistedOnCurve : m1TwistedOnCurve25519 identityTwisted. - unfold m1TwistedOnCurve25519, twistedOnCurve. - simpl; field. - Qed. - - *) - - Definition basepointY := 4 / 5. - - (* True iff this prime is odd *) - Definition char_gt_2: (1+1) <> 0. - Admitted. -End Curve25519Params. - -Module Edwards25519 := CompleteTwistedEdwardsCurve Modulus25519 Curve25519Params. -Module Edwards25519Minus1Twisted := Minus1Format Modulus25519 Curve25519Params. diff --git a/src/Curves/PointFormats.v b/src/Curves/PointFormats.v index a44ed7a6d..85f69b87a 100644 --- a/src/Curves/PointFormats.v +++ b/src/Curves/PointFormats.v @@ -5,12 +5,11 @@ Require Import BinNums NArith Nnat ZArith. Module Type TwistedEdwardsParams (M : Modulus). Module Export GFDefs := GaloisField M. + Axiom modulus_odd : (primeToZ M.modulus > 2)%Z. Local Open Scope GF_scope. - Axiom char_gt_2 : (1+1) <> 0. Parameter a : GF. Axiom a_nonzero : a <> 0. - Parameter sqrt_a : GF. - Axiom a_square : sqrt_a^2 = a. + Axiom a_square : exists sqrt_a, sqrt_a^2 = a. Parameter d : GF. Axiom d_nonsquare : forall x, x * x <> d. End TwistedEdwardsParams. @@ -232,6 +231,12 @@ Module CompleteTwistedEdwardsCurve (M : Modulus) (Import P : TwistedEdwardsParam Qed. + Lemma char_gt_2 : inject 2 <> 0. + intro H; inversion H; clear H. + pose proof modulus_odd. + rewrite Zmod_small in H1; intuition; auto; omega. + Qed. + Ltac whatsNotZero := repeat match goal with | [H: ?lhs = ?rhs |- _ ] => @@ -266,7 +271,7 @@ Module CompleteTwistedEdwardsCurve (M : Modulus) (Import P : TwistedEdwardsParam pose proof char_gt_2. pose proof a_nonzero as Ha_nonzero. destruct a_square as [sqrt_a a_square]. - rewrite a_square in Ha_nonzero. + rewrite <-a_square in *. (* Furthermore... *) pose proof (eq_refl (d*x1^2*y1^2*(sqrt_a^2*x2^2 + y2^2))) as Heqt. @@ -296,16 +301,12 @@ Module CompleteTwistedEdwardsCurve (M : Modulus) (Import P : TwistedEdwardsParam assert (Hc: (sqrt_a * x2 + y2) + (sqrt_a * x2 - y2) = 0) by (repeat rewriteAny; field). - rewrite a_square in *. replace (sqrt_a * x2 + y2 + (sqrt_a * x2 - y2)) with (inject 2 * sqrt_a * x2) in Hc by field. (* contradiction: product of nonzero things is zero *) - destruct (mul_zero_why _ _ Hc) as [Hcc|Hcc]; try solve [subst; intuition]. - destruct (mul_zero_why _ _ Hcc) as [Hccc|Hccc]; subst; intuition; apply Ha_nonzero. - - + replace (inject 2%Z) with (1+1) in Hccc by field; intuition. - - + rewrite <- a_square; simpl; rewrite Hccc; field. + destruct (mul_zero_why _ _ Hc) as [Hcc|Hcc]; subst; intuition. + destruct (mul_zero_why _ _ Hcc) as [Hccc|Hccc]; subst; intuition. + apply Ha_nonzero; field. Qed. Lemma edwardsAddCompletePlus x1 y1 x2 y2 : onCurve (x1,y1) -> @@ -604,12 +605,12 @@ End CompleteTwistedEdwardsFacts. Module Type Minus1Params (Import M : Modulus) <: TwistedEdwardsParams M. Module Export GFDefs := GaloisField M. + Axiom modulus_odd : (primeToZ M.modulus > 2)%Z. Local Open Scope GF_scope. - Axiom char_gt_2 : (1+1) <> 0. + Axiom char_gt_2 : inject 2 <> 0. Definition a := inject (- 1). Axiom a_nonzero : a <> 0. - Parameter sqrt_a : GF. - Axiom a_square : sqrt_a^2 = a. + Axiom a_square : exists sqrt_a, sqrt_a^2 = a. Parameter d : GF. Axiom d_nonsquare : forall x, x * x <> d. End Minus1Params. @@ -680,7 +681,7 @@ Module ExtendedM1 (M : Modulus) (Import P : Minus1Params M) <: CompleteTwistedEd extended_tac. Qed. - Local Notation "2" := (1+1). + Local Notation "2" := (inject 2). (** Second equation from <http://eprint.iacr.org/2008/522.pdf> section 3.1, also <https://www.hyperelliptic.org/EFD/g1p/auto-twisted-extended-1.html#addition-add-2008-hwcd-3> and <https://tools.ietf.org/html/draft-josefsson-eddsa-ed25519-03> *) Definition unifiedAdd (P1 P2 : point) : point := let '(X1, Y1, Z1, T1) := P1 in diff --git a/src/Galois/EdDSA.v b/src/Galois/EdDSA.v index 68b8867b8..c0699f316 100644 --- a/src/Galois/EdDSA.v +++ b/src/Galois/EdDSA.v @@ -25,7 +25,7 @@ Notation "'encoding' 'of' T 'as' B" := (Encoding T B) (at level 50). (* Spec from <https://eprint.iacr.org/2015/677.pdf> *) Module Type EdDSAParams. Parameter q : Prime. - Axiom q_odd : q > 2. + Axiom q_odd : (q > 2)%Z. (* Choosing q sufficiently large is important for security, since the size of * q constrains the size of l below. *) @@ -66,9 +66,8 @@ Module Type EdDSAParams. * on average to determine an EdDSA secret key from an EdDSA public key *) Parameter a : GF. - Parameter sqrt_a : GF. Axiom a_nonzero : a <> 0%GF. - Axiom a_square : sqrt_a^2 = a. + Axiom a_square : exists sqrt_a, sqrt_a^2 = a. (* The usual recommendation for best performance is a = −1 if q mod 4 = 1, * and a = 1 if q mod 4 = 3. * The original specification of EdDSA did not include this parameter: @@ -83,16 +82,12 @@ Module Type EdDSAParams. * This set forms a group with neutral element 0 = (0, 1) under the * twisted Edwards addition law. *) - (* We have an odd prime *) - Axiom char_gt_2: 1+1 <> 0. - Module CurveParameters <: TwistedEdwardsParams Modulus_q. Module GFDefs := GFDefs. + Definition modulus_odd : (Modulus_q.modulus > 2)%Z := q_odd. Definition a : GF := a. Definition a_nonzero := a_nonzero. Definition a_square := a_square. - Definition char_gt_2 := char_gt_2. - Definition sqrt_a := sqrt_a. Definition d := d. Definition d_nonsquare := d_nonsquare. End CurveParameters. diff --git a/src/Specific/EdDSA25519.v b/src/Specific/EdDSA25519.v index 194f94385..612b39641 100644 --- a/src/Specific/EdDSA25519.v +++ b/src/Specific/EdDSA25519.v @@ -9,25 +9,23 @@ Require Import Decidable. Require Import Omega. Module Modulus25519 <: Modulus. - Local Open Scope Z_scope. Definition two_255_19 := two_p 255 - 19. Lemma two_255_19_prime : prime two_255_19. Admitted. Definition prime25519 := exist _ two_255_19 two_255_19_prime. Definition modulus := prime25519. End Modulus25519. +Lemma prime_l : prime (252 + 27742317777372353535851937790883648493). Admitted. + Local Open Scope nat_scope. Module EdDSA25519_Params <: EdDSAParams. Definition q : Prime := Modulus25519.modulus. Ltac prime_bound := pose proof (prime_ge_2 q (proj2_sig q)); try omega. - Lemma q_odd : Z.to_nat q > 2. + Lemma q_odd : (primeToZ q > 2)%Z. Proof. - assert (q >= 0)%Z by (cbv; congruence). - assert (q > 2)%Z by (simpl; cbv; auto). - rewrite Nat2Z.inj_gt. - rewrite Z2Nat.id by omega; auto. + cbv; congruence. Qed. Module Modulus_q := Modulus25519. @@ -119,31 +117,27 @@ Module EdDSA25519_Params <: EdDSAParams. Qed. (* TODO *) - Parameter d : GF. - Parameter sqrt_a : GF. + Definition d : GF := (-121665 / 121666)%Z. Axiom d_nonsquare : forall x, x^2 <> d. - Axiom a_square: (sqrt_a^2 = a)%GF. - Axiom char_gt_2: (1+1 <> 0)%GF. + Axiom a_square: exists sqrt_a, (sqrt_a^2 = a)%GF. Module CurveParameters <: TwistedEdwardsParams Modulus_q. Module GFDefs := GFDefs. + Definition modulus_odd : (primeToZ Modulus_q.modulus > 2)%Z := q_odd. Definition a : GF := a. - Definition sqrt_a := sqrt_a. Definition a_nonzero := a_nonzero. Definition a_square := a_square. Definition d := d. Definition d_nonsquare := d_nonsquare. - Definition char_gt_2 := char_gt_2. End CurveParameters. Module Facts := CompleteTwistedEdwardsFacts Modulus_q CurveParameters. Module Import Curve := Facts.Curve. - (* TODO *) + (* TODO: B = decodePoint (y=4/5, x="positive") *) Parameter B : point. Axiom B_not_identity : B <> zero. - (* TODO *) - Parameter l : Prime. + Definition l : Prime := exist _ (252 + 27742317777372353535851937790883648493)%Z prime_l. Axiom l_odd : (Z.to_nat l > 2)%nat. Axiom l_order_B : (scalarMult (Z.to_nat l) B) = zero. @@ -197,6 +191,7 @@ Module EdDSA25519_Params <: EdDSAParams. end. Lemma Fl_encoding_valid : forall x, Fl_dec (Fl_enc x) = Some x. Proof. + Opaque l. unfold Fl_enc, Fl_dec; intros. assert (proj1_sig x < (Z.to_nat l)). { destruct x; simpl. @@ -210,6 +205,7 @@ Module EdDSA25519_Params <: EdDSAParams. do 2 (simpl in *; f_equal). apply Eqdep_dec.UIP_dec. apply eq_nat_dec. + Transparent l. Qed. Definition FlEncoding := Build_Encoding {s:nat | s mod (Z.to_nat l) = s} (word b) Fl_enc Fl_dec Fl_encoding_valid. |