From 13c4509d4fc43a56284ad592e9f893692b86a062 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Tue, 15 Dec 2015 18:47:55 -0500 Subject: PointFormats: all Edwards25519 points are onCurve --- src/Curves/Curve25519.v | 41 +++- src/Curves/PointFormats.v | 501 ++++++++++++++++++++++------------------------ src/Galois/EdDSA.v | 60 +++--- 3 files changed, 296 insertions(+), 306 deletions(-) (limited to 'src') diff --git a/src/Curves/Curve25519.v b/src/Curves/Curve25519.v index 8dc513a28..edcf6a24c 100644 --- a/src/Curves/Curve25519.v +++ b/src/Curves/Curve25519.v @@ -2,14 +2,36 @@ Require Import Zpower ZArith Znumtheory. Require Import Crypto.Galois.Galois Crypto.Galois.GaloisTheory Crypto.Galois.ComputationalGaloisField. Require Import Crypto.Curves.PointFormats. -Module Curve25519. - Import M. - Module Import GT := GaloisTheory M. - Local Open Scope GF_scope. +Definition two_255_19 := 2^255 - 19. (* *) +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 := GaloisDefs Modulus25519. + Coercion inject : Z >-> GF. + + Definition a : GF := -1. + Definition d : GF := -121665 / 121666. + + Lemma a_nonzero : a <> 0. + Proof. + discriminate. + Qed. + + Lemma a_square : exists x, x * x = a. + Proof. + unfold a. + exists 19681161376707505956807079304988542015446066515923890162744021073123829784752. + (* vm_compute runs out of memory. *) + Admitted. - Definition A : GF := ZToGF 486662. - Definition d : GF := ((0 -ZToGF 121665) / (ZToGF 121666))%GF. + Lemma d_nonsquare : forall x, x * x <> d. + (* *) + Admitted. + Definition A : GF := 486662. (* Definition montgomeryOnCurve25519 := montgomeryOnCurve 1 A. *) (* Module-izing Twisted was a breaking change @@ -24,7 +46,8 @@ Module Curve25519. *) - Definition basepointY := ZToGF 4 / ZToGF 5. - (* TODO(andreser): implement (in PointFormats) recoverX from *) -End Curve25519. + Definition basepointY := 4 / 5. +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 4c5572ea7..6db178aea 100644 --- a/src/Curves/PointFormats.v +++ b/src/Curves/PointFormats.v @@ -1,14 +1,14 @@ - Require Import Crypto.Galois.Galois Crypto.Galois.GaloisTheory Crypto.Galois.ComputationalGaloisField. Require Import Tactics.VerdiTactics. +Require Import Logic.Eqdep_dec. -Module TwistedEdwardsDefs (M : Modulus). +Module GaloisDefs (M : Modulus). Module Export GT := GaloisTheory M. Open Scope GF_scope. -End TwistedEdwardsDefs. +End GaloisDefs. Module Type TwistedEdwardsParams (M : Modulus). - Module Export Defs := TwistedEdwardsDefs M. + Module Export GFDefs := GaloisDefs M. Parameter a : GF. Axiom a_nonzero : a <> 0. Axiom a_square : exists x, x * x = a. @@ -22,304 +22,293 @@ Module CompleteTwistedEdwardsCurve (M : Modulus) (Import P : TwistedEdwardsParam * * *) - Record point := mkPoint {projX : GF; projY : GF}. - Notation "'(' x ',' y ')'" := (mkPoint x y). - Definition zero := (0, 1). - Definition unifiedAdd (P1 P2 : point) : point := - let x1 := projX P1 in - let y1 := projY P1 in - let x2 := projX P2 in - let y2 := projY P2 in - mkPoint - ((x1*y2 + y1*x2)/(1 + d*x1*x2*y1*y2)) - ((y1*y2 - a*x1*x2)/(1 - d*x1*x2*y1*y2)) - . - - Definition onCurve : point -> Prop := fun P => - let x := projX P in - let y := projY P in - a*x^2 + y^2 = 1 + d*x^2*y^2. - + Definition onCurve P := let '(x,y) := P in a*x^2 + y^2 = 1 + d*x^2*y^2. + Definition point := { P | onCurve P}. + Definition mkPoint := exist onCurve. + + Definition projX (P:point) := fst (proj1_sig P). + Definition projY (P:point) := snd (proj1_sig P). + + Definition checkOnCurve x y : if Zbool.Zeq_bool (a*x^2 + y^2) (1 + d*x^2*y^2) then point else True. + break_if. exists (x, y). exact (GFdecidable _ _ Heqb). trivial. + Defined. + Hint Unfold onCurve mkPoint. + + Definition zero : point. exists (0, 1). + abstract (unfold onCurve; ring). + Defined. + + Definition unifiedAdd' (P1' P2' : (GF*GF)) := + let '(x1, y1) := P1' in + let '(x2, y2) := P2' in + (((x1*y2 + y1*x2)/(1 + d*x1*x2*y1*y2)) , ((y1*y2 - a*x1*x2)/(1 - d*x1*x2*y1*y2))). + + Definition unifiedAdd (P1 P2 : point) : point. refine ( + let 'exist P1' pf1 := P1 in + let 'exist P2' pf2 := P2 in + mkPoint (unifiedAdd' P1' P2') _). + Proof. + destruct P1' as [x1 y1], P2' as [x2 y2]; unfold unifiedAdd', onCurve. + admit. (* field will likely work here, but I have not done this by hand *) + Defined. Local Infix "+" := unifiedAdd. - (* Naive implementation *) - Fixpoint scalarMultSpec (n:nat) (P : point) : point := + Fixpoint scalarMult (n:nat) (P : point) : point := match n with | O => zero - | S n' => P + scalarMultSpec n' P + | S n' => P + scalarMult n' P end . - - (* TODO: non-naive *) - Definition scalarMult := scalarMultSpec. - End CompleteTwistedEdwardsCurve. + Module Type CompleteTwistedEdwardsPointFormat (M : Modulus) (Import P : TwistedEdwardsParams M). Module Curve := CompleteTwistedEdwardsCurve M P. Parameter point : Type. - Parameter mkPoint : forall (x y:GF), point. - Parameter projX : point -> GF. - Parameter projY : point -> GF. + Parameter encode : (GF*GF) -> point. + Parameter decode : point -> (GF*GF). Parameter unifiedAdd : point -> point -> point. - Parameter rep : point -> Curve.point -> Prop. + Parameter rep : point -> (GF*GF) -> Prop. Local Notation "P '~=' rP" := (rep P rP) (at level 70). - Axiom mkPoint_rep: forall x y, mkPoint x y ~= Curve.mkPoint x y. + + Axiom encode_rep: forall P, encode P ~= P. + Axiom decode_rep : forall P rP, P ~= rP -> decode P = rP. Axiom unifiedAdd_rep: forall P Q rP rQ, Curve.onCurve rP -> Curve.onCurve rQ -> - P ~= rP -> Q ~= rQ -> (unifiedAdd P Q) ~= (Curve.unifiedAdd rP rQ). - Axiom projX_rep : forall P rP, P ~= rP -> projX P = Curve.projX rP. - Axiom projY_rep : forall P rP, P ~= rP -> projY P = Curve.projY rP. + P ~= rP -> Q ~= rQ -> (unifiedAdd P Q) ~= (Curve.unifiedAdd' rP rQ). End CompleteTwistedEdwardsPointFormat. Module CompleteTwistedEdwardsFacts (M : Modulus) (Import P : TwistedEdwardsParams M). Module Import Curve := CompleteTwistedEdwardsCurve M P. - Lemma twistedAddCompletePlus : forall (P1 P2:point) - (oc1:onCurve P1) (oc2:onCurve P2), - let x1 := projX P1 in - let y1 := projY P1 in - let x2 := projX P2 in - let y2 := projY P2 in + Lemma twistedAddCompletePlus : forall (P1 P2:point), + let '(x1, y1) := proj1_sig P1 in + let '(x2, y2) := proj1_sig P2 in (1 + d*x1*x2*y1*y2) <> 0. (* "Twisted Edwards Curves" section 6 *) Admitted. - Lemma twistedAddCompleteMinus : forall (P1 P2:point) - (oc1:onCurve P1) (oc2:onCurve P2), - let x1 := projX P1 in - let y1 := projY P1 in - let x2 := projX P2 in - let y2 := projY P2 in + Lemma twistedAddCompleteMinus : forall (P1 P2:point), + let '(x1, y1) := proj1_sig P1 in + let '(x2, y2) := proj1_sig P2 in (1 - d*x1*x2*y1*y2) <> 0. (* "Twisted Edwards Curves" section 6 *) Admitted. + Lemma point_eq : forall x1 x2 y1 y2, + x1 = x2 -> y1 = y2 -> + forall p1 p2, + mkPoint (x1, y1) p1 = mkPoint (x2, y2) p2. + Proof. + intros; subst; f_equal. + apply (UIP_dec). (* this is a hack. We actually don't care about the equality of the proofs. However, we *can* prove it, and knowing it lets us use the universal equality instead of a type-specific equivalence, which makes many things nicer. *) + admit. (* GF_eq_dec *) + Qed. + Hint Resolve point_eq. + Hint Unfold unifiedAdd onCurve. Ltac twisted := autounfold; intros; - repeat match goal with - | [ x : point |- _ ] => destruct x - end; simpl; repeat (ring || f_equal); field. + repeat (match goal with + | [ x : point |- _ ] => destruct x; unfold onCurve in * + | [ x : (GF*GF)%type |- _ ] => destruct x + | [ |- exist _ _ _ = exist _ _ _ ] => eapply point_eq + end; simpl; repeat (ring || f_equal)). Local Infix "+" := unifiedAdd. Lemma twistedAddComm : forall A B, (A+B = B+A). Proof. twisted. Qed. - Lemma twistedAddAssoc : forall A B C - (ocA:onCurve A) (ocB:onCurve B) (ocC:onCurve C), - (A+(B+C) = (A+B)+C). + Lemma twistedAddAssoc : forall A B C, A+(B+C) = (A+B)+C. Proof. - (* uh... I don't actually know where this is proven... *) + (* http://math.rice.edu/~friedl/papers/AAELLIPTIC.PDF *) Admitted. - Lemma zeroOnCurve : onCurve (0, 1). - Proof. - twisted. - Qed. Lemma zeroIsIdentity : forall P, P + zero = P. Proof. - admit. - Qed. + twisted. + (* the denominators are 1 and numerators are equal *) + Admitted. End CompleteTwistedEdwardsFacts. Module Type Minus1Params (Import M : Modulus) <: TwistedEdwardsParams M. - Module Export Defs := TwistedEdwardsDefs M. + Module Export GFDefs := GaloisDefs M. Open Scope GF_scope. - Definition a := 0 - 1. + Definition a := inject (- 1). Axiom a_nonzero : a <> 0. Axiom a_square : exists x, x * x = a. Parameter d : GF. Axiom d_nonsquare : forall x, x * x <> d. End Minus1Params. -Module Minus1Twisted (M : Modulus) (Import P : Minus1Params M). - Module Import Curve := CompleteTwistedEdwardsCurve M P. +Module Minus1Format (M : Modulus) (Import P : Minus1Params M) <: CompleteTwistedEdwardsPointFormat M P. + Module Import Facts := CompleteTwistedEdwardsFacts M P. + Module Import Curve := Facts.Curve. + (** [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}. + Local Notation "'(' X ',' Y ',' Z ')'" := (mkProjective X Y Z). + + Definition twistedToProjective (P : (GF*GF)) : projective := + let '(x, y) := P in (x, y, 1). + + Definition projectiveToTwisted (P : projective) : GF * GF := + let 'mkProjective X Y Z := P in + pair (X/Z) (Y/Z). + Hint Unfold projectiveToTwisted twistedToProjective. + + Lemma GFdiv_1 : forall x, x/1 = x. + Admitted. + Hint Resolve GFdiv_1. + + Lemma twistedProjectiveInv P : projectiveToTwisted (twistedToProjective P) = P. + Proof. + twisted; eapply GFdiv_1. + Qed. + + (** [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 point := extended. + Local Notation "'(' X ',' Y ',' Z ',' T ')'" := (mkExtended (X, Y, Z) T). + Definition extendedValid (P : point) : 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 + T = X*Y/Z. + + + Definition twistedToExtended (P : (GF*GF)) : point := + let '(x, y) := P in (x, y, 1, x*y). + Definition encode P := let '(x, y) := P in twistedToExtended (x, y). + + Definition decode (P : point) := + projectiveToTwisted (extendedToProjective P). + Local Hint Unfold extendedValid twistedToExtended decode projectiveToTwisted Curve.unifiedAdd'. + + Lemma twistedExtendedInv : forall P, + decode (twistedToExtended P) = P. + Proof. + twisted; eapply GFdiv_1. + Qed. + + Lemma twistedToExtendedValid : forall P, extendedValid (twistedToExtended P). + Proof. + autounfold. + destruct P. + simpl. + rewrite GFdiv_1; reflexivity. + Qed. + + Definition rep (P:point) (rP:(GF*GF)) : Prop := + decode P = rP /\ extendedValid P. + Local Notation "P '~=' rP" := (rep P rP) (at level 70). + Ltac rep := repeat progress (intros; autounfold; subst; auto; match goal with + | [ x : rep ?a ?b |- _ ] => destruct x + end). + + Lemma encode_rep : forall P, encode P ~= P. + Proof. + split. + apply twistedExtendedInv. + apply twistedToExtendedValid. + Qed. - Module Minus1Format <: CompleteTwistedEdwardsPointFormat M P. - Module Import Facts := CompleteTwistedEdwardsFacts M P. - (** [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}. - Local Notation "'(' X ',' Y ',' Z ')'" := (mkProjective X Y Z). - - Definition twistedToProjective (P : Curve.point) : projective := - let x := Curve.projX P in - let y := Curve.projY P in - (x, y, 1). - - Local Notation "'(' X ',' Y ')'" := (Curve.mkPoint X Y). - Definition projectiveToTwisted (P : projective) : Curve.point := - let X := projectiveX P in - let Y := projectiveY P in - let Z := projectiveZ P in - (X/Z, Y/Z). - - Hint Unfold projectiveToTwisted twistedToProjective. - - Lemma twistedProjectiveInv : forall P, - projectiveToTwisted (twistedToProjective P) = P. - Proof. - admit. - Qed. - - (** [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}. - (*Error: The kernel does not recognize yet that a parameter can be instantiated by an inductive type. Hint: you can rename the inductive type and give a definition to map the old name to the new name.*) - - Definition point := extended. - Local Notation "'(' X ',' Y ',' Z ',' T ')'" := (mkExtended (X, Y, Z) T). - Definition extendedValid (P : point) : 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 - T = X*Y/Z. - - - Definition twistedToExtended (P : Curve.point) : point := - let x := Curve.projX P in - let y := Curve.projY P in - (x, y, 1, x*y). - Definition mkPoint x y := twistedToExtended (x, y). - - Definition extendedToTwisted (P : point) : Curve.point := - projectiveToTwisted (extendedToProjective P). - Local Hint Unfold extendedValid twistedToExtended extendedToTwisted projectiveToTwisted Curve.unifiedAdd mkPoint. - - Lemma twistedExtendedInv : forall P, - extendedToTwisted (twistedToExtended P) = P. - Proof. - apply twistedProjectiveInv. - Qed. - - Lemma twistedToExtendedValid : forall (P : Curve.point), extendedValid (twistedToExtended P). - Proof. - autounfold. - destruct P. - simpl. - admit. - (* field. *) - Qed. - - Definition rep (P:point) (rP:Curve.point) : Prop := - extendedToTwisted P = rP /\ extendedValid P. - Lemma mkPoint_rep : forall x y, rep (mkPoint x y) (Curve.mkPoint x y). - Proof. - split. - apply twistedExtendedInv. - apply twistedToExtendedValid. - Qed. - Local Notation "P '~=' rP" := (rep P rP) (at level 70). - - Definition projX P := Curve.projX (extendedToTwisted P). - Definition projY P := Curve.projY (extendedToTwisted P). - - Ltac rep := repeat progress (intros; autounfold; subst; auto; match goal with - | [ x : rep ?a ?b |- _ ] => destruct x - end). - Lemma projX_rep : forall P rP, P ~= rP -> projX P = Curve.projX rP. - Proof. - rep. - Qed. - Lemma projY_rep : forall P rP, P ~= rP -> projY P = Curve.projY rP. - Proof. - rep. - Qed. - - Local Notation "2" := (1+1). - (** Second equation from section 3.1, also and *) - Definition unifiedAdd (P1 P2 : point) : point := - let k := 2 * d in - 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*k*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. - - Delimit Scope extendedM1_scope with extendedM1. - Infix "+" := unifiedAdd : extendedM1_scope. - - Lemma unifiedAddCon : forall (P1 P2:point) - (hv1:extendedValid P1) (hv2:extendedValid P2), - extendedValid (P1 + P2)%extendedM1. - Proof. - intros. - remember ((P1+P2)%extendedM1) as P3. - 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, Curve.projX, Curve.projY in *. - invcs HeqP3. - subst. - (* field. -- fails. but it works in sage: - sage -c 'var("d X1 X2 Y1 Y2 Z1 Z2"); - print(bool((((Y1 + X1) * (Y2 + X2) - (Y1 - X1) * (Y2 - X2)) * - ((Y1 + X1) * (Y2 + X2) - (Y1 - X1) * (Y2 - X2)) == - ((Y1 + X1) * (Y2 + X2) - (Y1 - X1) * (Y2 - X2)) * - (2 * Z1 * Z2 - 2 * ((0 - d) / a) * (X1 * Y1 / Z1) * (X2 * Y2 / Z2)) * - ((2 * Z1 * Z2 + 2 * ((0 - d) / a) * (X1 * Y1 / Z1) * (X2 * Y2 / Z2)) * - ((Y1 + X1) * (Y2 + X2) - (Y1 - X1) * (Y2 - X2))) / - ((2 * Z1 * Z2 - 2 * ((0 - d) / a) * (X1 * Y1 / Z1) * (X2 * Y2 / Z2)) * - (2 * Z1 * Z2 + 2 * ((0 - d) / a) * (X1 * Y1 / Z1) * (X2 * Y2 / Z2))))))' - Outputs: - True - *) - Admitted. - - Ltac extended0 := repeat progress (autounfold; simpl); intros; - repeat match goal with - | [ x : Curve.point |- _ ] => destruct x - | [ x : point |- _ ] => destruct x - | [ x : projective |- _ ] => destruct x - end; simpl in *; subst. - - Ltac extended := extended0; repeat (ring || f_equal)(*; field*). - - Lemma unifiedAddToTwisted : forall (P1 P2 : point) (tP1 tP2 : Curve.point) - (P1con : extendedValid P1) (P1on : Curve.onCurve tP1) (P1rep : extendedToTwisted P1 = tP1) - (P2con : extendedValid P2) (P2on : Curve.onCurve tP2) (P2rep : extendedToTwisted P2 = tP2), - extendedToTwisted (P1 + P2)%extendedM1 = Curve.unifiedAdd tP1 tP2. - Proof. - extended0. - apply f_equal2. - (* case 1 verified by hand: follows from field and completeness of edwards addition *) - (* field should work here *) - Admitted. - - Lemma unifiedAdd_rep: forall P Q rP rQ, Curve.onCurve rP -> Curve.onCurve rQ -> - P ~= rP -> Q ~= rQ -> (unifiedAdd P Q) ~= (Curve.unifiedAdd rP rQ). - Proof. - split; rep. - apply unifiedAddToTwisted; auto. - apply unifiedAddCon; auto. - Qed. - - Module Curve := Curve. - End Minus1Format. - -End Minus1Twisted. + Lemma decode_rep : forall P rP, P ~= rP -> decode P = rP. + Proof. + rep. + Qed. + + + Local Notation "2" := (1+1). + (** Second equation from section 3.1, also and *) + Definition unifiedAdd (P1 P2 : point) : point := + let k := 2 * d in + 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*k*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. + + Delimit Scope extendedM1_scope with extendedM1. + Infix "+" := unifiedAdd : extendedM1_scope. + + Lemma unifiedAddCon : forall (P1 P2:point) + (hv1:extendedValid P1) (hv2:extendedValid P2), + extendedValid (P1 + P2)%extendedM1. + Proof. + intros. + remember ((P1+P2)%extendedM1) as P3. + 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 in *. + invcs HeqP3. + subst. + (* field. -- fails. but it works in sage: +sage -c 'var("d X1 X2 Y1 Y2 Z1 Z2"); +print(bool((((Y1 + X1) * (Y2 + X2) - (Y1 - X1) * (Y2 - X2)) * +((Y1 + X1) * (Y2 + X2) - (Y1 - X1) * (Y2 - X2)) == +((Y1 + X1) * (Y2 + X2) - (Y1 - X1) * (Y2 - X2)) * +(2 * Z1 * Z2 - 2 * ((0 - d) / a) * (X1 * Y1 / Z1) * (X2 * Y2 / Z2)) * +((2 * Z1 * Z2 + 2 * ((0 - d) / a) * (X1 * Y1 / Z1) * (X2 * Y2 / Z2)) * +((Y1 + X1) * (Y2 + X2) - (Y1 - X1) * (Y2 - X2))) / +((2 * Z1 * Z2 - 2 * ((0 - d) / a) * (X1 * Y1 / Z1) * (X2 * Y2 / Z2)) * +(2 * Z1 * Z2 + 2 * ((0 - d) / a) * (X1 * Y1 / Z1) * (X2 * Y2 / Z2))))))' + Outputs: + True + *) + Admitted. + + Ltac extended0 := repeat progress (autounfold; simpl); intros; + repeat match goal with + | [ x : Curve.point |- _ ] => destruct x + | [ x : point |- _ ] => destruct x + | [ x : projective |- _ ] => destruct x + end; simpl in *; subst. + + Ltac extended := extended0; repeat (ring || f_equal)(*; field*). + + Lemma unifiedAddToTwisted : forall (P1 P2 : point) tP1 tP2 + (P1con : extendedValid P1) (P1on : Curve.onCurve tP1) (P1rep : decode P1 = tP1) + (P2con : extendedValid P2) (P2on : Curve.onCurve tP2) (P2rep : decode P2 = tP2), + decode (P1 + P2)%extendedM1 = Curve.unifiedAdd' tP1 tP2. + Proof. + extended0. + apply f_equal2. + (* case 1 verified by hand: follows from field and completeness of edwards addition *) + Admitted. + + Lemma unifiedAdd_rep: forall P Q rP rQ, Curve.onCurve rP -> Curve.onCurve rQ -> + P ~= rP -> Q ~= rQ -> (unifiedAdd P Q) ~= (Curve.unifiedAdd' rP rQ). + Proof. + split; rep. + apply unifiedAddToTwisted; auto. + apply unifiedAddCon; auto. + Qed. +End Minus1Format. (* @@ -443,13 +432,3 @@ Module WeirstrassMontgomery (Import M : Modulus). *) End WeirstrassMontgomery. - -(* FIXME: remove after [field] with modulus as a parameter (34d9f8a6e6a4be439d1c56a8b999d2c21ee12a46) is fixed *) -Require Import Zpower ZArith Znumtheory. -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. -Module M <: Modulus. - Definition modulus := prime25519. -End M. - diff --git a/src/Galois/EdDSA.v b/src/Galois/EdDSA.v index 7ab02718f..57b070148 100644 --- a/src/Galois/EdDSA.v +++ b/src/Galois/EdDSA.v @@ -5,6 +5,18 @@ Require Import Crypto.Galois.BaseSystem Crypto.Galois.GaloisTheory. Require Import Util.ListUtil Util.CaseUtil Util.ZUtil. Require Import VerdiTactics. +(* TODO : where should this be? *) +Definition wfirstn {m} {n} (w : word m) (H : (n <= m)%nat) : word n. + replace m with (n + (m - n))%nat in * by (symmetry; apply le_plus_minus; apply H) +. + exact (split1 n (m - n) w). +Defined. + +Lemma wtl_WS : forall b {n} (w : word n), wtl (WS b w) = w. +Proof. + auto. +Qed. + Class Encoding (T B:Type) := { enc : T -> B ; dec : B -> option T ; @@ -12,6 +24,7 @@ Class Encoding (T B:Type) := { }. Notation "'encoding' 'of' T 'as' B" := (Encoding T B) (at level 50). + (* Spec from *) Module Type EdDSAParams. Open Scope Z_scope. @@ -27,7 +40,7 @@ Module Type EdDSAParams. Module Modulus_q <: Modulus. Definition modulus := q. End Modulus_q. - Module Export CurveDefs := TwistedEdwardsDefs Modulus_q. + Module Export GFDefs := GaloisDefs Modulus_q. Parameter b : nat. Axiom b_valid : 2^(b - 1) > q. @@ -74,7 +87,7 @@ Module Type EdDSAParams. * This set forms a group with neutral element 0 = (0, 1) under the * twisted Edwards addition law. *) Module CurveParameters <: TwistedEdwardsParams Modulus_q. - Module Defs := CurveDefs. + Module GFDefs := GFDefs. Definition a : GF := a. Definition a_nonzero := a_nonzero. Definition a_square := a_square. @@ -85,7 +98,6 @@ Module Type EdDSAParams. Parameter B : point. (* element of E *) Axiom B_not_identity : B <> zero. - Axiom B_valid : onCurve B. (* * An odd prime l such that lB = 0 and (2^c)l = #E. @@ -110,21 +122,8 @@ Module Type EdDSAParams. *) Parameter H'_out_len : nat -> nat. Parameter H' : forall {n}, word n -> word (H'_out_len n). - End EdDSAParams. -(* TODO : where should this be? *) -Definition wfirstn {m} {n} (w : word m) (H : (n <= m)%nat) : word n. - replace m with (n + (m - n))%nat in * by (symmetry; apply le_plus_minus; apply H) -. - exact (split1 n (m - n) w). -Defined. - -Lemma wtl_WS : forall b {n} (w : word n), wtl (WS b w) = w. -Proof. - auto. -Qed. - Module EdDSADefs (Import P : EdDSAParams). Infix "++" := combine. Infix "*" := scalarMult. @@ -156,13 +155,13 @@ End EdDSADefs. Module Type EdDSA (Import P : EdDSAParams). Module Import Spec := EdDSADefs P. - (* FIXME: make [point] represent points on the curve *) Parameter PointEncoding : encoding of point as word b. Axiom encode_point_spec : forall P, enc P = encode_point_ref P. Parameter public : secretkey -> publickey. Axiom public_spec : forall sk, public sk = enc ((curveKey sk) * B). + (* TODO: use GF for both GF(q) and GF(l) *) Parameter sign : publickey -> secretkey -> forall {n}, word n -> signature. Axiom sign_spec : forall A_ sk {n} (M : word n), sign A_ sk M = let r := wordToNat (H (randKey sk ++ M)) in @@ -170,18 +169,14 @@ Module Type EdDSA (Import P : EdDSAParams). let S := (r + curveKey sk * wordToNat (H (enc R ++ A_ ++ M)))%nat mod (Z.to_nat l) in enc R ++ natToWord b S. - Parameter verify : publickey -> signature -> forall {n}, word n -> bool. - Axiom verify_spec : forall A_ sig {n} (M : word n), verify A_ sig M = true <-> + Parameter verify : publickey -> forall {n}, word n -> signature -> bool. + Axiom verify_spec : forall A_ sig {n} (M : word n), verify A_ M sig = true <-> ( let R_ := split1 b b sig in let S_ := split2 b b sig in let S := wordToNat S_ in - match dec A_ with - | None => False - | Some A => match dec R_ with - | None => False - | Some R => S * B = R + (wordToNat (H (R_ ++ A_ ++ M )) * A) - end - end. + exists A, dec A_ = Some A /\ + exists R, dec R_ = Some R /\ + S * B = R + (wordToNat (H (R_ ++ A_ ++ M )) * A) ). End EdDSA. Module EdDSAFacts (Import P : EdDSAParams) (Import Impl : EdDSA P). @@ -216,23 +211,16 @@ Module EdDSAFacts (Import P : EdDSAParams) (Import Impl : EdDSA P). Lemma l_gt_zero : (Z.to_nat l <> 0)%nat. Admitted. - (* TODO : move to TwistedEdwardsFacts *) - Lemma scalarMultOnCurve : forall n P, onCurve P -> onCurve (n * P). - Proof. - intros; induction n0; boring. - Admitted. - Hint Resolve scalarMultOnCurve. - (* TODO : move somewhere else (EdDSAFacts?) *) Lemma verify_valid_passes : forall sk {n} (M : word n), - verify (public sk) (sign (public sk) sk M) M = true. + verify (public sk) M (sign (public sk) sk M) = true. Proof. intros; rewrite verify_spec. intros; subst R_. rewrite decode_sign_split1. rewrite public_spec. - rewrite encoding_valid by auto. - rewrite encoding_valid by auto. + exists (curveKey sk * B); intuition; [apply encoding_valid|]. + exists (wordToNat (H (randKey sk ++ M)) * B); intuition; [apply encoding_valid|]. subst S S_. rewrite decode_sign_split2. remember (wordToNat (H (randKey sk ++ M))) as r. -- cgit v1.2.3