highlevel.tex 24.6 KB
Newer Older
1
\section{Proving that X25519 in Coq matches the mathematical model}
Benoit Viguier's avatar
Benoit Viguier committed
2
\label{sec:maths}
3

Benoit Viguier's avatar
Benoit Viguier committed
4
5
6
7
8
9
In this section we prove the following theorem:
\begin{theorem}
\label{thm:Elliptic-CSM}
The implementation of X25519 in TweetNaCl (\TNaCle{crypto_scalarmult}) computes the
$\F{p}$-restricted $x$-coordinate scalar multiplication on $E(\F{p^2})$ where $p$ is $\p$
and $E$ is the elliptic curve $y^2 = x^3 + 486662 x^2 + x$.
Benoit Viguier's avatar
Benoit Viguier committed
10
11
\end{theorem}

Benoit Viguier's avatar
Benoit Viguier committed
12
13
14
15
We first review the work of Bartzia and Strub \cite{BartziaS14} (\ref{subsec:ECC-Weierstrass}).
We extend it to support Montgomery curves (\ref{subsec:ECC-Montgomery})
with homogeneous coordinates (\ref{subsec:ECC-projective}) and prove the
correctness of the ladder (\ref{subsec:ECC-ladder}).
16
17

\subsection{Formalization of Elliptic Curves}
Benoit Viguier's avatar
Benoit Viguier committed
18
\label{subsec:ECC}
19
20
21
22

We consider elliptic curves over a field $\K$. We assume that the
characteristic of $\K$ is neither 2 or 3.

Benoit Viguier's avatar
Benoit Viguier committed
23
\begin{dfn}
24
Let a field $\K$, using an appropriate choice of coordinates, an elliptic curve $E$
Benoit Viguier's avatar
Benoit Viguier committed
25
is a plane cubic algebraic curve $E(x,y)$ defined by an equation of the form:
26
27
28
29
30
$$E : y^2 + a_1 xy + a_3 y = x^3 + a_2 x^2 + a_4 x + a_6$$
where the $a_i$'s are in \K\ and the curve has no singular point (\ie no cusps
or self-intersections). The set of points, written $E(\K)$, is formed by the
solutions $(x,y)$ of $E$ augmented by a distinguished point $\Oinf$ (called point at infinity):
$$E(\K) = \{(x,y) \in \K \times \K | E(x,y)\} \cup \{\Oinf\}$$
Benoit Viguier's avatar
Benoit Viguier committed
31
\end{dfn}
32
33

\subsubsection{Weierstra{\ss} Curves}
Benoit Viguier's avatar
Benoit Viguier committed
34
35
\label{subsec:ECC-Weierstrass}

Benoit Viguier's avatar
Benoit Viguier committed
36
This equation $E(x,y)$ can be reduced into its short Weierstra{\ss} form.
37

Benoit Viguier's avatar
Benoit Viguier committed
38
\begin{dfn}
Benoit Viguier's avatar
Benoit Viguier committed
39
40
Let $a \in \K$, and $b \in \K$ such that $$\Delta(a,b) = -16(4a^3 + 27b^2) \neq 0.$$
The \textit{elliptic curve} $E_{a,b}(\K)$ is the set of all points $(x,y) \in \K^2$ satisfying the equation:
41
$$y^2 = x^3 + ax + b,$$
Benoit Viguier's avatar
Benoit Viguier committed
42
along with an additional formal point $\Oinf$, ``at infinity''. Such a curve does not present any singularity.
Benoit Viguier's avatar
Benoit Viguier committed
43
\end{dfn}
44
45

In this setting, Bartzia and Strub defined the parametric type \texttt{ec} which
Benoit Viguier's avatar
Benoit Viguier committed
46
represent the points on a specific curve. It is parameterized by
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
a \texttt{K : ecuFieldType} -- the type of fields which characteristic is not 2 or 3 --
and \texttt{E : ecuType} -- a record that packs the curve parameters $a$ and $b$
along with the proof that $\Delta(a,b) \neq 0$.
\begin{lstlisting}[language=Coq]
Inductive point := EC_Inf | EC_In of K * K.
Notation "(| x, y |)" := (EC_In x y).
Notation "\infty" := (EC_Inf).

Record ecuType :=
  { A : K; B : K; _ : 4 * A^3 + 27 * B^2 != 0}.
Definition oncurve (p : point) :=
  if p is (| x, y |)
    then y^2 == x^3 + A * x + B
    else true.
Inductive ec : Type := EC p of oncurve p.
\end{lstlisting}

Benoit Viguier's avatar
Benoit Viguier committed
64
Points of an elliptic curve are equipped with a structure of an abelian group.
65
\begin{itemize}
Benoit Viguier's avatar
Benoit Viguier committed
66
  \item The negation of a point $P = (x,y)$ by taking the symmetric with respect to the x axis $-P = (x, -y)$.
67
68
  \item The addition of two points $P$ and $Q$ is defined by the negation of third intersection
  of the line passing by $P$ and $Q$ or tangent to $P$ if $P = Q$.
Benoit Viguier's avatar
Benoit Viguier committed
69
  \item $\Oinf$ is the neutral element under this law: if 3 points are collinear, their sum is equal to $\Oinf$.
70
71
\end{itemize}

Benoit Viguier's avatar
Benoit Viguier committed
72
These operations are defined in Coq as follow:
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
\begin{lstlisting}[language=Coq]
Definition neg (p : point) :=
  if p is (| x, y |) then (| x, -y |) else EC_Inf.

Definition add (p1 p2 : point) :=
  match p1, p2 with
    | \infty , _ => p2
    | _ , \infty => p1
    | (| x1, y1 |), (| x2, y2 |) =>
      if x1 == x2 then ... else
        let s := (y2 - y1) / (x2 - x1) in
        let xs := s^2 - x1 - x2 in
          (| xs, - s * (xs - x1 ) - y1 |)
  end.
\end{lstlisting}

Benoit Viguier's avatar
Benoit Viguier committed
89
And are proven internal to the curve (with coercion):
90
91
92
93
94
95
96
97
\begin{lstlisting}[language=Coq]
Lemma addO (p q : ec): oncurve (add p q).

Definition addec (p1 p2 : ec) : ec :=
  EC p1 p2 (addO p1 p2)
\end{lstlisting}

\subsubsection{Montgomery Curves}
Benoit Viguier's avatar
Benoit Viguier committed
98
99
\label{subsec:ECC-Montgomery}

Benoit Viguier's avatar
Benoit Viguier committed
100
101
Speedups can be obtained by switching to homogeneous coordinates and other forms
than the Weierstra{\ss} form. We consider the Montgomery form \cite{MontgomerySpeeding}.
102

Benoit Viguier's avatar
Benoit Viguier committed
103
\begin{dfn}
Benoit Viguier's avatar
Benoit Viguier committed
104
105
  Let $a \in \K \backslash \{-2, 2\}$, and $b \in \K \backslash \{ 0\}$.
  The \textit{Montgomery curve} $M_{a,b}(\K)$ is the set of all points $(x,y) \in \K^2$ satisfying the equation:
106
107
  $$by^2 = x^3 + ax^2 + x,$$
  along with an additional formal point $\Oinf$, ``at infinity''.
Benoit Viguier's avatar
Benoit Viguier committed
108
\end{dfn}
109
Using a similar representation, we defined the parametric type \texttt{mc} which
Benoit Viguier's avatar
Benoit Viguier committed
110
represent the points on a specific Montgomery curve. It is parameterized by
111
a \texttt{K : ecuFieldType} -- the type of fields which characteristic is not 2 or 3 --
Benoit Viguier's avatar
Benoit Viguier committed
112
and \texttt{M : mcuType} -- a record that packs the curve parameters $a$ and $b$
Benoit Viguier's avatar
Benoit Viguier committed
113
along with the proofs that $b \neq 0$ and $a^2 \neq 4$.
114
115
116
117
118
119
120
121
122
123
124
\begin{lstlisting}[language=Coq]
Record mcuType :=
  { cA : K; cB : K; _ : cB != 0; _ : cA^2 != 4}.
Definition oncurve (p : point K) :=
if p is (| x, y |)
  then cB * y^+2 == x^+3 + cA * x^+2 + x
  else true.
Inductive mc : Type := MC p of oncurve p.

Lemma oncurve_mc: forall p : mc, oncurve p.
\end{lstlisting}
Benoit Viguier's avatar
Benoit Viguier committed
125
We define the addition on Montgomery curves the same way as it is in the Weierstra{\ss} form,
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
however the actual computations will be slightly different.
\begin{lstlisting}[language=Coq]
Definition add (p1 p2 : point K) :=
  match p1, p2 with
    | \infty, _ => p2
    | _, \infty => p1
    | (|x1, y1|), (|x2, y2|) =>
      if   x1 == x2
      then if  (y1 == y2) && (y1 != 0)
           then ... else \infty
      else
        let s  := (y2 - y1) / (x2 - x1) in
        let xs := s^+2 * cB - cA - x1 - x2 in
          (| xs, - s * (xs - x1) - y1 |)
    end.
\end{lstlisting}
But we prove it is internal to the curve (again with coercion):
\begin{lstlisting}[language=Coq]
Lemma addO (p q : mc) : oncurve (add p q).
Definition addmc (p1 p2 : mc) : mc :=
  MC p1 p2 (addO p1 p2)
\end{lstlisting}

We then prove a bijection between a Montgomery curve and its Weierstra{\ss} equation.
\begin{lemma}
  Let $M_{a,b}(\K)$ be a Montgomery curve, define $$a' = \frac{3-a^2}{3b^2} \text{\ \ \ \ and\ \ \ \ } b' = \frac{2a^3 - 9a}{27b^3}.$$
  then $E_{a',b'}(\K)$ is an elliptic curve, and the mapping $\varphi : M_{a,b}(\K) \mapsto E_{a',b'}(\K)$ defined as:
  \begin{align*}
    \varphi(\Oinf_M) &= \Oinf_E\\
    \varphi( (x , y) ) &= ( \frac{x}{b} + \frac{a}{3b} , \frac{y}{b} )
  \end{align*}
  is an isomorphism between groups.
\end{lemma}
\begin{lstlisting}[language=Coq]
Definition ec_of_mc_point p :=
  match p with
  | \infty => \infty
  | (|x, y|) => (|x/(M#b) + (M#a)/(3%:R * (M#b)), y/(M#b)|)
  end.
Lemma ec_of_mc_point_ok p :
  oncurve M p ->
  ec.oncurve E (ec_of_mc_point p).

Definition ec_of_mc p :=
  EC (ec_of_mc_point_ok (oncurve_mc p)).

Lemma ec_of_mc_bij : bijective ec_of_mc.
\end{lstlisting}

\subsubsection{Projective Coordinates}
Benoit Viguier's avatar
Benoit Viguier committed
176
177
\label{subsec:ECC-projective}

Benoit Viguier's avatar
Benoit Viguier committed
178
179
180
181
182
183
184
185
186
187
188
189
On a projective plane, points are represented with a triple $(X:Y:Z)$.
With the exception of $(0:0:0)$, any points can be projected.
Scalar multiples are representing the same point, \ie
for all $\lambda \neq 0$, $(X:Y:Z)$ are $(\lambda X:\lambda Y:\lambda Z)$ defining
the same point.
For $Z\neq 0$, the projective point $(X:Y:Z)$ corresponds to the
point $(X/Z,Y/Z)$ on the Euclidean plane, likewise the point $(X,Y)$ on the
Euclidean plane corresponds to $(X:Y:1)$ on the projective plane.

Using fractions as coordinates, the equation for a Montgomery curve $M_{a,b}(\K)$
becomes:
$$b \bigg(\frac{Y}{Z}\bigg)^2 = \bigg(\frac{X}{Z}\bigg)^3 + a \bigg(\frac{X}{Z}\bigg)^2 + \bigg(\frac{X}{Z}\bigg)$$
190
Multiplying both sides by $Z^3$ yields:
Benoit Viguier's avatar
Benoit Viguier committed
191
$$b Y^2Z = X^3 + a X^2Z + XZ^2$$
Benoit Viguier's avatar
Benoit Viguier committed
192
193
With this equation we can additionally represent the ``point at infinity''. By
setting $Z=0$, we derive $X=0$, giving us the ``infinite points'' $(0:Y:0)$ with $Y\neq 0$.
194

Benoit Viguier's avatar
Benoit Viguier committed
195
By restricting the parameter $a$ of $M_{a,b}(\K)$ such that $a^2-4$ is not a
Benoit Viguier's avatar
Benoit Viguier committed
196
square in \K, we ensure that $(0,0)$ is the only point with a $y$-coordinate of $0$.
197
198
199
200
\begin{lstlisting}[language=Coq]
Hypothesis mcu_no_square : forall x : K, x^+2 != (M#a)^+2 - 4%:R.
\end{lstlisting}

Benoit Viguier's avatar
Benoit Viguier committed
201
202
We define $\chi$ and $\chi_0$ to return the $x$-coordinate of points on a curve.
\begin{dfn}Let $\chi$ and $\chi_0$:\\
203
204
205
206
-- $\chi : M_{a,b}(\K) \to \K \cup \{\infty\}$\\
  such that $\chi(\Oinf) = \infty$ and $\chi((x,y)) = x$.\\
-- $\chi_0 : M_{a,b}(\K) \to \K$\\
  such that $\chi_0(\Oinf) = 0$ and $\chi_0((x,y)) = x$.
Benoit Viguier's avatar
Benoit Viguier committed
207
\end{dfn}
Benoit Viguier's avatar
Benoit Viguier committed
208
209
Using projective coordinates we prove the
With those coordinates we prove the following lemmas for the addition of two points.
210
\begin{lemma}
211
\label{lemma:add}
Benoit Viguier's avatar
Benoit Viguier committed
212
213
Let $M_{a,b}(\K)$ be a Montgomery curve such that $a^2-4$ is not a square, and
let $X_1, Z_1, X_2, Z_2, X_3, Z_3 \in \K$, such that $(X_1,Z_1) \neq (0,0)$, $(X_2,Z_2) \neq (0,0)$, $X_4 \neq 0$ and $Z_4 \neq 0$.
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
Define
\begin{align*}
X_3 &= Z_4((X_1 - Z_1)(X_2+Z_2) + (X_1+Z_1)(X_2-Z_2))^2\\
Z_3 &= X_4((X_1 - Z_1)(X_2+Z_2) - (X_1+Z_1)(X_2-Z_2))^2,
\end{align*}
then for any point $P_1$ and $P_2$ on $M_{a,b}(\K)$ such that $X_1/Z_1 = \chi(P_1), X_2/Z_2 = \chi(P_2)$, and $X_4/Z_4 = \chi(P_1 - P_2)$, we have $X_3/Z_3 = \chi(P_1+P_2)$.\\
\textbf{Remark:} For any $x \in \K \backslash\{0\}, x/0$ should be understood as $\infty$.
\end{lemma}
% This can be formalized as follow:
% \begin{lstlisting}[language=Coq]
% Inductive K_infty :=
% | K_Inf : K_infty
% | K_Fin : K -> K_infty.
%
% Definition point_x (p : point K) :=
%   if p is (|x, _|) then K_Fin x else K_Inf.
% Local Notation "p '#x'" := (point_x p) (at level 30).
% Definition point_x0 (p : point K) :=
%   if p is (|x, _|) then x else 0.
%   Local Notation "p '#x0'" := (point_x0 p) (at level 30).
%
% Definition inf_div (x z : K) :=
%   if z == 0 then K_Inf else K_Fin (x / z).
% Definition hom_ok (x z : K) := (x != 0) || (z != 0).
% Lemma montgomery_hom_neq :
%   forall x1 x2 x4 z1 z2 z4 : K,
%   hom_ok x1 z1 -> hom_ok x2 z2 ->
%   (x4 != 0) && (z4 != 0) ->
%   let x3 := z4 * ((x1 - z1)*(x2 + z2)
%     + (x1 + z1)*(x2 - z2))^+2 in
%   let z3 := x4 * ((x1 - z1)*(x2 + z2)
%     - (x1 + z1)*(x2 - z2))^+2 in
%   forall p1 p2 : point K,
%   oncurve M p1 -> oncurve M p2 ->
%   p1#x = inf_div x1 z1 ->
%   p2#x = inf_div x2 z2 ->
%   (p1 \- p2)#x = inf_div x4 z4 ->
%   hom_ok x3 z3 && ((p1 \+ p2)#x == inf_div x3 z3).
% \end{lstlisting}

With those coordinates we also prove a similar lemma for point doubling.
\begin{lemma}
256
\label{lemma:double}
Benoit Viguier's avatar
Benoit Viguier committed
257
258
Let $M_{a,b}(\K)$ be a Montgomery curve such that $a^2-4$ is not a square, and
let $X_1, Z_1, X_2, Z_2, X_3, Z_3 \in \K$, such that $(X_1,Z_1) \neq (0,0)$. Define
259
260
261
262
263
\begin{align*}
  c &= (X_1 + Z_1)^2 - (X_1 - Z_1)^2\\
X_3 &= (X_1 + Z_1)^2(X_1-Z_1)^2\\
Z_3 &= c\Big((X_1 + Z_1)^2+\frac{a-2}{4}\times c\Big),
\end{align*}
Benoit Viguier's avatar
Benoit Viguier committed
264
265
then for any point $P_1$ on $M_{a,b}(\K)$ such that $X_1/Z_1 = \chi(P_1)$,
we have $X_3/Z_3 = \chi(2P_1)$.
266
267
268
269
270
271
272
273
274
275
276
277
278
279
\end{lemma}
% Which is formalized as follow:
% \begin{lstlisting}[language=Coq]
% Lemma montgomery_hom_eq :
%   forall x1 z1 : K,
%   hom_ok x1 z1 ->
%   let c := (x1 + z1)^+2 - (x1 - z1)^+2 in
%   let x3 := (x1 + z1)^+2 * (x1 - z1)^+2 in
%   let z3 := c * ((x1 + z1)^+2 + (((M#a) - 2%:R)/4%:R) * c) in
%   forall p : point K, oncurve M p ->
%   p#x = inf_div x1 z1 ->
%   (p \+ p)#x = inf_div x3 z3.
% \end{lstlisting}

280
With these two lemmas (\ref{lemma:add} and \ref{lemma:double}), we have the basic
Benoit Viguier's avatar
Benoit Viguier committed
281
tools to compute efficiently additions and point doubling on projective coordinates.
282
283

\subsubsection{Scalar Multiplication Algorithms}
Benoit Viguier's avatar
Benoit Viguier committed
284
\label{subsec:ECC-ladder}
285

Benoit Viguier's avatar
Benoit Viguier committed
286
287
288
289
Suppose we have a scalar $n$ and a point $P$ on some curve. The most straightforward
way to compute $n \cdot P$ is to repetitively add $P$ \ie computing $P + \ldots + P$.
However there is an more efficient algorithm which makes use of the binary
representation of $n$ and by combining doubling and adding and starting from $\Oinf$.
290
291
\eg for $n=11$, we compute $2(2(2(2\Oinf + P)) + P)+ P$.

Benoit Viguier's avatar
Benoit Viguier committed
292
293
294
With a simple double-and-add algorithm, with careful timing, an attacker could reconstruct $n$.
In the case of X25519, $n$ is the private key. With the Montgomery's ladder, while
it provides slightly more computations and an extra variable, we can prevent such weakness.
Benoit Viguier's avatar
Benoit Viguier committed
295
See \aref{alg:montgomery-ladder}.
296
297

\begin{lemma}
298
\label{lemma:montgomery-ladder}
Benoit Viguier's avatar
Benoit Viguier committed
299
\aref{alg:montgomery-ladder} is correct, \ie it respects its output conditions given the input conditions.
300
301
\end{lemma}

Benoit Viguier's avatar
Benoit Viguier committed
302
In Curve25519 we are only interested in the $x$ coordinate of points, using
303
Lemmas \ref{lemma:add} and \ref{lemma:double}, and replacing the if statements
Benoit Viguier's avatar
Benoit Viguier committed
304
with conditional swapping we can define a ladder similar to the one used in TweetNaCl.
Benoit Viguier's avatar
Benoit Viguier committed
305
See \aref{alg:montgomery-double-add}
306
307
308

\begin{algorithm}
\caption{Montgomery ladder for scalar multiplication on $M_{a,b}(\K)$ with optimizations}
Benoit Viguier's avatar
Benoit Viguier committed
309
\label{alg:montgomery-double-add}
310
311
\begin{algorithmic}
\REQUIRE{$x \in \K\backslash \{0\}$, scalars $n$ and $m$, $n < 2^m$}
Benoit Viguier's avatar
Benoit Viguier committed
312
\ENSURE{$a/c = \chi_0(n \cdot P)$ for any $P$ such that $\chi_0(P) = x$}
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
\STATE $(a,b,c,d) \leftarrow (1,x,0,1)$
\FOR{$k$ := $m$ downto $1$}
  \IF{$k^{\text{th}}$ bit of $n$ is $1$}
    \STATE $(a,b) \leftarrow (b,a)$
    \STATE $(c,d) \leftarrow (d,c)$
  \ENDIF
  \STATE $e \leftarrow a + c$
  \STATE $a \leftarrow a - c$
  \STATE $c \leftarrow b + d$
  \STATE $b \leftarrow b - d$
  \STATE $d \leftarrow e^2$
  \STATE $f \leftarrow a^2$
  \STATE $a \leftarrow c \times a$
  \STATE $c \leftarrow b \times e$
  \STATE $e \leftarrow a + c$
  \STATE $a \leftarrow a - c$
  \STATE $b \leftarrow a^2$
  \STATE $c \leftarrow d-f$
  \STATE $a \leftarrow c\times\frac{A - 2}{4}$
  \STATE $a \leftarrow a + d$
  \STATE $c \leftarrow c \times a$
  \STATE $a \leftarrow d \times f$
  \STATE $d \leftarrow b \times x$
  \STATE $b \leftarrow e^2$
  \IF{$k^{\text{th}}$ bit of $n$ is $1$}
    \STATE $(a,b) \leftarrow (b,a)$
    \STATE $(c,d) \leftarrow (d,c)$
  \ENDIF
\ENDFOR
\end{algorithmic}
\end{algorithm}

\begin{lemma}
346
\label{lemma:montgomery-double-add}
Benoit Viguier's avatar
Benoit Viguier committed
347
\aref{alg:montgomery-double-add} is correct, \ie it respects its output
Benoit Viguier's avatar
Benoit Viguier committed
348
conditions given the input conditions.
349
350
351
352
\end{lemma}

%% here we have \chi and \chi_0 ...

353
We formalized this lemma (\ref{lemma:montgomery-double-add}):
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
\begin{lstlisting}[language=Coq]
Lemma opt_montgomery_x :
  forall (n m : nat) (x : K),
  n < 2^m -> x != 0 ->
  forall (p : mc M), p#x0 = x ->
  opt_montgomery n m x = (p *+ n)#x0.
\end{lstlisting}

We can remark that for an input $x = 0$, the ladder returns $0$.
\begin{lstlisting}[language=Coq]
Lemma opt_montgomery_0:
  forall (n m : nat), opt_montgomery n m 0 = 0.
\end{lstlisting}
Also \Oinf\ is the neutral element over $M_{a,b}(\K)$, we have:
$$\forall P, P + \Oinf\ = P$$
thus we derive the following lemma.
% \begin{lemma}
371
% \label{lemma:montgomery-double-add}
372
373
374
375
376
377
378
379
380
381
% Algorithm \ref{montgomery-double-add} is correct even if $x=0$, \ie it respects its output conditions given the input conditions or $x=0$.
% \end{lemma}
\begin{lstlisting}[language=Coq]
Lemma p_x0_0_eq_0 : forall (n : nat) (p : mc M),
  p #x0 = 0%:R -> (p *+ n) #x0 = 0%R.
\end{lstlisting}
And thus the theorem of the correctness of the Montgomery ladder.
\begin{theorem}
\label{montgomery-ladder-correct}
For all $n, m \in \N$, $x \in \K$, $P \in M_{a,b}(\K)$,
Benoit Viguier's avatar
Benoit Viguier committed
382
if $\chi_0(P) = x$ then \aref{alg:montgomery-double-add} returns $\chi_0(n \cdot P)$
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
\end{theorem}
\begin{lstlisting}[language=Coq]
Theorem opt_montgomery_ok (n m: nat) (x : K) :
  n < 2^m ->
  forall (p : mc M), p#x0 = x ->
  opt_montgomery n m x = (p *+ n)#x0.
\end{lstlisting}

\subsection{Curves, Twists and Extension Fields}

One hypothesis to be able to use the above theorem is that $a^2-4$ is not a square:
$$\forall x \in \K,\ x^2 \neq a^2-4$$
As Curve25519 is defined over the field $\K = \F{p^2}$, there exists $x$ such that $x^2 = a^2-4$.
We first study Curve25519 and one of the quadratic twist Twist25519, first defined over \F{p}.

\subsubsection{Curves and Twists}

We define $\F{p}$ as the numbers between $0$ and $p = \p$.
We create a \coqe{Zmodp} module to encapsulate those definitions.
\begin{lstlisting}[language=Coq]
Module Zmodp.
Definition betweenb x y z := (x <=? z) && (z <? y).
Definition p := locked (2^255 - 19).
Fact Hp_gt0 : p > 0.
Inductive type := Zmodp x of betweenb 0 p x.

Lemma Z_mod_betweenb (x y : Z) :
  y > 0 -> betweenb 0 y (x mod y).

Definition pi (x : Z) : type :=
  Zmodp (Z_mod_betweenb x Hp_gt0).
Coercion repr (x : type) : Z :=
  let: @Zmodp x _ := x in x.
End Zmodp.
\end{lstlisting}

We define the basic operations ($+, -, \times$) with their respective neutral elements ($0, 1$).
\begin{lemma}
$\F{p}$ is a commutative ring.
\end{lemma}
% \begin{lstlisting}[language=Coq]
% Definition zero : type := pi 0.
% Definition one : type := pi 1.
% Definition opp (x : type) : type := pi (p - x).
% Definition add (x y : type) : type := pi (x + y).
% Definition sub (x y : type) : type := pi (x - y).
% Definition mul (x y : type) : type := pi (x * y).
%
% Lemma Zmodp_ring :
%   ring_theory zero one add mul sub opp eq.
% \end{lstlisting}
And finally for $a = 486662$, by using the Legendre symbol we prove that $a^2 - 4$ and $2$ are not squares in $\F{p}$.
\begin{lstlisting}[language=Coq]
Lemma a_not_square : forall x: Zmodp.type,
  x^+2 != (Zmodp.pi 486662)^+2 - 4%:R.
\end{lstlisting}
\begin{lstlisting}[language=Coq,label=two_not_square]
Lemma two_not_square : forall x : Zmodp.type,
  x^+2 != 2%:R.
\end{lstlisting}
We consider $M_{486662,1}(\F{p})$ and $M_{486662,2}(\F{p})$, one of its quadratic twist.
% $M_{486662,1}(\F{p})$ has the same equation as $M_{486662,1}(\F{p^2})$ while $M_{486662,2}(\F{p})$ is one of its quadratic twist.


Benoit Viguier's avatar
Benoit Viguier committed
447
By instantiating theorem \ref{montgomery-ladder-correct} we derive the following two lemmas:
448
449
\begin{lemma} For all $x \in \F{p},\ n \in \N,\ P \in \F{p} \times \F{p}$,\\
such that $P \in M_{486662,1}(\F{p})$ and $\chi_0(P) = x$.
Benoit Viguier's avatar
Benoit Viguier committed
450
Given $n$ and $x$, $Curve25519\_Fp(n,x) = \chi_0(n \cdot P)$.
451
452
453
\end{lemma}
\begin{lemma} For all $x \in \F{p},\ n \in \N,\ P \in \F{p} \times \F{p}$\\
such that $P \in M_{486662,2}(\F{p})$ and $\chi_0(P) = x$.
Benoit Viguier's avatar
Benoit Viguier committed
454
Given $n$ and $x$, $Twist25519\_Fp(n,x) = \chi_0(n \cdot P)$.
455
\end{lemma}
Benoit Viguier's avatar
Benoit Viguier committed
456
As the Montgomery ladder defined above does not depend on $b$, it is trivial to see that the computations done for points of $M_{486662,1}(\F{p})$ and of $M_{486662,2}(\F{p})$ are the same.
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
\begin{lstlisting}[language=Coq]
Theorem curve_twist_eq: forall n x,
  curve25519_Fp_ladder n x = twist25519_Fp_ladder n x.
\end{lstlisting}

Because $2$ is not a square in $\F{p}$, it allows us split $\F{p}$ into two sets.
\begin{lemma}
\label{square-or-2square}
For all $x$ in $\F{p}$, there exists $y$ in $\F{p}$ such that
$$y^2 = x\ \ \ \lor\ \ 2y^2 = x$$
\end{lemma}
For all $x \in \F{p}$, we can compute $x^3 + ax^2 + x$. Using Lemma \ref{square-or-2square} we can find a $y$ such that $(x,y)$ is either on the curve or on the quadratic twist:
\begin{lemma}
\label{curve-or-twist}
For all $x \in \F{p}$, there exists a point $P$ over $M_{486662,1}(\F{p})$ or over $M_{486662,2}(\F{p})$ such that the $x$-coordinate of $P$ is $x$.
\end{lemma}
\begin{lstlisting}[language=Coq]
Theorem x_is_on_curve_or_twist: forall x : Zmodp.type,
  (exists (p : mc curve25519_mcuType), p#x0 = x) \/
  (exists (p' : mc twist25519_mcuType), p'#x0 = x).
\end{lstlisting}

\subsubsection{Curve25519 over \F{p^2}}

We use the same definitions as in \cite{Ber06}. We consider the extension field $\F{p^2}$ as the set $\F{p} \times \F{p}$ with $\delta = 2$, in other words,
the polynomial with coefficients in $\F{p}$ modulo $X^2 - 2$. In a similar way as for $\F{p}$ we use Module in Coq.
\begin{lstlisting}[language=Coq]
Benoit Viguier's avatar
Benoit Viguier committed
484
Module Zmodp2.
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
Inductive type :=
  Zmodp2 (x: Zmodp.type) (y:Zmodp.type).

Definition pi (x : Zmodp.type * Zmodp.type) : type :=
  Zmodp2 x.1 x.2.
Coercion repr (x : type) : Zmodp.type*Zmodp.type :=
  let: Zmodp2 u v := x in (u, v).

Definition zero : type :=
  pi ( 0%:R, 0%:R ).
Definition one : type :=
  pi ( 1, 0%:R ).
Definition opp (x : type) : type :=
  pi (- x.1 , - x.2).
Definition add (x y : type) : type :=
  pi (x.1 + y.1, x.2 + y.2).
Definition sub (x y : type) : type :=
  pi (x.1 - y.1, x.2 - y.2).
Definition mul (x y : type) : type :=
  pi ((x.1 * y.1) + (2%:R * (x.2 * y.2)),
      (x.1 * y.2) + (x.2 * y.1)).
\end{lstlisting}
We define the basic operations ($+, -, \times$) with their respective neutral elements ($0, 1$).
Additionally we verify that for each element of in $\F{p^2}\backslash\{0\}$, there exists a multiplicative inverse.
\begin{lemma} For all $x \in \F{p^2}\backslash\{0\}$ and $a,b \in \F{p}$ such that $x = (a,b)$,
$$x^{-1} = \Big(\frac{a}{a^2-2b^2}\ , \frac{-b}{a^2-2b^2}\Big)$$
\end{lemma}
Benoit Viguier's avatar
Benoit Viguier committed
512
Similarly as in $\F{p}$, we define $0^{-1} = 0$.
513
514
515
\begin{lemma}
$\F{p^2}$ is a commutative ring.
\end{lemma}
Benoit Viguier's avatar
Benoit Viguier committed
516
We can then specialize the basic operations in order to speed up the verification of formulas by using rewrite rules:
517
518
519
520
521
522
523
524
525
526
527
\begin{align*}
(a,0) + (b,0) &= (a+b, 0)\\
(a,0) \cdot   (b,0) &= (a \cdot b, 0)\\
(a, 0)^n &= (a^n, 0)\\
(a, 0)^{-1} &= (a^{-1}, 0)\\
(a, 0)\cdot (0,b) &= (0, a\cdot b)\\
(0, a)\cdot (0,b) &= (2\cdot a\cdot b, 0)\\
(0,a)^{-1} &= ((2\cdot a)^{-1},0)
\end{align*}
The injection $a \mapsto (a,0)$ from $\F{p}$ to $\F{p^2}$ preserves $0, 1, +, -, \times$. Thus $(a,0)$ can be abbreviated as $a$ without confusions.

Benoit Viguier's avatar
Benoit Viguier committed
528
We define $M_{486662,1}(\F{p^2})$. With the rewrite rule above, it is straightforward to prove that any point on the curve $M_{486662,1}(\F{p})$ is also on the curve $M_{486662,1}(\F{p^2})$. Similarly, any point on the quadratic twist $M_{486662,2}(\F{p})$ is also on the curve $M_{486662,1}(\F{p^2})$.
529
530
531
532
533
534
535
536
537
538
As direct consequence, using lemma \ref{curve-or-twist}, we prove that for all $x \in \F{p}$, there exists a point $P \in \F{p^2}\times\F{p^2}$ on $M_{486662,2}(\F{p})$ such that $\chi_0(P)$ is $(x,0)$

\begin{lstlisting}[language=Coq]
Theorem x_is_on_curve_or_twist_implies_x_in_Fp2:
  forall (x:Zmodp.type),
    exists (p: mc curve25519_Fp2_mcuType),
      p#x0 = Zmodp2.Zmodp2 x 0.
\end{lstlisting}

We now study the case of the scalar multiplication and show similar proofs.
Benoit Viguier's avatar
Benoit Viguier committed
539
\begin{dfn}
540
541
542
543
544
545
546
Define the functions $\varphi_c$, $\varphi_t$ and $\psi$\\
-- $\varphi_c: M_{486662,1}(\F{p}) \mapsto M_{486662,1}(\F{p^2})$\\
  such that $\varphi((x,y)) = ((x,0), (y,0))$.\\
-- $\varphi_t: M_{486662,2}(\F{p}) \mapsto M_{486662,1}(\F{p^2})$\\
  such that $\varphi((x,y)) = ((x,0), (0,y))$.\\
-- $\psi: \F{p^2} \mapsto \F{p}$\\
  such that $\psi(x,y) = (x)$.
Benoit Viguier's avatar
Benoit Viguier committed
547
\end{dfn}
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562

\begin{lemma}
For all $n \in \N$, for all point $P\in\F{p}\times\F{p}$ on the curve $M_{486662,1}(\F{p})$ (respectively on the quadratic twist $M_{486662,2}(\F{p})$), we have:
\begin{align*}
P \in M_{486662,1}(\F{p}) &\implies \varphi_c(n \cdot P) = n \cdot \varphi_c(P)\\
P \in M_{486662,2}(\F{p}) &\implies \varphi_t(n \cdot P) = n \cdot \varphi_t(P)
\end{align*}
\end{lemma}

Notice that:
\begin{align*}
\forall P \in M_{486662,1}(\F{p}),\ \ \psi(\chi_0(\varphi_c(P))) = \chi_0(P)\\
\forall P \in M_{486662,2}(\F{p}),\ \ \psi(\chi_0(\varphi_t(P))) = \chi_0(P)
\end{align*}

Benoit Viguier's avatar
Benoit Viguier committed
563
In summary for all $n \in \N,\ n < 2^{255}$, for any given point $P\in\F{p}\times\F{p}$ on $M_{486662,1}(\F{p})$ or $M_{486662,2}(\F{p})$ \texttt{curve25519\_Fp\_ladder} computes the $\chi_0(n \cdot P)$.
564
565
566
We have proved that for all $P \in \F{p^2}\times\F{p^2}$ such that $\chi_0(P) \in \F{p}$ there exists a corresponding point on the curve or the twist over $\F{p}$.
We have proved that for any point, on the curve or the twist we can compute the scalar multiplication by $n$ and yield to the same result as if we did the computation in $\F{p^2}$. As a result we have proved theorem 2.1 of \cite{Ber06}:
\begin{theorem}
Benoit Viguier's avatar
Benoit Viguier committed
567
For all $n \in \N$, $x \in \F{P}$, $P \in M_{486662,1}(\F{p^2})$, such that $n < 2^{255}$ and $\chi_0(P) = \varphi(x)$, \texttt{curve25519\_Fp\_ladder}$(n, x)$ computes $\psi(\chi_0(n \cdot P))$.
568
569
570
571
572
573
574
575
576
\end{theorem}
which can be formalized in Coq as:
\begin{lstlisting}[language=Coq]
Lemma curve25519_Fp2_ladder_ok (n : nat) (x:Zmodp.type) :
    (n < 2^255)%nat ->
    forall (p  : mc curve25519_Fp2_mcuType),
    p #x0 = Zmodp2.Zmodp2 x 0 ->
    curve25519_Fp_ladder n x = (p *+ n)#x0 /p.
\end{lstlisting}
Benoit Viguier's avatar
Benoit Viguier committed
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604





By converting those array of 32 bytes into their respective little-endian value
we prove the correctness of \TNaCle{crypto_scalarmult} (Theorem \ref{CSM-correct})
in Coq (for the sake of simplicity we do not display the conversion in the theorem).
\begin{theorem}
\label{CSM-correct}
For all $n \in \N, n < 2^{255}$ and where the bits 1, 2, 5 248, 249, 250
are cleared and bit 6 is set, for all $P \in E(\F{p^2})$,
for all $p \in \F{p}$ such that $P.x = p$,
there exists $Q \in E(\F{p^2})$ such that $Q = \cdot P$ where $Q.x = q$ and $q$ = \VSTe{CSM} $n$ $p$.
\end{theorem}
A more complete description in Coq of Theorem \ref{CSM-correct} with the associated conversions
is as follow:
\begin{lstlisting}[language=Coq]
Theorem Crypto_Scalarmult_Correct:
  forall (n p:list Z) (P:mc curve25519_Fp2_mcuType),
  Zlength n = 32 ->
  Zlength p = 32 ->
  Forall (fun x => 0 <= x /\ x < 2^8) n ->
  Forall (fun x => 0 <= x /\ x < 2^8) p ->
  Fp2_x (ZUnpack25519 (ZofList 8 p)) = P#x0 ->
  ZofList 8 (Crypto_Scalarmult n p) =
    (P *+ (Z.to_nat (Zclamp (ZofList 8 n)))) _x0.
\end{lstlisting}