From bef57ecff64515be2741da3e3e780a19af56b956 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Thu, 17 Sep 2015 23:50:38 -0400 Subject: Curves: elliptic curve point format record declarations and some invariants --- src/Curves/Curve25519.v | 35 ++++++-- src/Curves/PointFormats.v | 207 ++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 234 insertions(+), 8 deletions(-) create mode 100644 src/Curves/PointFormats.v (limited to 'src/Curves') diff --git a/src/Curves/Curve25519.v b/src/Curves/Curve25519.v index 8c34ea098..fc6cbb104 100644 --- a/src/Curves/Curve25519.v +++ b/src/Curves/Curve25519.v @@ -1,21 +1,40 @@ - Require Import Zpower ZArith Znumtheory. Require Import Crypto.Galois.GaloisField Crypto.Galois.GaloisFieldTheory. +Require Import Crypto.Curves.PointFormats. -Definition prime25519 : Prime. - exists ((two_p 255) - 19). - (* *) +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. +Local Notation p := two_255_19. + Module Modulus25519 <: Modulus. Definition modulus := prime25519. End Modulus25519. -Module GaloisTheory25519 := GaloisFieldTheory Modulus25519. - Module Curve25519. - Import Modulus25519 GaloisTheory25519.Field GaloisTheory25519. + Module PointFormats25519 := PointFormats Modulus25519. + Import Modulus25519 PointFormats25519 PointFormats25519.Theory PointFormats25519.Field. + Local Open Scope GF_scope. + + Definition A : GF := ZToGF 486662. + Definition d : GF := ((0 -ZToGF 121665) / (ZToGF 121666))%GF. + + + Definition montgomeryOnCurve25519 := montgomeryOnCurve 1 A. + Definition m1TwistedOnCurve25519 := twistedOnCurve (0 -1) d. + + Definition identityTwisted : twisted := mkTwisted 0 1. + + Lemma identityTwistedOnCurve : m1TwistedOnCurve25519 identityTwisted. + unfold m1TwistedOnCurve25519, twistedOnCurve, identityTwisted. + simpl; field. + Qed. - (* Prove some theorems! *) + Definition basepointY := ZToGF 4 / ZToGF 5. + (* TODO(andreser): implement (in PointFormats) recoverX from *) End Curve25519. diff --git a/src/Curves/PointFormats.v b/src/Curves/PointFormats.v new file mode 100644 index 000000000..b30831c58 --- /dev/null +++ b/src/Curves/PointFormats.v @@ -0,0 +1,207 @@ + +Require Import Crypto.Galois.GaloisField Crypto.Galois.GaloisFieldTheory. +Require Import Tactics.VerdiTactics. + +(** Theory of elliptic curves over prime fields for cryptographic applications, +with focus on the curves in *) +Module PointFormats (M: Modulus). + Module Field := GaloisField M. + Module Theory := GaloisFieldTheory M. + Import M Field Theory. + Local Open Scope GF_scope. + Local Notation "2" := (1+1). + Local Notation "3" := (1+1+1). + Local Notation "27" := (3*3*3). + + (** [weierstrass] represents a point on an elliptic curve using Weierstrass + * coordinates () definition 13.1*) + Record weierstrass := mkWeierstrass {weierstrassX : GF; weierstrassY : GF}. + Definition weierstrassOnCurve (a1 a2 a3 a4 a5 a6:GF) (P : weierstrass) : Prop := + let x := weierstrassX P in + let y := weierstrassY P in + y^2 + a1*x*y + a3*y = x^3 + a2*x^2 + a4*x + a6. + + (** [montgomery] represents a point on an elliptic curve using Montgomery + * coordinates (see ) *) + Record montgomery := mkMontgomery {montgomeryX : GF; montgomeryY : GF}. + Definition montgomeryOnCurve (B A:GF) (P : montgomery) : Prop := + let x := montgomeryX P in + let y := montgomeryY P in + B*y^2 = x^3 + A*x^2 + x. + + (** see section 13.2.3.c and *) + Definition montgomeryToWeierstrass (B A:GF) (P : montgomery) : weierstrass := + let x := montgomeryX P in + let y := montgomeryY P in + mkWeierstrass (x/B + A/(3*B)) (y/B). + + Lemma montgomeryToWeierstrassOnCurve : forall (B A:GF) (P:montgomery), + let a4 := 1/B^2 - A^2/(3*B^2) in + let a6 := 0- A^3/(27*B^3) - a4*A/(3*B) in + let P' := montgomeryToWeierstrass B A P in + montgomeryOnCurve B A P -> weierstrassOnCurve 0 0 0 a4 0 a6 P'. + Proof. + intros. + unfold montgomeryToWeierstrass, montgomeryOnCurve, weierstrassOnCurve in *. + remember (weierstrassY P') as y in *. + remember (weierstrassX P') as x in *. + remember (montgomeryX P) as u in *. + remember (montgomeryY P) as v in *. + field_simplify. + subst P'; simpl in Heqy, Heqx. + clear P Hequ Heqv. + (* This is not currently important and makes field run out of memory. Maybe + * because I transcribed it incorrectly... *) + Abort. + + (** [montgomeryxFrac] represents a point on an elliptic curve using Montgomery x + * coordinate stored as fraction as in + * appendix B. *) + Record montgomeryXFrac := mkMontgomeryXFrac {montgomeryXFracX : GF; montgomeryXFracZ : GF}. + Definition montgomeryToMontgomeryXFrac P := mkMontgomeryXFrac (montgomeryX P) 1. + Definition montgomeryXFracToMontgomeryX P : GF := (montgomeryXFracX P) / (montgomeryXFracZ P). + + (** [twisted] represents a point on an elliptic curve using twisted Edwards + * coordinates (see + * , and ) *) + Record twisted := mkTwisted {twistedX : GF; twistedY : GF}. + Definition twistedOnCurve (a d:GF) (P : twisted) : Prop := + let x := twistedX P in + let y := twistedY P in + a*x^2 + y^2 = 1 + d*x^2*y^2. + + (* Theorem 3.2. *) + (* TODO: exceptional points *) + Definition twistedToMontfomery (a d:GF) (P : twisted) : montgomery := + let x := twistedX P in + let y := twistedY P in + mkMontgomery ((1+y)/(1-y)) ((1+y)/((1-y)*x)). + Definition montgomeryToTwisted (B A:GF) (P : montgomery) : twisted := + let X := montgomeryX P in + let Y := montgomeryY P in + mkTwisted (X/Y) ((X-1)/(X+1)). + + (** [projective] represents a point on an elliptic curve using projective + * Edwards coordinates for twisted edwards curves with a=-1 (see + * + * ) *) + Record projective := mkProjective {projectiveX : GF; projectiveY : GF; projectiveZ : GF}. + Definition twistedToProjective (P : twisted) : projective := + let x := twistedX P in + let y := twistedY P in + mkProjective x y 1. + + Definition projectiveToTwisted (P : projective) : twisted := + let X := projectiveX P in + let Y := projectiveY P in + let Z := projectiveZ P in + mkTwisted (X/Z) (Y/Z). + + (** [extended] represents a point on an elliptic curve using extended projective + * Edwards coordinates with twist a=-1 (see ). *) + Record extended := mkExtended {extendedToProjective : projective; extendedT : GF}. + Definition extendedValid (P : extended) : Prop := + let pP := extendedToProjective P in + let X := projectiveX pP in + let Y := projectiveY pP in + let Z := projectiveZ pP in + let T := extendedT P in + X*Y = Z*T. + + Definition twistedToExtended (P : twisted) : extended := + let x := twistedX P in + let y := twistedY P in + mkExtended (mkProjective x y 1) (x*y). + + Definition extendedToTwisted (P : extended) : twisted := + projectiveToTwisted (extendedToProjective P). + + (** [precomputed] represents a point on an elliptic curve using "precomputed" + * Edwards coordinates, as used for fixed-base scalar multiplication + * (see section 4: addition). *) + Record precomputed := mkPrecomputed {precomputedSum : GF; + precomputedDifference : GF; + precomputed2dxy : GF}. + Definition twistedToPrecomputed (d:GF) (P : twisted) : precomputed := + let x := twistedX P in + let y := twistedY P in + mkPrecomputed (y+x) (y-x) (2*d*x*y). + + + (** *) + Definition twistedAdd (a d:GF) (P1 P2 : twisted) : twisted := + let x1 := twistedX P1 in + let y1 := twistedY P1 in + let x2 := twistedX P2 in + let y2 := twistedY P2 in + mkTwisted + ((x1*y2 + y1*x2)/(1 + 2*d*x1*x2*y1*y2)) + ((y1*y2 - a*x1*x2)/(1 - 2*d*x1*x2*y1*y2)) + . + + (** From *) + Definition extendedM1Add (d:GF) (P1 P2 : extended) : extended := + let pP1 := extendedToProjective P1 in + let X1 := projectiveX pP1 in + let Y1 := projectiveY pP1 in + let Z1 := projectiveZ pP1 in + let T1 := extendedT P1 in + let pP2 := extendedToProjective P2 in + let X2 := projectiveX pP2 in + let Y2 := projectiveY pP2 in + let Z2 := projectiveZ pP2 in + let T2 := extendedT P2 in + let A := (Y1-X1)*(Y2-X2) in + let B := (Y1+X1)*(Y2+X2) in + let C := T1*2*d*T2 in + let D := Z1*2*Z2 in + let E := B-A in + let F := D-C in + let G := D+C in + let H := B-A in + let X3 := E*F in + let Y3 := G*H in + let T3 := E*H in + let Z3 := F*G in + mkExtended (mkProjective X3 Y3 Z3) T3. + + Lemma extendeM1dAddCon : forall (d:GF) + (P1 P2 P3 : extended) (HeqP3 : P3 = extendedM1Add d P1 P2), + extendedValid P3. + Proof. + intros. + destruct P1 as [[X1 Y1 Z1] T1]. + destruct P2 as [[X2 Y2 Z2] T2]. + destruct P3 as [[X3 Y3 Z3] T3]. + unfold extendedValid, extendedToProjective, projectiveToTwisted, twistedX, twistedY in *. + invcs HeqP3. + + field. + Qed. + + Lemma extendedM1AddRep : forall (d:GF) (P1 P2 : extended) (tP1 tP2 : twisted) + (P1con : extendedValid P1) (P1rep : extendedToTwisted P1 = tP1) + (P2con : extendedValid P2) (P2rep : extendedToTwisted P2 = tP2), + twistedAdd (0-1) d tP1 tP2 = extendedToTwisted (extendedM1Add d P1 P2). + Proof. + intros. + destruct P1 as [[X1 Y1 Z1] T1]; destruct P2 as [[X2 Y2 Z2] T2]. + unfold extendedValid, twistedAdd, extendedToTwisted, extendedToProjective, projectiveToTwisted, twistedX, twistedY in *. + break_let; break_let. + invcs P1rep; invcs P2rep. + + f_equal. + + assert (T1 = X1 * Y1 / Z1). + + (* + FIXME: + In nested Ltac calls to "field" and + "field_lookup PackField ltac:FIELD [ ] G" (expanded to + "field_lookup [ ] (T1 = X1 * Y2 / Z2)"), last call failed. + Error: cannot find a declared field structure over "GF" + *) + + Abort. + +End PointFormats. -- cgit v1.2.3