From 7ef4da17c2a2530fcce15b1b04249c4ef97aab86 Mon Sep 17 00:00:00 2001 From: Jade Philipoom Date: Tue, 5 Jan 2016 18:24:38 -0500 Subject: PointFormats/EdDSA: scoping tweaks in PointFormats, small changes of phrasing in EdDSA to make proofs more convenient. --- src/Curves/Curve25519.v | 1 + src/Curves/PointFormats.v | 42 ++++++++++++++++-------------------------- src/Galois/EdDSA.v | 21 ++++++++++++--------- 3 files changed, 29 insertions(+), 35 deletions(-) (limited to 'src') diff --git a/src/Curves/Curve25519.v b/src/Curves/Curve25519.v index edcf6a24c..8bb2148db 100644 --- a/src/Curves/Curve25519.v +++ b/src/Curves/Curve25519.v @@ -10,6 +10,7 @@ End Modulus25519. Module Curve25519Params <: TwistedEdwardsParams Modulus25519 <: Minus1Params Modulus25519. Module Import GFDefs := GaloisDefs Modulus25519. + Local Open Scope GF_scope. Coercion inject : Z >-> GF. Definition a : GF := -1. diff --git a/src/Curves/PointFormats.v b/src/Curves/PointFormats.v index 2cf5d3665..1e8df9337 100644 --- a/src/Curves/PointFormats.v +++ b/src/Curves/PointFormats.v @@ -5,11 +5,11 @@ Require Import BinNums NArith. Module GaloisDefs (M : Modulus). Module Export GT := GaloisTheory M. - Open Scope GF_scope. End GaloisDefs. Module Type TwistedEdwardsParams (M : Modulus). Module Export GFDefs := GaloisDefs M. + Local Open Scope GF_scope. Parameter a : GF. Axiom a_nonzero : a <> 0. Axiom a_square : exists x, x * x = a. @@ -54,7 +54,7 @@ Proof. case_eq (b - S i); intros; simpl; auto. Qed. -Lemma iter_op_xI : forall {A} p i op z b (a : A), (i < S b) -> +Lemma iter_op_step_xI : forall {A} p i op z b (a : A), (i < S b) -> iter_op op z (S b) p~1 i a = iter_op op z b p i a. Proof. induction i; intros; [pose proof (Gt.gt_irrefl 0); intuition | ]. @@ -64,7 +64,7 @@ Proof. rewrite IHi by omega; auto. Qed. -Lemma iter_op_xO : forall {A} p i op z b (a : A), (i < S b) -> +Lemma iter_op_step_xO : forall {A} p i op z b (a : A), (i < S b) -> iter_op op z (S b) p~0 i a = iter_op op z b p i a. Proof. induction i; intros; [pose proof (Gt.gt_irrefl 0); intuition | ]. @@ -74,7 +74,7 @@ Proof. rewrite IHi by omega; auto. Qed. -Lemma iter_op_1 : forall {A} i op z b (a : A), (i < S b) -> +Lemma iter_op_step_1 : forall {A} i op z b (a : A), (i < S b) -> iter_op op z (S b) 1%positive i a = z. Proof. induction i; intros; [pose proof (Gt.gt_irrefl 0); intuition | ]. @@ -90,36 +90,23 @@ Proof. Qed. Hint Resolve pos_size_gt0. -Lemma test_low_bit_xI : forall p b, testbit_rev p~1 b b = true. -Proof. - unfold testbit_rev; intros; rewrite Minus.minus_diag; auto. -Qed. - -Lemma test_low_bit_xO : forall p b, testbit_rev p~0 b b = false. -Proof. - unfold testbit_rev; intros; rewrite Minus.minus_diag; auto. -Qed. - -Lemma test_low_bit_1 : forall b, testbit_rev 1%positive b b = true. -Proof. - unfold testbit_rev; intros; rewrite Minus.minus_diag; auto. -Qed. - -Ltac low_bit := match goal with -| [ |- context[testbit_rev ?p~1 ?b ?b] ] => rewrite test_low_bit_xI; f_equal; rewrite iter_op_xI -| [ |- context[testbit_rev ?p~0 ?b ?b] ] => rewrite test_low_bit_xO; rewrite iter_op_xO -| [ |- context[testbit_rev 1%positive ?b ?b] ] => rewrite test_low_bit_1; rewrite iter_op_1 +Ltac iter_op_step := match goal with +| [ |- context[iter_op ?op ?z ?b ?p~1 ?i ?a] ] => rewrite iter_op_step_xI +| [ |- context[iter_op ?op ?z ?b ?p~0 ?i ?a] ] => rewrite iter_op_step_xO +| [ |- context[iter_op ?op ?z ?b 1%positive ?i ?a] ] => rewrite iter_op_step_1 end; auto. Lemma iter_op_spec : forall b p {A} op z (a : A) (zero_id : forall x : A, op x z = x), (Pos.size_nat p <= b) -> iter_op op z b p b a = Pos.iter_op op p a. Proof. induction b; intros; [pose proof (pos_size_gt0 p); omega |]. - case_eq p; intros; simpl; low_bit; apply IHb; - rewrite H0 in *; simpl in H; apply Le.le_S_n in H; auto. + simpl; unfold testbit_rev; rewrite Minus.minus_diag. + case_eq p; intros; simpl; iter_op_step; simpl; + rewrite IHb; rewrite H0 in *; simpl in H; apply Le.le_S_n in H; auto. Qed. Module CompleteTwistedEdwardsCurve (M : Modulus) (Import P : TwistedEdwardsParams M). + Local Open Scope GF_scope. (** Twisted Ewdwards curves with complete addition laws. References: * * @@ -173,6 +160,7 @@ End CompleteTwistedEdwardsCurve. Module Type CompleteTwistedEdwardsPointFormat (M : Modulus) (Import P : TwistedEdwardsParams M). + Local Open Scope GF_scope. Module Curve := CompleteTwistedEdwardsCurve M P. Parameter point : Type. Parameter encode : (GF*GF) -> point. @@ -189,6 +177,7 @@ Module Type CompleteTwistedEdwardsPointFormat (M : Modulus) (Import P : TwistedE End CompleteTwistedEdwardsPointFormat. Module CompleteTwistedEdwardsFacts (M : Modulus) (Import P : TwistedEdwardsParams M). + Local Open Scope GF_scope. Module Import Curve := CompleteTwistedEdwardsCurve M P. Lemma twistedAddCompletePlus : forall (P1 P2:point), let '(x1, y1) := proj1_sig P1 in @@ -365,7 +354,7 @@ End CompleteTwistedEdwardsFacts. Module Type Minus1Params (Import M : Modulus) <: TwistedEdwardsParams M. Module Export GFDefs := GaloisDefs M. - Open Scope GF_scope. + Local Open Scope GF_scope. Definition a := inject (- 1). Axiom a_nonzero : a <> 0. Axiom a_square : exists x, x * x = a. @@ -374,6 +363,7 @@ Module Type Minus1Params (Import M : Modulus) <: TwistedEdwardsParams M. End Minus1Params. Module Minus1Format (M : Modulus) (Import P : Minus1Params M) <: CompleteTwistedEdwardsPointFormat M P. + Local Open Scope GF_scope. Module Import Facts := CompleteTwistedEdwardsFacts M P. Module Import Curve := Facts.Curve. (** [projective] represents a point on an elliptic curve using projective diff --git a/src/Galois/EdDSA.v b/src/Galois/EdDSA.v index a2df23076..af4f892ca 100644 --- a/src/Galois/EdDSA.v +++ b/src/Galois/EdDSA.v @@ -5,8 +5,7 @@ Require Import Crypto.Galois.BaseSystem Crypto.Galois.GaloisTheory. Require Import Util.ListUtil Util.CaseUtil Util.ZUtil. Require Import VerdiTactics. -Open Scope nat_scope. - +Local Open Scope nat_scope. Local Coercion Z.to_nat : Z >-> nat. (* TODO : where should this be? *) @@ -27,6 +26,7 @@ Notation "'encoding' 'of' T 'as' B" := (Encoding T B) (at level 50). Module Type EdDSAParams. Parameter q : Prime. Axiom q_odd : q > 2. + (* Choosing q sufficiently large is important for security, since the size of * q constrains the size of l below. *) @@ -34,10 +34,9 @@ Module Type EdDSAParams. Module Modulus_q <: Modulus. Definition modulus := q. End Modulus_q. - Module Export GFDefs := GaloisDefs Modulus_q. Parameter b : nat. - Axiom b_valid : 2^(b - 1) > q. + Axiom b_valid : (2^(Z.of_nat b - 1) > q)%Z. Notation secretkey := (word b) (only parsing). Notation publickey := (word b) (only parsing). Notation signature := (word (b + b)) (only parsing). @@ -54,6 +53,10 @@ Module Type EdDSAParams. Parameter n : nat. Axiom n_ge_c : n >= c. Axiom n_le_b : n <= b. + + Module Import GFDefs := GaloisDefs Modulus_q. + Local Open Scope GF_scope. + (* Secret EdDSA scalars have exactly n + 1 bits, with the top bit * (the 2n position) always set and the bottom c bits always cleared. * The original specification of EdDSA did not include this parameter: @@ -64,7 +67,7 @@ Module Type EdDSAParams. Parameter a : GF. Axiom a_nonzero : a <> 0%GF. - Axiom a_square : exists x, x^2 = a. + Axiom a_square : exists x, x * x = 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: @@ -100,7 +103,7 @@ Module Type EdDSAParams. * EdDSA secret key from an EdDSA public key. *) Parameter l : Prime. - Axiom l_odd : l > 2. + Axiom l_odd : (l > 2)%nat. Axiom l_order_B : scalarMult l B = zero. (* TODO: (2^c)l = #E *) @@ -116,7 +119,7 @@ Module Type EdDSAParams. Parameter H' : forall {n}, word n -> word (H'_out_len n). Parameter FqEncoding : encoding of GF as word (b-1). - Parameter FlEncoding : encoding of {s:nat | s = s mod l} as word b. + Parameter FlEncoding : encoding of {s:nat | s mod l = s} as word b. Parameter PointEncoding : encoding of point as word b. End EdDSAParams. @@ -130,7 +133,7 @@ Ltac arith := arith'; | [ H : _ |- _ ] => rewrite H; arith' end. -Definition modularNat (l : nat) (l_odd : l > 2) (n : nat) : {s : nat | s = s mod l}. +Definition modularNat (l : nat) (l_odd : l > 2) (n : nat) : {s : nat | s mod l = s}. exists (n mod l); abstract arith. Defined. @@ -163,7 +166,7 @@ Module Type EdDSA (Import P : EdDSAParams). let S_ := split2 b b sig in exists A, dec A_ = Some A /\ exists R, dec R_ = Some R /\ - exists S : {s:nat | s = s mod l}, dec S_ = Some S /\ + exists S : {s:nat | s mod l = s}, dec S_ = Some S /\ proj1_sig S * B = R + wordToNat (H (R_ ++ A_ ++ M)) * A). End EdDSA. -- cgit v1.2.3