From 1ea69cd53ff8472bb23c338d0e3fcac0a1f9ada5 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Fri, 16 Sep 2016 13:31:40 -0400 Subject: Derive EdDSA.verify from equational specification Experiments/SpecEd25519 will come back soon --- src/Spec/EdDSA.v | 31 ++++++++++++++++--------------- 1 file changed, 16 insertions(+), 15 deletions(-) (limited to 'src/Spec') diff --git a/src/Spec/EdDSA.v b/src/Spec/EdDSA.v index 38dc64cef..2971bfef8 100644 --- a/src/Spec/EdDSA.v +++ b/src/Spec/EdDSA.v @@ -3,6 +3,10 @@ Require Coq.ZArith.Znumtheory Coq.ZArith.BinInt. Require Coq.Numbers.Natural.Peano.NPeano. Require Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems. +Require Import Omega. (* TODO: remove this import when we drop 8.4 *) + +Require Import Crypto.Spec.ModularArithmetic. + (** In Coq 8.4, we have [NPeano.pow] and [NPeano.modulo]. In Coq 8.5, they are [Nat.pow] and [Nat.modulo]. To allow this file to work with both versions, we create a module where we (locally) import @@ -28,12 +32,12 @@ Section EdDSA. {H : forall {n}, Word.word n -> Word.word (b + b)} (* main hash function *) {c : nat} (* cofactor E = 2^c *) {n : nat} (* secret keys are (n+1) bits *) - {l : nat} (* order of the subgroup of E generated by B *) + {l : BinInt.Z} (* order of the subgroup of E generated by B *) {B : E} (* base point *) {Eenc : E -> Word.word b} (* normative encoding of elliptic cuve points *) - {Senc : nat -> Word.word b} (* normative encoding of scalars *) + {Senc : F l -> Word.word b} (* normative encoding of scalars *) := { EdDSA_group:@Algebra.group E Eeq Eadd Ezero Eopp; @@ -44,19 +48,19 @@ Section EdDSA. EdDSA_n_ge_c : n >= c; EdDSA_n_le_b : n <= b; - EdDSA_B_not_identity : B <> Ezero; + EdDSA_B_not_identity : not (Eeq B Ezero); - EdDSA_l_prime : Znumtheory.prime (BinInt.Z.of_nat l); - EdDSA_l_odd : l > 2; - EdDSA_l_order_B : Eeq (EscalarMult l B) Ezero + EdDSA_l_prime : Znumtheory.prime l; + EdDSA_l_odd : BinInt.Z.lt 2 l; + EdDSA_l_order_B : Eeq (EscalarMult (BinInt.Z.to_nat l) B) Ezero }. Global Existing Instance EdDSA_group. Global Existing Instance EdDSA_scalarmult. Context `{prm:EdDSA}. - Local Infix "=" := Eeq : type_scope. Local Coercion Word.wordToNat : Word.word >-> nat. + Local Coercion BinInt.Z.to_nat : BinInt.Z >-> nat. Local Notation secretkey := (Word.word b) (only parsing). Local Notation publickey := (Word.word b) (only parsing). Local Notation signature := (Word.word (b + b)) (only parsing). @@ -64,8 +68,7 @@ Section EdDSA. Local Arguments H {n} _. Local Notation wfirstn n w := (@WordUtil.wfirstn n _ w _) (only parsing). - Require Import Coq.omega.Omega. - Obligation Tactic := simpl; intros; try apply NPeano.Nat.mod_upper_bound; destruct prm; omega. + Local Obligation Tactic := destruct prm; simpl; intros; omega. Program Definition curveKey (sk:secretkey) : nat := let x := wfirstn n (H sk) in (* hash the key, use first "half" for secret scalar *) @@ -82,12 +85,10 @@ Section EdDSA. let r : nat := H (prngKey sk ++ M) in (* secret nonce *) let R : E := r * B in (* commitment to nonce *) let s : nat := curveKey sk in (* secret scalar *) - let S : nat := (r + H (Eenc R ++ A_ ++ M) * s) mod l in + let S : F l := F.nat_mod l (r + H (Eenc R ++ A_ ++ M) * s) in Eenc R ++ Senc S. - (* For a [n]-bit [message] from public key [A_], validity of a signature [R_ ++ S_] *) - Inductive valid {n:nat} : Word.word n -> publickey -> signature -> Prop := - ValidityRule : forall (message:Word.word n) (A:E) (R:E) (S:nat), - S * B = R + (H (Eenc R ++ Eenc A ++ message) mod l) * A - -> valid message (Eenc A) (Eenc R ++ Senc S). + Definition valid {n} (message : Word.word n) pubkey signature := + exists A S R, Eenc A = pubkey /\ Eenc R ++ Senc S = signature /\ + Eeq (F.to_nat S * B) (R + (H (Eenc R ++ Eenc A ++ message) mod l) * A). End EdDSA. -- cgit v1.2.3