blob: 25109bc4cdf51f4ed48747adf77420daf8672e87 (
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
|
Require Bedrock.Word Crypto.Util.WordUtil.
Require Coq.ZArith.Znumtheory Coq.ZArith.BinInt.
Require Coq.Numbers.Natural.Peano.NPeano.
Require Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems.
(** 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.
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 : nat} (* 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 *)
:=
{
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 : 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
}.
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 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).
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 := 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 : nat := (r + H (Eenc R ++ A_ ++ M) * s) mod l 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).
End EdDSA.
|
