diff options
-rw-r--r-- | src/Curves/PointFormats.v | 69 | ||||
-rw-r--r-- | src/Galois/BaseSystem.v | 2 | ||||
-rw-r--r-- | src/Galois/EdDSA.v | 203 |
3 files changed, 204 insertions, 70 deletions
diff --git a/src/Curves/PointFormats.v b/src/Curves/PointFormats.v index 430a48c82..4c5572ea7 100644 --- a/src/Curves/PointFormats.v +++ b/src/Curves/PointFormats.v @@ -2,23 +2,18 @@ Require Import Crypto.Galois.Galois Crypto.Galois.GaloisTheory Crypto.Galois.ComputationalGaloisField. Require Import Tactics.VerdiTactics. -Module TwistedEdwardsDefs (Import M : Modulus). +Module TwistedEdwardsDefs (M : Modulus). Module Export GT := GaloisTheory M. Open Scope GF_scope. - 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. - Coercion twistedDToGF : twistedD >-> GF. End TwistedEdwardsDefs. Module Type TwistedEdwardsParams (M : Modulus). - Module Export D := TwistedEdwardsDefs M. - Parameter a : twistedA. - Parameter d : twistedD. + Module Export Defs := TwistedEdwardsDefs M. + Parameter a : GF. + 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 TwistedEdwardsParams. Module CompleteTwistedEdwardsCurve (M : Modulus) (Import P : TwistedEdwardsParams M). @@ -28,7 +23,8 @@ Module CompleteTwistedEdwardsCurve (M : Modulus) (Import P : TwistedEdwardsParam * <https://eprint.iacr.org/2015/677.pdf> *) 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 @@ -43,6 +39,20 @@ Module CompleteTwistedEdwardsCurve (M : Modulus) (Import P : TwistedEdwardsParam let x := projX P in let y := projY P in a*x^2 + y^2 = 1 + d*x^2*y^2. + + Local Infix "+" := unifiedAdd. + + (* Naive implementation *) + Fixpoint scalarMultSpec (n:nat) (P : point) : point := + match n with + | O => zero + | S n' => P + scalarMultSpec n' P + end + . + + (* TODO: non-naive *) + Definition scalarMult := scalarMultSpec. + End CompleteTwistedEdwardsCurve. Module Type CompleteTwistedEdwardsPointFormat (M : Modulus) (Import P : TwistedEdwardsParams M). @@ -63,7 +73,7 @@ Module Type CompleteTwistedEdwardsPointFormat (M : Modulus) (Import P : TwistedE End CompleteTwistedEdwardsPointFormat. Module CompleteTwistedEdwardsFacts (M : Modulus) (Import P : TwistedEdwardsParams M). - Module Export Curve := CompleteTwistedEdwardsCurve M P. + Module Import Curve := CompleteTwistedEdwardsCurve M P. Lemma twistedAddCompletePlus : forall (P1 P2:point) (oc1:onCurve P1) (oc2:onCurve P2), let x1 := projX P1 in @@ -101,8 +111,6 @@ Module CompleteTwistedEdwardsFacts (M : Modulus) (Import P : TwistedEdwardsParam (* uh... I don't actually know where this is proven... *) Admitted. - Local Notation "'(' x ',' y ')'" := (mkPoint x y). - Definition zero := (0, 1). Lemma zeroOnCurve : onCurve (0, 1). Proof. twisted. @@ -111,21 +119,24 @@ Module CompleteTwistedEdwardsFacts (M : Modulus) (Import P : TwistedEdwardsParam Proof. admit. Qed. -End CompleteTwistedEdwardsFacts. - -Module Minus1Twisted (Import M : Modulus). - Module Minus1Params <: TwistedEdwardsParams M. - Module Export D := TwistedEdwardsDefs M. - Axiom minusOneIsSquareAndNonzero : isSquareAndNonzero (0 - 1). - Definition a : twistedA := exist _ _ minusOneIsSquareAndNonzero. - Parameter d : twistedD. - End Minus1Params. - Import Minus1Params. - Module Import Curve := CompleteTwistedEdwardsCurve M Minus1Params. +End CompleteTwistedEdwardsFacts. - Module Minus1Format <: CompleteTwistedEdwardsPointFormat M Minus1Params. - Module Import Facts := CompleteTwistedEdwardsFacts M Minus1Params. +Module Type Minus1Params (Import M : Modulus) <: TwistedEdwardsParams M. + Module Export Defs := TwistedEdwardsDefs M. + Open Scope GF_scope. + Definition a := 0 - 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 <: 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 * <https://hyperelliptic.org/EFD/g1p/auto-edwards-projective.html> diff --git a/src/Galois/BaseSystem.v b/src/Galois/BaseSystem.v index 8197bed8d..28ae37233 100644 --- a/src/Galois/BaseSystem.v +++ b/src/Galois/BaseSystem.v @@ -39,7 +39,7 @@ Module BaseSystem (Import B:BaseCoefs). Lemma decode'_truncate : forall bs us, decode' bs us = decode' bs (firstn (length bs) us). Proof. - unfold decode, decode'; intros; f_equal; apply combine_truncate_l. + unfold decode'; intros; f_equal; apply combine_truncate_l. Qed. Fixpoint add (us vs:digits) : digits := diff --git a/src/Galois/EdDSA.v b/src/Galois/EdDSA.v index bb256248d..1f0792acb 100644 --- a/src/Galois/EdDSA.v +++ b/src/Galois/EdDSA.v @@ -1,5 +1,4 @@ Require Import ZArith. -Require Import List. Require Import Bedrock.Word. Require Import Crypto.Curves.PointFormats. Require Import Crypto.Galois.BaseSystem Crypto.Galois.GaloisTheory. @@ -17,32 +16,39 @@ Module Type EdDSAParams. * There are additional security concerns when q is not chosen to be prime. *) Parameter q : Prime. - Axiom q_odd : Z.odd q = true. + Axiom q_odd : q > 2. Module Modulus_q <: Modulus. Definition modulus := q. End Modulus_q. - Module Import Defs := TwistedEdwardsDefs Modulus_q. + Module Export CurveDefs := TwistedEdwardsDefs Modulus_q. (* * An integer b with 2^(b − 1) > q. * EdDSA public keys have exactly b bits, * and EdDSA signatures have exactly 2b bits. *) + (* Note: the parameter pred_b is (b - 1) to make proofs about the (b-1)-bit + * encoding easier *) Parameter b : nat. - Axiom b_valid : 2^((Z.of_nat b) - 1) > q. + Coercion Z.of_nat : nat >-> Z. + Axiom b_valid : 2^(b - 1) > q. + Definition secretkey : Type := word b. + Definition publickey : Type := word b. + Definition signature : Type := word (b + b). (* A (b − 1)-bit encoding of elements of the finite field Fq. *) - Parameter decode : word (b - 1) -> GF. - Parameter encode : GF -> word (b - 1). - Axiom consistent : forall x, decode( encode x) = x. + Parameter decode_scalar : word (b - 1) -> GF. + Parameter encode_scalar : GF -> word (b - 1). + Axiom decode_encode_scalar_consistent : forall x, decode_scalar (encode_scalar x) = x. + Axiom encode_decode_scalar_consistent : forall x, encode_scalar (decode_scalar x) = x. (* * A cryptographic hash function H producing 2b-bit output. * Conservative hash functions are recommended and do not have much * impact on the total cost of EdDSA. *) - Parameter H : forall n, word n -> word (b + b). + Parameter H : forall {n}, word n -> word (b + b). (* * An integer c \in {2, 3}. Secret EdDSA scalars are multiples of 2c. @@ -63,8 +69,8 @@ Module Type EdDSAParams. * on average to determine an EdDSA secret key from an EdDSA public key. *) Parameter n : nat. - Axiom n_gte_c : (n >= c)%nat. - Axiom n_lte_b : (n <= b)%nat. + Axiom n_ge_c : n >= c. + Axiom n_le_b : (n <= b)%nat. (* * A nonzero square element a of Fq. @@ -73,22 +79,28 @@ 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 : twistedA. + Parameter a : GF. + Axiom a_nonzero : a <> 0%GF. + Axiom a_square : exists x, x * x = a. (* * 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”. *) - Parameter d : twistedD. + Parameter d : GF. + Axiom d_nonsquare : forall x, x * x <> d. Module Parameters <: TwistedEdwardsParams Modulus_q. - Definition a := a. + Module Defs := CurveDefs. + Definition a : GF := a. + Definition a_nonzero := a_nonzero. + Definition a_square := a_square. Definition d := d. - Module D := Defs. + Definition d_nonsquare := d_nonsquare. End Parameters. - Module Export Facts := CompleteTwistedEdwardsFacts Modulus_q Parameters. + Module Export Curve := CompleteTwistedEdwardsCurve Modulus_q Parameters. (* * An element B \neq (0, 1) of the set @@ -97,8 +109,9 @@ Module Type EdDSAParams. * twisted Edwards addition law. *) Parameter B : point. + Axiom B_not_identity : B <> zero. Axiom B_valid : onCurve B. - Axiom B_not_identity : B = zero -> False. + Hint Resolve B_valid. (* * An odd prime l such that lB = 0 and (2^c)l = #E. @@ -109,7 +122,8 @@ Module Type EdDSAParams. * EdDSA secret key from an EdDSA public key. *) Parameter l : Prime. - Axiom l_odd : Z.odd l = true. + Axiom l_odd : l > 2. + (* TODO: (2^c)l = #E *) (* * A “prehash” function H'. @@ -120,36 +134,145 @@ Module Type EdDSAParams. * it implicitly took H0 as the identity function. *) Parameter H'_out_len : nat -> nat. - Parameter H' : forall n, word n -> word (H'_out_len n). + 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 Type EdDSA (Import P : EdDSAParams). + Local Infix "++" := combine. + Local Infix "*" := scalarMult. + Local Infix "+" := unifiedAdd. + + (* From [https://eprint.iacr.org/2015/677.pdf]: x is negative if the + * (b − 1)-bit encoding of x is lexicographically larger than the + * (b − 1)-bit encoding of −x *) + Definition sign_bit x : word 1 := + match (wordToNat (encode_scalar x) ?= wordToNat (encode_scalar (GFopp x)))%nat with + | Gt => wone 1 + | _ => wzero 1 + end. + + (* TODO: move eventually *) + Lemma b_gt_0 : b > 0. + Proof. + pose proof b_valid. + pose proof q_odd. + destruct b; boring. + Qed. + Parameter encode_point : point -> word b. - Parameter decode_point : word b -> point. - Parameter secret : Type. - Parameter public : secret -> word b. - Parameter signature : secret -> forall n, word n -> word (b + b). -End EdDSA. + Definition encode_point_ref (P : point) : word b. + replace b with (b - 1 + 1)%nat by abstract (pose proof b_gt_0; omega). + apply (combine (encode_scalar (projY P)) (sign_bit (projX P))). + Defined. + Axiom encode_point_spec : forall P, encode_point P = encode_point_ref P. + Parameter decode_point : word b -> option point. + Axiom decode_point_spec : forall P, onCurve P -> + decode_point (encode_point P) = Some P. + + Definition s (sk : secretkey) := + let N := wordToNat (wfirstn sk n_le_b) in + ((N - (NPeano.modulo N (pow2 c))) * pow2 c)%nat. + Parameter public : secretkey -> publickey. + Axiom public_spec : forall sk, public sk = encode_point ((s sk) * B). -Module EdDSAImpl (Import P : EdDSAParams) <: EdDSA P. - Definition encode_point (p : point) := wzero b. (* TODO *) - Definition decode_point (w : word b) := zero. (* TODO *) + Parameter sign : secretkey -> forall {n}, word n -> signature. + Axiom sign_spec : forall sk {n} (M : word n), sign sk M = + let r := wordToNat (H ((split2 b b (H sk)) ++ M)) in + let R := r * B in + let S := NPeano.modulo (r + ((s sk) * wordToNat (H ((encode_point R) ++ (public sk) ++ M))))%nat (Z.to_nat l) in + (encode_point R) ++ (natToWord b S). - 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; - s : Z; - hash_high : word b; - s_def : s = wordToZ (wand c_to_n_window key); - hash_high_def : hash_high = split2 b b (H b key) - }. + Parameter verify : publickey -> signature -> forall {n}, word n -> bool. + Axiom verify_spec : forall A_ sig {n} (M : word n), verify A_ sig M = true <-> + let R_ := split1 b b sig in + let S_ := split2 b b sig in + let S := wordToNat S_ in + match (decode_point A_) with + | None => False + | Some A => match (decode_point R_) with + | None => False + | Some R => S * B = R + (wordToNat (H (R_ ++ A_ ++ M )) * A) + end + end. - (* Needs scalar multiplication: - * Definition public (sk : secret) := H b (encode_point (scalar_mul (inject (s sk)) B)). *) + (* for signature (R_, S_), R_ = encode_point (r * B) *) + Lemma decode_sign_split1 : forall (sk : secretkey) {n} (M : word n), + split1 b b (sign sk M) = encode_point ((wordToNat (H ((split2 b b (H sk)) ++ M))) * B). + Proof. + intros. pose proof (sign_spec sk M). + simpl in H0. rewrite H0; clear H0. + apply split1_combine. + Qed. + + (* for signature (R_, S_), S_ = encode_scalar (r + H(R_, A_, M)s) *) + Lemma decode_sign_split2 : forall (sk : secretkey) {n} (M : word n), + split2 b b (sign sk M) = + let r := wordToNat (H ((split2 b b (H sk)) ++ M)) in + natToWord b (NPeano.modulo (r + ((s sk) * wordToNat (H ((encode_point (r * B)) ++ (public sk) ++ M)))) (Z.to_nat l)). + Proof. + intros. rewrite sign_spec; simpl. + rewrite split2_combine. + f_equal. + Qed. - Definition signature (sk : secret) n (w : word n) := wzero (b + b). + Lemma verification_principle : forall n, + NPeano.modulo n (Z.to_nat l) * B = n * B. + Admitted. -End EdDSAImpl. + Lemma l_bound : (Z.to_nat l < pow2 b)%nat. + Admitted. + + 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 sk M) M = true. + Proof. + intros; rewrite verify_spec. + intros; subst R_. + rewrite decode_sign_split1. + rewrite public_spec. + rewrite decode_point_spec by auto. + rewrite decode_point_spec by auto. + subst S S_. + rewrite decode_sign_split2; simpl. + remember (wordToNat (H (split2 b b (H sk) ++ M))) as r. + rewrite public_spec. + remember (wordToNat + (H (encode_point (r * B) ++ encode_point (s sk * B) ++ M))). + assert (N.of_nat (NPeano.modulo (r + s sk * n1) (Z.to_nat l)) < Npow2 b)%N. { + remember (r + s sk * n1)%nat. + pose proof (NPeano.Nat.mod_upper_bound n2 (Z.to_nat l) l_gt_zero). + pose proof l_bound. + pose proof (lt_trans _ (Z.to_nat l) (pow2 b) H0 H1). + clear H0 H1. + apply Nomega.Nlt_in. + rewrite Nnat.Nat2N.id, Npow2_nat; auto. + } + rewrite (wordToNat_natToWord_idempotent b + (NPeano.modulo (r + s sk * n1) (Z.to_nat l)) H0); clear H0. + rewrite verification_principle. + Admitted. (* relies on group properties, e.g. distributivity, exp *) + +End EdDSA. |