blob: f8581c4c933260367aa77a9fc19d57ec367f805b (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
|
Require Bedrock.Word Crypto.Util.WordUtil.
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
both [NPeano] and [Nat], and define the notations with unqualified
names. By importing the module, we get access to the notations
without importing [NPeano] and [Nat] in the top-level of this
file. *)
Module Import Notations.
Import NPeano Nat.
Infix "^" := pow.
Infix "mod" := modulo (at level 40, no associativity).
Infix "++" := Word.combine.
Notation setbit := setbit.
End Notations.
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 *)
{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 : 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 : F l -> Word.word b} (* normative encoding of scalars *)
:=
{
EdDSA_group:@Algebra.group E Eeq Eadd Ezero Eopp;
EdDSA_scalarmult:@Algebra.ScalarMult.is_scalarmult E Eeq Eadd Ezero EscalarMult;
EdDSA_c_valid : c = 2 \/ c = 3;
EdDSA_n_ge_c : n >= c;
EdDSA_n_le_b : n <= b;
EdDSA_B_not_identity : not (Eeq 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 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).
Local Arguments H {n} _.
Local Notation wfirstn n w := (@WordUtil.wfirstn n _ w _) (only parsing).
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 *)
let x := x - (x mod (2^c)) in (* it is implicitly 0 mod (2^c) *)
setbit x 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 := Eenc (curveKey sk*B).
Program Definition sign (A_:publickey) sk {n} (M : Word.word n) :=
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 : F l := F.nat_mod l (r + H (Eenc R ++ A_ ++ M) * s) in
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.
|
