diff options
Diffstat (limited to 'src/Spec/EdDSA.v')
-rw-r--r-- | src/Spec/EdDSA.v | 121 |
1 files changed, 57 insertions, 64 deletions
diff --git a/src/Spec/EdDSA.v b/src/Spec/EdDSA.v index 99f0766e0..d71f2ad44 100644 --- a/src/Spec/EdDSA.v +++ b/src/Spec/EdDSA.v @@ -1,87 +1,80 @@ Require Import Crypto.Spec.Encoding. -Require Import Crypto.Spec.ModularArithmetic. -Require Import Crypto.Spec.CompleteEdwardsCurve. - -Require Import Crypto.Util.WordUtil. -Require Bedrock.Word. +Require Bedrock.Word Crypto.Util.WordUtil. 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. + +Generalizable All Variables. +Section EdDSA. + Class EdDSA (* <https://eprint.iacr.org/2015/677.pdf> *) + {E Eeq Eadd Ezero Eopp} {EscalarMult} (* the underllying elliptic curve operations *) -Infix "^" := NPeano.pow. -Infix "mod" := NPeano.modulo. -Infix "++" := Word.combine. + {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 *) -Section EdDSAParams. + {B : E} (* base point *) - Class EdDSAParams := { (* <https://eprint.iacr.org/2015/677.pdf> *) - E : TwistedEdwardsParams; (* underlying elliptic curve *) + {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; - 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; + EdDSA_c_valid : c = 2 \/ c = 3; - H : forall {n}, Word.word n -> Word.word (b + b); (* main hash function *) + EdDSA_n_ge_c : n >= c; + EdDSA_n_le_b : n <= b; - c : nat; (* cofactor E = 2^c *) - c_valid : c = 2 \/ c = 3; + EdDSA_B_not_identity : B <> Ezero; - n : nat; (* secret keys are (n+1) bits *) - n_ge_c : n >= c; - n_le_b : n <= b; + 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. - B : E.point; - B_not_identity : B <> E.zero; + Context `{prm:EdDSA}. - 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. + 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}. - 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). - Local Infix "==" := CompleteEdwardsCurveTheorems.E.point_eq_dec (at level 70) : E_scope . - - (* 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 *) + Local Arguments H {n} _. + Local Notation wfirstn n w := (@WordUtil.wfirstn n _ w _) (only parsing). + + Require Import Omega. + Obligation Tactic := simpl; intros; try apply NPeano.Nat.mod_upper_bound; destruct prm; omega. + + Program Definition curveKey (sk:secretkey) : nat := + let x := wfirstn n (H sk) in (* hash the key, use first "half" for secret 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<l} := exist _ ((r + H (enc R ++ public sk ++ M) * s) mod l) _ in enc R ++ enc S. - 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 S_ : option (F (BinInt.Z.of_nat l)) with None => 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. -End EdDSA.
\ No newline at end of file + (* 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. |