From 2d7d0872895639be94f6b274bbe2ef05044bd6db Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Mon, 20 Jun 2016 02:01:29 -0400 Subject: port EdDSA spec --- src/Spec/EdDSA.v | 107 ++++++++++++++++++++++++++----------------------------- 1 file changed, 51 insertions(+), 56 deletions(-) (limited to 'src') diff --git a/src/Spec/EdDSA.v b/src/Spec/EdDSA.v index a0e5e9da7..bd8a095dd 100644 --- a/src/Spec/EdDSA.v +++ b/src/Spec/EdDSA.v @@ -1,6 +1,4 @@ Require Import Crypto.Spec.Encoding. -Require Import Crypto.Spec.ModularArithmetic. -Require Import Crypto.Spec.CompleteEdwardsCurve. Require Import Crypto.Util.WordUtil. Require Bedrock.Word. @@ -8,80 +6,77 @@ Require Coq.ZArith.Znumtheory Coq.ZArith.BinInt. Require Coq.Numbers.Natural.Peano.NPeano. Require Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems. -Coercion Word.wordToNat : Word.word >-> nat. +Local Infix "^" := NPeano.pow. +Local Infix "mod" := NPeano.modulo (at level 40, no associativity). +Local Infix "++" := Word.combine. -Infix "^" := NPeano.pow. -Infix "mod" := NPeano.modulo. -Infix "++" := Word.combine. +Generalizable All Variables. +Section EdDSA. + Class EdDSA (* *) + {E Eeq Eadd Ezero Eopp} {EscalarMult} (* the underllying elliptic curve operations *) -Section EdDSAParams. + {b : nat} (* public keys are k bits, signatures are 2*k bits *) + {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 *) - Class EdDSAParams := { (* *) - E : TwistedEdwardsParams; (* underlying elliptic curve *) + {B : E} (* base point *) - b : nat; (* public keys are k bits, signatures are 2*k bits *) - b_valid : 2^(b - 1) > BinInt.Z.to_nat q; - FqEncoding : canonical encoding of F q as Word.word (b-1); - PointEncoding : canonical encoding of E.point as Word.word b; + {PointEncoding : canonical encoding of E as Word.word b} (* wire format *) + {FlEncoding : canonical encoding of { n | n < l } as Word.word b} + := + { + EdDSA_group:@Algebra.group E Eeq Eadd Ezero Eopp; - H : forall {n}, Word.word n -> Word.word (b + b); (* main hash function *) + EdDSA_c_valid : c = 2 \/ c = 3; - c : nat; (* cofactor E = 2^c *) - c_valid : c = 2 \/ c = 3; + EdDSA_n_ge_c : n >= c; + EdDSA_n_le_b : n <= b; - n : nat; (* secret keys are (n+1) bits *) - n_ge_c : n >= c; - n_le_b : n <= b; + EdDSA_B_not_identity : B <> Ezero; - B : E.point; - B_not_identity : B <> E.zero; + EdDSA_l_prime : Znumtheory.prime (BinInt.Z.of_nat l); + EdDSA_l_odd : l > 2; + EdDSA_l_order_B : EscalarMult l B = Ezero + }. + Global Existing Instance EdDSA_group. - 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 : (l*B)%E = E.zero; - FlEncoding : canonical encoding of F (BinInt.Z.of_nat l) as Word.word b - }. -End EdDSAParams. + Context `{prm:EdDSA}. + + Local Infix "=" := Eeq. + Local Coercion Word.wordToNat : Word.word >-> 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). -Section EdDSA. - Context {prm:EdDSAParams}. - Global Existing Instance E. - Global Existing Instance PointEncoding. - Global 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). - Local Infix "==" := CompleteEdwardsCurveTheorems.E.point_eq_dec (at level 70) : E_scope . + + Existing Class le. Local Existing Instance EdDSA_n_le_b. + Local Arguments H {n} _. (* 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 *) + + Local Infix "+" := Eadd. + Local Infix "*" := EscalarMult. + Definition prngKey (sk:secretkey) : Word.word b := Word.split2 b b (H sk). - Definition public (sk:secretkey) : publickey := enc (curveKey sk * B)%E. + Definition public (sk:secretkey) : publickey := enc (curveKey sk*B). - Definition sign (A_:publickey) sk {n} (M : Word.word n) := + Program Definition sign (A_:publickey) sk {n} (M : Word.word n) := let r : nat := H (prngKey sk ++ M) in (* secret nonce *) - let R : E.point := (r * B)%E in (* commitment to nonce *) + let R : E := r * B 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 + let S : {n|n false | Some S' => - match dec A_ : option E.point with None => false | Some A => - match dec R_ : option E.point with None => false | Some R => - if BinInt.Z.to_nat (FieldToZ S') * B == R + (H (R_ ++ A_ ++ M)) * A - then true else false - end - end - end%E. + (* 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_lt_l, + S * B = R + (H (enc R ++ enc A ++ message) mod l) * A + -> valid message (enc A) (enc R ++ enc (exist _ S S_lt_l)). End EdDSA. \ No newline at end of file -- cgit v1.2.3