diff options
author | Andres Erbsen <andreser@mit.edu> | 2016-02-13 22:09:21 -0500 |
---|---|---|
committer | Robert Sloan <varomodt@gmail.com> | 2016-06-22 13:39:04 -0400 |
commit | 75926e67a551d99153bccf8fe82c8eabc0b9ebcd (patch) | |
tree | fda18a059a2e774b74146496104092114e2a6030 /src/Spec | |
parent | bca928f049b75c13fd3c376c287c568020935534 (diff) |
Spec/EdDSA: cleanup; refactor lemmas to src/EdDSAProofs.v
Diffstat (limited to 'src/Spec')
-rw-r--r-- | src/Spec/EdDSA.v | 334 |
1 files changed, 85 insertions, 249 deletions
diff --git a/src/Spec/EdDSA.v b/src/Spec/EdDSA.v index bc81dce01..c7314486e 100644 --- a/src/Spec/EdDSA.v +++ b/src/Spec/EdDSA.v @@ -1,19 +1,17 @@ -Require Import ZArith NPeano Znumtheory. -Require Import Bedrock.Word. -Require Import Crypto.Spec.CompleteEdwardsCurve Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems. -Require Import Crypto.ModularArithmetic.PrimeFieldTheorems Crypto.ModularArithmetic.ModularArithmeticTheorems. -Require Import Util.ListUtil Util.CaseUtil Util.ZUtil. -Require Import VerdiTactics. +Require Import Crypto.Spec.ModularArithmetic. +Require Import Crypto.Spec.CompleteEdwardsCurve. -Local Open Scope nat_scope. -Local Coercion Z.to_nat : Z >-> nat. +Require Bedrock.Word. +Require Znumtheory BinInt. +Require NPeano. (* TODO : where should this be? *) -Definition wfirstn {m} {n} (w : word m) (H : n <= m) : word n. - refine (split1 n (m - n) (match _ in _ = N return word N with +Definition wfirstn n {m} (w : Word.word m) {H : n <= m} : Word.word n. + refine (Word.split1 n (m - n) (match _ in _ = N return Word.word N with | eq_refl => w - end)); abstract omega. -Defined. + end)); abstract omega. Defined. + +Coercion Word.wordToNat : Word.word >-> nat. Class Encoding (T B:Type) := { enc : T -> B ; @@ -22,243 +20,81 @@ Class Encoding (T B:Type) := { }. Notation "'encoding' 'of' T 'as' B" := (Encoding T B) (at level 50). -(* Spec from <https://eprint.iacr.org/2015/677.pdf> *) -Module Type EdDSAParams. - Parameter q : Z. - Axiom q_prime : prime q. - Axiom q_odd : (2 < q)%Z. - - (* Choosing q sufficiently large is important for security, since the size of - * q constrains the size of l below. *) - - (* GF is the finite field of integers modulo q *) - Module Modulus_q <: PrimeModulus. - Definition modulus := q. - Definition prime_modulus := q_prime. - End Modulus_q. - - Parameter b : nat. - 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). - - Parameter H : forall {n}, word n -> word (b + b). - (* A cryptographic hash function. Conservative hash functions are recommended - * and do not have much impact on the total cost of EdDSA. *) - - Parameter c : nat. - Axiom c_valid : c = 2 \/ c = 3. - (* Secret EdDSA scalars are multiples of 2^c. The original specification of - * EdDSA did not include this parameter: it implicitly took c = 3. *) - - Parameter n : nat. - Axiom n_ge_c : n >= c. - Axiom n_le_b : n <= b. - - Module Import Field := FieldModulo Modulus_q. - Definition Fq := F q. - Local Open Scope F_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: - * it implicitly took n = b−2. - * Choosing n sufficiently large is important for security: - * standard “kangaroo” attacks use approximately 1.36\sqrt(2n−c) additions - * on average to determine an EdDSA secret key from an EdDSA public key *) - - Parameter a : Fq. - Axiom a_nonzero : a <> 0%F. - Axiom a_square : exists sqrt_a, sqrt_a^2 = 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: - * it implicitly took a = −1 (and required q mod 4 = 1). *) - - Parameter d : Fq. - Axiom d_nonsquare : forall x, x^2 <> d. - (* The exact choice of d (together with a and q) is important for security, - * and is the main topic considered in “curve selection”. *) - - (* E = {(x, y) \in Fq x Fq : ax^2 + y^2 = 1 + dx^2y^2}. - * This set forms a group with neutral element 0 = (0, 1) under the - * twisted Edwards addition law. *) - Definition CurveParameters : TwistedEdwardsParams := - Build_TwistedEdwardsParams q a d q_prime q_odd a_nonzero a_square d_nonsquare. - - Definition pt := @point CurveParameters. - Parameter B : pt. (* element of E *) - Axiom B_not_identity : B <> zero. - - (* - * An odd prime l such that lB = 0 and (2^c)l = #E. - * The number #E is part of the standard data provided for an elliptic - * curve E. - * Choosing l sufficiently large is important for security: standard “rho” - * attacks use approximately 0.886√l additions on average to determine an - * EdDSA secret key from an EdDSA public key. - *) - Parameter l : Z. - Axiom l_prime : prime l. - Axiom l_odd : (l > 2)%nat. - Axiom l_order_B : scalarMult l B = zero. - (* TODO: (2^c)l = #E *) - - (* - * A “prehash” function H'. - * PureEdDSA means EdDSA where H' is the identity function, i.e. H'(M) = M. - * HashEdDSA means EdDSA where H' generates a short output, no matter how - * long the message is; for example, H'(M) = SHA-512(M). - * The original specification of EdDSA did not include this parameter: - * 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 FqEncoding : encoding of Fq as word (b-1). - Parameter FlEncoding : encoding of {s:nat | s mod l = s} as word b. - Parameter PointEncoding : encoding of pt as word b. +Infix "^" := NPeano.pow. +Infix "mod" := NPeano.modulo. +Infix "++" := Word.combine. + +Section EdDSAParams. + Class EdDSAParams := { (* <https://eprint.iacr.org/2015/677.pdf> *) + E : TwistedEdwardsParams; (* underlying elliptic curve *) + + b : nat; + b_valid : 2^(b - 1) > BinInt.Z.to_nat q; + FqEncoding : encoding of F q as Word.word (b-1); + PointEncoding : encoding of point as Word.word b; + + H : forall {n}, Word.word n -> Word.word (b + b); (* main hash function *) + + c : nat; (* cofactor E = 2^c *) + c_valid : c = 2 \/ c = 3; + n : nat; + n_ge_c : n >= c; + n_le_b : n <= b; + + B : point; + B_not_identity : B <> zero; + + l : nat; (* order of the subgroup of E generated by B *) + l_prime : Znumtheory.prime (BinInt.Z.of_nat l); + l_odd : l > 2; + l_order_B : scalarMult l B = zero; + FlEncoding : encoding of F (BinInt.Z.of_nat l) as Word.word b; + + H'_out_len : nat -> nat; + H' : forall {n}, Word.word n -> Word.word (H'_out_len n) (* prehash function *) + }. End EdDSAParams. -Hint Rewrite Nat.mod_mod using omega. - -Ltac arith' := intros; autorewrite with core; try (omega || congruence). - -Ltac arith := arith'; - repeat match goal with - | [ H : _ |- _ ] => rewrite H; arith' - end. - -Definition modularNat (l : nat) (l_odd : l > 2) (n : nat) : {s : nat | s mod l = s}. - exists (n mod l); abstract arith. -Defined. - -Module Type EdDSA (Import P : EdDSAParams). - Infix "++" := combine. - Infix "*" := scalarMult. - Infix "+" := unifiedAdd. - Coercion wordToNat : word >-> nat. - - Definition curveKey sk := let N := wfirstn sk n_le_b in - (N - (N mod pow2 c) + pow2 n)%nat. - Definition randKey (sk:secretkey) := split2 b b (H sk). - Definition modL := modularNat l l_odd. - - 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 := H (randKey sk ++ M) in - let R := r * B in - let s := curveKey sk in - let S := (r + H (enc R ++ public sk ++ M) * s)%nat in - enc R ++ enc (modL S). - - 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 - exists A, dec A_ = Some A /\ - exists R, dec R_ = Some R /\ - 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. - -Module EdDSAFacts (Import P : EdDSAParams) (Import Impl : EdDSA P). - Hint Rewrite sign_spec split1_combine split2_combine. - - (* for signature (R_, S_), R_ = encode_point (r * B) *) - Lemma decode_sign_split1 : forall A_ sk {n} (M : word n), - split1 b b (sign A_ sk M) = enc (wordToNat (H (randKey sk ++ M)) * B). - Proof. - arith. - Qed. - Hint Rewrite decode_sign_split1. - - (* for signature (R_, S_), S_ = encode_scalar (r + H(R_, A_, M)s) *) - Lemma decode_sign_split2 : forall sk {n} (M : word n), - split2 b b (sign (public sk) sk M) = - let r := H (randKey sk ++ M) in - let R := r * B in - let s := curveKey sk in - let S := (r + (H ((enc R) ++ (public sk) ++ M) * s))%nat in - enc (modL S). - Proof. - arith. - Qed. - Hint Rewrite decode_sign_split2. - - Existing Instance CurveParameters. - Lemma zero_times : forall n, 0 * n = zero. - Proof. - auto. - Qed. - - Lemma zero_plus : forall n, zero + n = n. - Proof. - intros; rewrite twistedAddComm; apply zeroIsIdentity. - Qed. - - Lemma times_S : forall n m, S n * m = m + n * m. - Proof. - auto. - Qed. - - Lemma times_S_nat : forall n m, (S n * m = m + n * m)%nat. - Proof. - auto. - Qed. - - Hint Rewrite plus_O_n plus_Sn_m times_S times_S_nat. - Hint Rewrite zeroIsIdentity zero_times zero_plus twistedAddAssoc. - - Lemma scalarMult_distr : forall n0 m, (n0 + m) * B = unifiedAdd (n0 * B) (m * B). - Proof. - induction n0; arith. - Qed. - Hint Rewrite scalarMult_distr. - - Lemma scalarMult_assoc : forall (n0 m : nat), n0 * (m * B) = (n0 * m) * B. - Proof. - induction n0; arith. - Qed. - Hint Rewrite scalarMult_assoc. - - Lemma scalarMult_zero : forall m, m * zero = zero. - Proof. - induction m; arith. - Qed. - Hint Rewrite scalarMult_zero. - Hint Rewrite l_order_B. - - Lemma l_order_B' : forall x, l * x * B = zero. - Proof. - intros; rewrite mult_comm; rewrite <- scalarMult_assoc; arith. - Qed. - - Hint Rewrite l_order_B'. - - Lemma scalarMult_mod_l : forall n0, n0 mod l * B = n0 * B. - Proof. - intros. - rewrite (div_mod n0 l) at 2 by (generalize l_odd; omega). - arith. - Qed. - Hint Rewrite scalarMult_mod_l. - - Hint Rewrite verify_spec public_spec. - - Hint Resolve @encoding_valid. - - Lemma verify_valid_passes : forall sk {n} (M : word n), - verify (public sk) M (sign (public sk) sk M) = true. - Proof. - arith; simpl. - repeat eexists; eauto; simpl; arith. - Qed. - -End EdDSAFacts. +Section EdDSA. + Context {prm:EdDSAParams}. + Existing Instance E. + Existing Instance PointEncoding. + Existing Instance FlEncoding. + Existing Class le. + Existing Instance n_le_b. + + Notation secretkey := (Word.word b) (only parsing). + Notation publickey := (Word.word b) (only parsing). + Notation signature := (Word.word (b + b)) (only parsing). + + (* TODO: proofread curveKey and definition of n *) + Definition curveKey (sk:secretkey) : nat := + let x := wfirstn n sk in (* first half of the secret key is a scalar *) + let x := x - (x mod (2^c)) in (* it is implicitly 0 mod (2^c) *) + x + 2^n. (* and the high bit is always set *) + Definition prngKey (sk:secretkey) : Word.word b := Word.split2 b b (H sk). + Definition public (sk:secretkey) : publickey := enc (curveKey sk * B)%E. + + Definition sign (A_:publickey) sk {n} (M : Word.word n) := + let r : nat := H (prngKey sk ++ M) in (* secret nonce *) + let R : point := (r * B)%E in (* commitment to nonce *) + let s : nat := curveKey sk in (* secret scalar *) + let S : F (BinInt.Z.of_nat l) := ZToField (BinInt.Z.of_nat + (r + H (enc R ++ public sk ++ M) * s)) in + enc R ++ enc S. + + Axiom point_eq_dec : forall P Q : point, {P = Q} + {P <> Q}. + Infix "==" := point_eq_dec (no associativity, at level 70) : E_scope. + Definition verify (A_:publickey) {n:nat} (M : Word.word n) (sig:signature) : bool := + let R_ := Word.split1 b b sig in + let S_ := Word.split2 b b sig in + match dec A_ : option point with None => false | Some A => + match dec R_ : option point with None => false | Some R => + match dec S_ : option (F (BinInt.Z.of_nat l)) with None => false | Some S' => + if BinInt.Z.to_nat (FieldToZ S') * B == R + (H (R_ ++ A_ ++ M)) * A + then true else false + end + end + end%E. +End EdDSA.
\ No newline at end of file |