diff options
-rw-r--r-- | src/Curves/PointFormats.v | 10 | ||||
-rw-r--r-- | src/Galois/EdDSA.v | 56 |
2 files changed, 23 insertions, 43 deletions
diff --git a/src/Curves/PointFormats.v b/src/Curves/PointFormats.v index 5bc0ecd85..430a48c82 100644 --- a/src/Curves/PointFormats.v +++ b/src/Curves/PointFormats.v @@ -5,8 +5,10 @@ Require Import Tactics.VerdiTactics. Module TwistedEdwardsDefs (Import M : Modulus). Module Export GT := GaloisTheory M. Open Scope GF_scope. - Definition twistedA := { a : GF | a <> 0 /\ exists sqrt_a, sqrt_a^2 = a }. - Definition twistedD := { d : GF | forall not_sqrt_d, not_sqrt_d^2 <> d }. + Definition isSquareAndNonzero (a : GF) := a <> 0 /\ exists sqrt_a, sqrt_a^2 = a. + Definition isNonSquare (d : GF) := forall not_sqrt_d, not_sqrt_d^2 <> d. + Definition twistedA := { a : GF | isSquareAndNonzero a }. + Definition twistedD := { d : GF | isNonSquare d }. Definition twistedAToGF (a : twistedA) := proj1_sig a. Coercion twistedAToGF : twistedA >-> GF. Definition twistedDToGF (d : twistedD) := proj1_sig d. @@ -61,7 +63,7 @@ Module Type CompleteTwistedEdwardsPointFormat (M : Modulus) (Import P : TwistedE End CompleteTwistedEdwardsPointFormat. Module CompleteTwistedEdwardsFacts (M : Modulus) (Import P : TwistedEdwardsParams M). - Module Import Curve := CompleteTwistedEdwardsCurve M P. + Module Export Curve := CompleteTwistedEdwardsCurve M P. Lemma twistedAddCompletePlus : forall (P1 P2:point) (oc1:onCurve P1) (oc2:onCurve P2), let x1 := projX P1 in @@ -114,10 +116,8 @@ End CompleteTwistedEdwardsFacts. Module Minus1Twisted (Import M : Modulus). Module Minus1Params <: TwistedEdwardsParams M. Module Export D := TwistedEdwardsDefs M. - Definition isSquareAndNonzero (a : GF) := a <> 0 /\ exists sqrt_a, sqrt_a^2 = a. Axiom minusOneIsSquareAndNonzero : isSquareAndNonzero (0 - 1). Definition a : twistedA := exist _ _ minusOneIsSquareAndNonzero. - Parameter d : twistedD. End Minus1Params. Import Minus1Params. diff --git a/src/Galois/EdDSA.v b/src/Galois/EdDSA.v index 45ed05243..bb256248d 100644 --- a/src/Galois/EdDSA.v +++ b/src/Galois/EdDSA.v @@ -7,26 +7,6 @@ Require Import Util.ListUtil Util.CaseUtil Util.ZUtil. Require Import VerdiTactics. Local Open Scope Z_scope. -Module Type PointFormatsSpec (Import Q : Modulus). - Module Import GT := GaloisTheory Q. - - Parameter a : GF. - - Parameter d : GF. - - Record point := mkPoint{x : GF; y : GF}. - Definition id := (mkPoint 0 1)%GF. - - Parameter onCurve : point -> Prop. - - Parameter scalar_mul : GF -> point -> point. - Axiom scalar_mul_onCurve : forall x P, onCurve P -> onCurve (scalar_mul x P). - - Parameter add : point -> point -> point. - Axiom add_onCurve : forall P Q, onCurve P -> onCurve Q -> onCurve (add P Q). - Axiom add_id : forall P, add P id = P. -End PointFormatsSpec. - Module Type EdDSAParams. (* Spec from https://eprint.iacr.org/2015/677.pdf *) @@ -42,7 +22,7 @@ Module Type EdDSAParams. Module Modulus_q <: Modulus. Definition modulus := q. End Modulus_q. - Module Import GF := GaloisTheory Modulus_q. + Module Import Defs := TwistedEdwardsDefs Modulus_q. (* * An integer b with 2^(b − 1) > q. @@ -93,17 +73,22 @@ Module Type EdDSAParams. * The original specification of EdDSA did not include this parameter: * it implicitly took a = −1 (and required q mod 4 = 1). *) - Parameter a : GF. - Axiom a_nonzero : a <> 0%GF. - Axiom a_square: exists x, (x * x = a)%GF. + Parameter a : twistedA. (* * A non-square element d of Fq. * The exact choice of d (together with a and q) is important for security, * and is the main topic considered in “curve selection”. *) - Definition d : GF := PF.d. - Axiom d_not_square : forall x, ((x * x = d)%GF -> False). + Parameter d : twistedD. + + Module Parameters <: TwistedEdwardsParams Modulus_q. + Definition a := a. + Definition d := d. + Module D := Defs. + End Parameters. + + Module Export Facts := CompleteTwistedEdwardsFacts Modulus_q Parameters. (* * An element B \neq (0, 1) of the set @@ -111,10 +96,9 @@ Module Type EdDSAParams. * This set forms a group with neutral element 0 = (0, 1) under the * twisted Edwards addition law. *) - Declare Module PF : PointFormatsSpec Modulus_q. - Parameter B : PF.point. - Axiom B_valid : PF.onCurve B. - Axiom B_not_identity : B = PF.id -> False. + Parameter B : point. + Axiom B_valid : onCurve B. + Axiom B_not_identity : B = zero -> False. (* * An odd prime l such that lB = 0 and (2^c)l = #E. @@ -141,24 +125,19 @@ Module Type EdDSAParams. End EdDSAParams. Module Type EdDSA (Import P : EdDSAParams). - Import P.PF P.GF. Parameter encode_point : point -> word b. Parameter decode_point : word b -> point. - Record secret. + Parameter secret : Type. Parameter public : secret -> word b. Parameter signature : secret -> forall n, word n -> word (b + b). End EdDSA. Module EdDSAImpl (Import P : EdDSAParams) <: EdDSA P. - Import P.PF P.GF. Definition encode_point (p : point) := wzero b. (* TODO *) + Definition decode_point (w : word b) := zero. (* TODO *) - Definition decode_point (w : word b) := id. (* TODO *) - - (* Utilities for words -- TODO : move *) Definition leading_ones n := natToWord b (wordToNat (wone n)). Definition c_to_n_window := wxor (leading_ones c) (leading_ones n). - (* Precompute s and the high half of H(k) *) Record secret := mkSecret{ key : word b; @@ -168,7 +147,8 @@ Module EdDSAImpl (Import P : EdDSAParams) <: EdDSA P. hash_high_def : hash_high = split2 b b (H b key) }. - Definition public (sk : secret) := H b (encode_point (scalar_mul (inject (s sk)) B)). + (* Needs scalar multiplication: + * Definition public (sk : secret) := H b (encode_point (scalar_mul (inject (s sk)) B)). *) Definition signature (sk : secret) n (w : word n) := wzero (b + b). |