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 Crypto.Algebra.
Require Import Crypto.Util.Notations.
Module MxDH. (* from RFC7748 *)
Section MontgomeryLadderKeyExchange.
Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {field:@Algebra.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {Feq_dec:Decidable.DecidableRel Feq}.
Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope.
Local Infix "+" := Fadd. Local Infix "*" := Fmul.
Local Infix "-" := Fsub. Local Infix "/" := Fdiv.
Local Notation "x ^ 2" := (x*x) (at level 30).
Local Notation "0" := Fzero. Local Notation "1" := Fone.
Local Notation "2" := (1+1). Local Notation "4" := (2+2).
Context {a b: F}. (* parameters of the Montgomery curve *)
Context {nonsquare_aa_m4:~exists sqrt, sqrt^2 = a^2-4} {five_neq_zero:1+4<>0}.
(* Implemention from RFC7748. Note that this differs from EFD and
Montgomery '87 in the choice of which precomputed constant to use
for [a] *)
(* Ideally we would want to verify that this correspons to
x-coordinate addition on the relevant elliptic curve, as
specified by addition formulas in Montgomery coordinates.
However, even if we did get to doing that, we still would not
want to change the type of the ladder function to talk about
points that are on the curve -- there are contexts where this
can be, carefully, used with values that are not verified to
be on the curve *)
Context {a24:F} {a24_correct:4*a24 = a-2}.
Section generic.
Context (F4 : Type)
(pair4 : F -> F -> F -> F -> F4)
(let_in : F -> (F -> F4) -> F4).
Local Notation "'slet' x := y 'in' z" := (let_in y (fun x => z)).
Definition ladderstep_gen (X1:F) (P1 P2:F * F) : F4 :=
let '(X2, Z2) := P1 in
let '(X3, Z3) := P2 in
slet A := X2+Z2 in
slet AA := A^2 in
slet B := X2-Z2 in
slet BB := B^2 in
slet E := AA-BB in
slet C := X3+Z3 in
slet D := X3-Z3 in
slet DA := D*A in
slet CB := C*B in
slet X5 := (DA+CB)^2 in
slet Z5 := X1*(DA-CB)^2 in
slet X4 := AA*BB in
slet Z4 := E*(AA + a24*E) in
pair4 X4 Z4 X5 Z5.
End generic.
Definition ladderstep (X1:F) (P1 P2:F*F) : (F*F)*(F*F) :=
Eval cbv beta delta [ladderstep_gen] in
@ladderstep_gen
((F*F)*(F*F))
(fun X3 Y3 Z3 T3 => ((X3, Y3), (Z3, T3)))
(fun x f => let y := x in f y)
X1 P1 P2.
Context {cswap:bool->F*F->F*F->(F*F)*(F*F)}.
Fixpoint downto_iter (i:nat) : list nat :=
match i with
| Datatypes.S i' => cons i' (downto_iter i')
| O => nil
end.
Definition downto {state} init count (step:state->nat->state) : state :=
List.fold_left step (downto_iter count) init.
Local Notation xor := Coq.Init.Datatypes.xorb.
(* Ideally, we would verify that this corresponds to x coordinate
multiplication *)
Definition montladder bound (testbit:nat->bool) (u:F) :=
let '(P1, P2, swap) :=
downto
((1, 0), (u, 1), false)
bound
(fun state i =>
let '(P1, P2, swap) := state in
let s_i := testbit i in
let swap := xor swap s_i in
let '(P1, P2) := cswap swap P1 P2 in
let swap := s_i in
let '(P1, P2) := ladderstep u P1 P2 in
(P1, P2, swap)
) in
let '((x, z), _) := cswap swap P1 P2 in
x * Finv z.
End MontgomeryLadderKeyExchange.
End MxDH.
(* see [Test.Curve25519SpecTestVectors] for sanity-checks *)
|
