blob: 51b1b0831011d94d53c066fec547174b93c495f5 (
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
|
Require Import Crypto.Spec.ModularArithmetic.
Require Import Crypto.Spec.CompleteEdwardsCurve.
Require Import Crypto.Spec.EdDSA.
Require ModularArithmetic.PrimeFieldTheorems. (* to know that Z mod p is a field *)
(* TODO: move this to a separate file *)
Require Crypto.Util.Decidable.
Require Crypto.Util.Tactics.
Module Pre.
Local Open Scope F_scope.
Lemma curve25519_params_ok {prime_q:Znumtheory.prime (2^255-19)} :
@E.twisted_edwards_params (F (2 ^ 255 - 19)) (@eq (F (2 ^ 255 - 19))) (@F.zero (2 ^ 255 - 19))
(@F.one (2 ^ 255 - 19)) (@F.add (2 ^ 255 - 19)) (@F.mul (2 ^ 255 - 19))
(@F.opp (2 ^ 255 - 19) 1)
(@F.opp (2 ^ 255 - 19) (F.of_Z (2 ^ 255 - 19) 121665) / F.of_Z (2 ^ 255 - 19) 121666).
Proof.
pose (@PrimeFieldTheorems.F.Decidable_square (2^255-19) _);
Tactics.specialize_by Decidable.vm_decide; split; Decidable.vm_decide_no_check.
Qed.
End Pre.
(* these 2 proofs can be generated using https://github.com/andres-erbsen/safecurves-primes *)
Axiom prime_q : Znumtheory.prime (2^255-19). Global Existing Instance prime_q.
Axiom prime_l : Znumtheory.prime (2^252 + 27742317777372353535851937790883648493). Global Existing Instance prime_l.
Section Ed25519.
Local Open Scope Z_scope.
Definition q : BinNums.Z := 2^255 - 19.
Definition Fq : Type := F q.
Definition l : BinNums.Z := 2^252 + 27742317777372353535851937790883648493.
Definition Fl : Type := F l.
Local Open Scope F_scope.
Definition a : Fq := F.opp 1.
Definition d : Fq := F.opp (F.of_Z _ 121665) / (F.of_Z _ 121666).
Local Open Scope nat_scope.
Definition b : nat := 256.
Definition n : nat := b - 2.
Definition c : nat := 3.
Context {H: forall n : nat, Word.word n -> Word.word (b + b)}.
Global Instance curve_params :
E.twisted_edwards_params
(F:=Fq) (Feq:=Logic.eq) (Fzero:=F.zero) (Fone:=F.one) (Fadd:=F.add) (Fmul:=F.mul)
(a:=a) (d:=d). Proof Pre.curve25519_params_ok.
Definition E : Type := E.point
(F:=Fq) (Feq:=Logic.eq) (Fone:=F.one) (Fadd:=F.add) (Fmul:=F.mul)
(a:=a) (d:=d).
Axiom B : E. (* TODO(andreser) *)
Axiom Eenc : E -> Word.word b. (* TODO(jadep) *)
Axiom Senc : Fl -> Word.word b. (* TODO(jadep) *)
Require Import Crypto.Util.Decidable.
Definition ed25519 :
EdDSA (E:=E) (Eadd:=E.add) (Ezero:=E.zero) (EscalarMult:=E.mul) (B:=B)
(Eopp:=Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems.E.opp) (* TODO: move defn *)
(Eeq:=Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems.E.eq) (* TODO: move defn *)
(l:=l) (b:=b) (n:=n) (c:=c)
(Eenc:=Eenc) (Senc:=Senc) (H:=H).
Admitted.
End Ed25519.
|
