highlevel.tex 24.7 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
In this section we prove the following informal theorem:
Benoit Viguier's avatar
Benoit Viguier committed
5
6

\begin{informaltheorem}
benoit's avatar
wip    
benoit committed
7
8
9
  The implementation of X25519 in TweetNaCl computes the
  $\F{p}$-restricted \xcoord 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{informaltheorem}

Benoit Viguier's avatar
Benoit Viguier committed
12
More precisely, we prove that our formalization of the RFC matches the definitions of Curve25519 by Bernstein:
Benoit Viguier's avatar
Benoit Viguier committed
13
14
15
16
17
18
19
20
21
\begin{lstlisting}[language=Coq]
Theorem RFC_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 (decodeUCoordinate p) = P#x0 ->
  RFC n p =
Benoit Viguier's avatar
Benoit Viguier committed
22
23
    encodeUCoordinate
      ((P *+ (Z.to_nat (decodeScalar25519 n))) _x0).
Benoit Viguier's avatar
Benoit Viguier committed
24
\end{lstlisting}
Benoit Viguier's avatar
Benoit Viguier committed
25

Benoit Viguier's avatar
Benoit Viguier committed
26
27
28
29
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}).
Benoit Viguier's avatar
fixes    
Benoit Viguier committed
30
31
We discuss the twist of Curve25519 (\ref{subsec:Zmodp}) and explain how we deal
with it in the proofs (\ref{subsec:curvep2}).
32

33
\subsection{Formalization of elliptic Curves}
Benoit Viguier's avatar
Benoit Viguier committed
34
\label{subsec:ECC}
35

Benoit Viguier's avatar
Benoit Viguier committed
36
\fref{tikz:ProofHighLevel1} presents the structure of the proof of the ladder's
37
correctness. The white tiles are definitions, the orange ones are hypothesis and
38
39
40
41
42
43
44
45
46
the green tiles represent major lemmas and theorems.

We consider elliptic curves over a field $\K$. We assume that the
characteristic of $\K$ is neither 2 or 3.
We formalize the Montgomery curves ($M_{a,b}(\K)$), then by using the equivalent
Weierstra{\ss} form ($E_{a',b'}(\K)$) from the library of Bartzia and Strub, we prove
that $M_{a,b}(\K)$ forms an associative finite group. Under the hypothesis that
$a^2 - 4$ is not a square in $\K$, we prove the correctness of the ladder (\tref{thm:montgomery-ladder-correct}).

47
48
49
50
51
52
53
\begin{figure}[h]
  \centering
  \include{tikz/highlevel1}
  \caption{Overview of the proof of Montgomery ladder's correctness}
  \label{tikz:ProofHighLevel1}
\end{figure}

benoit's avatar
benoit committed
54
We now turn our attention to the details of the proof of the ladder's correctness.
55

Benoit Viguier's avatar
Benoit Viguier committed
56
\begin{dfn}
benoit's avatar
wip    
benoit committed
57
58
59
60
61
62
63
64
65
  Given a field $\K$,
  using an appropriate choice of coordinates,
  an elliptic curve $E$
  is a plane cubic algebraic curve defined by an equation $E(x,y)$ of the form:
  $$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 defined over \K, written $E(\K)$, is formed by the
  solutions $(x,y)$ of $E$ together with 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
66
\end{dfn}
67

Benoit Viguier's avatar
WIP    
Benoit Viguier committed
68
\subsubsection{Short Weierstra{\ss} curves}
Benoit Viguier's avatar
Benoit Viguier committed
69
70
\label{subsec:ECC-Weierstrass}

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

Benoit Viguier's avatar
Benoit Viguier committed
73
\begin{dfn}
benoit's avatar
wip    
benoit committed
74
75
76
77
78
  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}$ is defined by the equation:
  $$y^2 = x^3 + ax + b.$$
  $E_{a,b}(\K)$ is the set of all points $(x,y) \in \K^2$ satisfying the $E_{a,b}$
  along with an additional formal point $\Oinf$, ``at infinity''. Such a curve does not have any singularity.
Benoit Viguier's avatar
Benoit Viguier committed
79
\end{dfn}
80
81

In this setting, Bartzia and Strub defined the parametric type \texttt{ec} which
Benoit Viguier's avatar
Benoit Viguier committed
82
represent the points on a specific curve. It is parameterized by
benoit's avatar
wip    
benoit committed
83
a \texttt{K : ecuFieldType} --- the type of fields whose characteristic is not 2 or 3 ---
Benoit Viguier's avatar
WIP    
Benoit Viguier committed
84
and \texttt{E : ecuType} --- a record that packs the curve parameters $a$ and $b$
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
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
WIP    
Benoit Viguier committed
100
Points on an elliptic curve are equipped with the structure of an abelian group.
101
\begin{itemize}
Benoit Viguier's avatar
WIP    
Benoit Viguier committed
102
  \item The negation of a point $P = (x,y)$ is defined by reflection over the $x$ axis $-P = (x, -y)$.
103
  \item The addition of two points $P$ and $Q$ is defined as the negation of the third intersection point
benoit's avatar
wip    
benoit committed
104
        of the line passing through $P$ and $Q$, or tangent to $P$ if $P = Q$.
Benoit Viguier's avatar
Benoit Viguier committed
105
  \item $\Oinf$ is the neutral element under this law: if 3 points are collinear, their sum is equal to $\Oinf$.
106
\end{itemize}
107
These operations are defined in Coq as follows (where we omit the code for the tangent case):
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
\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's avatar
wip    
benoit committed
123
The value of \texttt{add} is proven to be on the curve with coercion:
124
125
126
127
128
129
130
\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}

131
\subsubsection{Montgomery curves}
Benoit Viguier's avatar
Benoit Viguier committed
132
133
\label{subsec:ECC-Montgomery}

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

Benoit Viguier's avatar
Benoit Viguier committed
137
\begin{dfn}
Benoit Viguier's avatar
Benoit Viguier committed
138
  Let $a \in \K \backslash \{-2, 2\}$, and $b \in \K \backslash \{ 0\}$.
Benoit Viguier's avatar
Benoit Viguier committed
139
  The \textit{elliptic curve} $M_{a,b}$ is defined by the equation:
140
  $$by^2 = x^3 + ax^2 + x,$$
Benoit Viguier's avatar
Benoit Viguier committed
141
  $M_{a,b}(\K)$ is the set of all points $(x,y) \in \K^2$ satisfying the $M_{a,b}$
142
  along with an additional formal point $\Oinf$, ``at infinity''.
Benoit Viguier's avatar
Benoit Viguier committed
143
\end{dfn}
144
145
146
Similar to the definition of \texttt{ec}, we defined the parametric type \texttt{mc} which
represents the points on a specific Montgomery curve.
It is parameterized by
benoit's avatar
wip    
benoit committed
147
a \texttt{K : ecuFieldType} --- the type of fields whose characteristic is not
Benoit Viguier's avatar
WIP    
Benoit Viguier committed
148
149
2 or 3 --- and \texttt{M : mcuType} --- a record that packs the curve
parameters $a$ and $b$ along with the proofs that $b \neq 0$ and $a^2 \neq 4$.
150
\begin{lstlisting}[language=Coq,belowskip=-0.1 \baselineskip]
151
152
153
154
155
156
157
158
159
160
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
161
We define the addition on Montgomery curves in a similar way as for the Weierstra{\ss} form.
162
\begin{lstlisting}[language=Coq,belowskip=-0.25 \baselineskip]
163
164
165
166
167
168
169
170
171
172
173
174
175
176
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}
Benoit Viguier's avatar
Benoit Viguier committed
177
And again we prove the result is on the curve: % (again with coercion):
178
179
\begin{lstlisting}[language=Coq]
Lemma addO (p q : mc) : oncurve (add p q).
180

181
182
183
184
Definition addmc (p1 p2 : mc) : mc :=
  MC p1 p2 (addO p1 p2)
\end{lstlisting}

185
186
We then define a bijection between a Montgomery curve and its short Weierstra{\ss} form
(\lref{lemma:bij-ecc}).
187
188
In this way we get associativity of addition on Montgomery curves from the
corresponding property for Weierstra{\ss} curves.
189
\begin{lemma}
190
  \label{lemma:bij-ecc}
Benoit Viguier's avatar
Benoit Viguier committed
191
  Let $M_{a,b}$ be a Montgomery curve, define
192
  $$a' = \frac{3-a^2}{3b^2} \text{\ \ \ \ and\ \ \ \ } b' = \frac{2a^3 - 9a}{27b^3}.$$
Benoit Viguier's avatar
Benoit Viguier committed
193
194
  then $E_{a',b'}$ is an elliptic curve, and the mapping
  $\varphi : M_{a,b} \mapsto E_{a',b'}$ defined as:
195
  \begin{align*}
benoit's avatar
wip    
benoit committed
196
197
    \varphi(\Oinf_M)   & = \Oinf_E                                                 \\
    \varphi( (x , y) ) & = \left( \frac{x}{b} + \frac{a}{3b} , \frac{y}{b} \right)
198
  \end{align*}
Benoit Viguier's avatar
WIP    
Benoit Viguier committed
199
  is an isomorphism between elliptic curves.
200
\end{lemma}
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
% \begin{lstlisting}[language=Coq,belowskip=-0.25 \baselineskip]
% 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}
216

217
\subsubsection{Projective coordinates}
Benoit Viguier's avatar
Benoit Viguier committed
218
219
\label{subsec:ECC-projective}

Freek Wiedijk's avatar
Freek Wiedijk committed
220
221
In a projective plane, points are represented with triples $(X:Y:Z)$,
with the exception of $(0:0:0)$.
Benoit Viguier's avatar
Benoit Viguier committed
222
Scalar multiples are representing the same point, \ie
223
for all $\lambda \neq 0$, the triples $(X:Y:Z)$ and $(\lambda X:\lambda Y:\lambda Z)$ represent
Benoit Viguier's avatar
Benoit Viguier committed
224
225
the same point.
For $Z\neq 0$, the projective point $(X:Y:Z)$ corresponds to the
Benoit Viguier's avatar
WIP    
Benoit Viguier committed
226
227
point $(X/Z,Y/Z)$ on the affine plane. Likewise the point $(X,Y)$ on the
affine plane corresponds to $(X:Y:1)$ on the projective plane.
Benoit Viguier's avatar
Benoit Viguier committed
228

Benoit Viguier's avatar
Benoit Viguier committed
229
Using fractions as coordinates, the equation for a Montgomery curve $M_{a,b}$
Benoit Viguier's avatar
Benoit Viguier committed
230
231
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)$$
232
Multiplying both sides by $Z^3$ yields:
Benoit Viguier's avatar
Benoit Viguier committed
233
$$b Y^2Z = X^3 + a X^2Z + XZ^2$$
Benoit Viguier's avatar
Benoit Viguier committed
234
With this equation we can additionally represent the ``point at infinity''. By
Benoit Viguier's avatar
WIP    
Benoit Viguier committed
235
setting $Z=0$, we derive $X=0$, giving us the ``infinite point'' $(0:1:0)$.
236

Benoit Viguier's avatar
Benoit Viguier committed
237
By restricting the parameter $a$ of $M_{a,b}(\K)$ such that $a^2-4$ is not a
238
239
square in \K (Hypothesis \ref{hyp:a_minus_4_not_square}),
we ensure that $(0,0)$ is the only point with a $y$-coordinate of $0$.
240
\begin{hypothesis}
benoit's avatar
wip    
benoit committed
241
242
  \label{hyp:a_minus_4_not_square}
  $a^2-4$ is not a square in \K.
243
\end{hypothesis}
244
\begin{lstlisting}[language=Coq]
245
246
Hypothesis mcu_no_square :
  forall x : K, x^+2 != (M#a)^+2 - 4%:R.
247
248
\end{lstlisting}

249
We define $\chi$ and $\chi_0$ to return the \xcoord of points on a curve.
Benoit Viguier's avatar
Benoit Viguier committed
250
\begin{dfn}Let $\chi$ and $\chi_0$:\\
251
252
253
254
255
256
257
  \vspace{-1em}
  \begin{itemize}
    \item[--] $\chi : M_{a,b}(\K) \to \K \cup \{\infty\}$\\
          such that $\chi(\Oinf) = \infty$ and $\chi((x,y)) = x$.
    \item[--] $\chi_0 : M_{a,b}(\K) \to \K$\\
          such that $\chi_0(\Oinf) = 0$ and $\chi_0((x,y)) = x$.
  \end{itemize}
Benoit Viguier's avatar
Benoit Viguier committed
258
\end{dfn}
Benoit Viguier's avatar
Benoit Viguier committed
259
Using projective coordinates we prove the formula for differential addition.% (\lref{lemma:xADD}).
260
\begin{lemma}
benoit's avatar
wip    
benoit committed
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
  \label{lemma:xADD}
  Let $M_{a,b}$ be a Montgomery curve such that $a^2-4$ is not a square in \K, and
  let $X_1, Z_1, X_2, Z_2, X_4, Z_4 \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$.
  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$ in $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:}
  These definitions should be understood in $\K \cup \{\infty\}$.
  If $x\ne 0$ then we define $x/0 = \infty$.
276
\end{lemma}
Benoit Viguier's avatar
Benoit Viguier committed
277
Similarly we also prove the formula for point doubling.% (\lref{lemma:xDBL}).
278
\begin{lemma}
benoit's avatar
wip    
benoit committed
279
280
281
282
283
284
285
286
287
288
  \label{lemma:xDBL}
  Let $M_{a,b}$ be a Montgomery curve such that $a^2-4$ is not a square in \K, and
  let $X_1, Z_1 \in \K$, such that $(X_1,Z_1) \neq (0,0)$. Define
  \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*}
  then for any point $P_1$ in $M_{a,b}(\K)$ such that $X_1/Z_1 = \chi(P_1)$,
  we have $X_3/Z_3 = \chi(2P_1)$.
289
\end{lemma}
290
291

With \lref{lemma:xADD} and \lref{lemma:xDBL}, we are able to compute efficiently
Freek Wiedijk's avatar
Freek Wiedijk committed
292
differential additions and point doublings using projective coordinates.
293

294
\subsubsection{Scalar multiplication algorithms}
Benoit Viguier's avatar
Benoit Viguier committed
295
\label{subsec:ECC-ladder}
296

297
298
By taking \aref{alg:montgomery-ladder} and replacing \texttt{xDBL\&ADD} by a
combination of the formulae from \lref{lemma:xADD} and \lref{lemma:xDBL},
Benoit Viguier's avatar
Benoit Viguier committed
299
300
we define a ladder \coqe{opt_montgomery} (in which $\K$ has not been fixed yet).
% similar to the one used in TweetNaCl (with \coqe{montgomery_rec}).
benoit's avatar
wip    
benoit committed
301
% shown above.
Benoit Viguier's avatar
Benoit Viguier committed
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322

% We prove its correctness for any point whose \xcoord is not 0.
%
% \begin{lstlisting}[language=Coq,belowskip=-0.25 \baselineskip]
% 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,belowskip=-0.25 \baselineskip]
% Lemma opt_montgomery_0:
%   forall (n m : nat), opt_montgomery n m 0 = 0.
% \end{lstlisting}
% Also \Oinf\ is the neutral element of $M_{a,b}(\K)$.
% \begin{lstlisting}[language=Coq,belowskip=-0.25 \baselineskip]
% Lemma p_x0_0_eq_0 : forall (n : nat) (p : mc M),
%   p #x0 = 0%:R -> (p *+ n) #x0 = 0%R.
% \end{lstlisting}
% This gives us the theorem of the correctness of the Montgomery ladder.
Freek Wiedijk's avatar
Freek Wiedijk committed
323
324

This gives us the theorem of the correctness of the Montgomery ladder.
325
\begin{theorem}
benoit's avatar
wip    
benoit committed
326
327
328
  \label{thm:montgomery-ladder-correct}
  For all $n, m \in \N$, $x \in \K$, $P \in M_{a,b}(\K)$,
  if $\chi_0(P) = x$ then \coqe{opt_montgomery} returns $\chi_0(n \cdot P)$
329
\end{theorem}
Benoit Viguier's avatar
Benoit Viguier committed
330
\begin{lstlisting}[language=Coq]
331
332
333
334
335
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}
Benoit Viguier's avatar
Benoit Viguier committed
336
The definition of \coqe{opt_montgomery} is similar to \coqe{montgomery_rec_swap}
Benoit Viguier's avatar
Benoit Viguier committed
337
338
339
340
that was used in \coqe{RFC}.
We proved their equivalence, and used it in our
final proof of \coqe{Theorem RFC_Correct}.

341

342
\subsection{Curves, twists and extension fields}
Benoit Viguier's avatar
Benoit Viguier committed
343
\label{subsec:curve_twist_fields}
344

Benoit Viguier's avatar
Benoit Viguier committed
345
\fref{tikz:ProofHighLevel2} gives a high-level view of the proofs presented here.
346
347
The white tiles are definitions while green tiles are important lemmas and theorems.

benoit's avatar
benoit committed
348
349
350
351
352
353
354
355
\begin{figure}[h]
  \centering
  \include{tikz/highlevel2}
  \caption{Proof dependencies for the correctness of X25519.}
  \label{tikz:ProofHighLevel2}
\end{figure}

A brief overview of the complete proof of is described bellow.
356
357
358
359
360
361
362
363
We first pose $a = 486662$, $b = 1$, $b' = 2$, $p = 2^{255}-19$, with the equations $C = M_{a,b}$, and $T = M_{a,b'}$.
We prove the primality of $p$ and define the field $\F{p}$.
Subsquently we show that neither $2$ nor $a^2 - 2$ are square in $\F{p}$.
We consider $\F{p^2}$ and define $C(\F{p})$, $T(\F{p})$, and $C(\F{p^2})$.
We prove that for all $x \in \F{p}$ there exist a point of \xcoord $x$ either on $C(\F{p})$ or on the quadratic twist $T(\F{p})$.
We prove that all points in $M(\F{p})$ and $T(\F{p})$ can be projected in $M(\F{p^2})$ and derive that computations done in $M(\F{p})$ and $T(\F{p})$ yield to the same results if projected to $M(\F{p^2})$.
Using \tref{thm:montgomery-ladder-correct} we prove that the ladder is correct for $M(\F{p})$ and $T(\F{p})$; with the previous results, this results in the correctness of the ladder for $M(\F{p^2})$, in other words the correctness of X25519.

benoit's avatar
benoit committed
364
365
366
Now that we have an red line for the proof, we turn our attention to the details.
Indeed \tref{thm:montgomery-ladder-correct} cannot be applied directly to prove that X25519 is
doing the computations over $M(\F{p^2})$. This would infer that $\K = \F{p^2}$ and we would need to satisfy
Benoit Viguier's avatar
mods    
Benoit Viguier committed
367
368
hypothesis~\ref{hyp:a_minus_4_not_square}:%
% $a^2-4$ is not a square in \K:
Benoit Viguier's avatar
WIP    
Benoit Viguier committed
369
$$\forall x \in \K,\ x^2 \neq a^2-4.$$
benoit's avatar
benoit committed
370
371
372
which is not possible as there always exists $x \in \F{p^2}$ such that $x^2 = a^2-4$.
Consequently, we first study Curve25519 and one of its quadratic twists Twist25519,
both defined over \F{p}.
373

374
\subsubsection{Curves and twists}
Benoit Viguier's avatar
Benoit Viguier committed
375
\label{subsec:Zmodp}
376
377
378
379
380
381
382
383
384
385
386

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.
\end{lstlisting}

387
We define the basic operations ($+, -, \times$) with their respective neutral
Benoit Viguier's avatar
Benoit Viguier committed
388
elements ($0, 1$) and prove \lref{lemma:Zmodp_field}.
389
\begin{lemma}
Benoit Viguier's avatar
Benoit Viguier committed
390
  \label{lemma:Zmodp_field}
Benoit Viguier's avatar
Benoit Viguier committed
391
  $\F{p}$ is a field.
392
\end{lemma}
Freek Wiedijk's avatar
Freek Wiedijk committed
393
For $a = 486662$, by using the Legendre symbol we prove that
394
$a^2 - 4$ and $2$ are not squares in $\F{p}$.
395
\begin{lstlisting}[language=Coq,belowskip=-0.25 \baselineskip]
396
Fact a_not_square : forall x: Zmodp.type,
397
398
  x^+2 != (Zmodp.pi 486662)^+2 - 4%:R.
\end{lstlisting}
399
\begin{lstlisting}[language=Coq,label=two_not_square,belowskip=-0.1 \baselineskip]
400
Fact two_not_square : forall x: Zmodp.type,
401
402
  x^+2 != 2%:R.
\end{lstlisting}
Freek Wiedijk's avatar
Freek Wiedijk committed
403
We now consider $M_{486662,1}(\F{p})$ and $M_{486662,2}(\F{p})$, one of its quadratic twists.
Benoit Viguier's avatar
Benoit Viguier committed
404
% \begin{dfn}Let the following instantiations of \aref{alg:montgomery-double-add}:\\
Freek Wiedijk's avatar
Freek Wiedijk committed
405
\begin{dfn}
benoit's avatar
wip    
benoit committed
406
  %Let the following instantiations of \aref{alg:montgomery-ladder}:\\
benoit's avatar
benoit committed
407
408
409
410
411
  We instantiate \coqe{opt_montgomery} in two specific ways:
  \begin{itemize}
    \item[--] $Curve25519\_Fp(n,x)$ for $M_{486662,1}(\F{p})$.
    \item[--] $Twist25519\_Fp(n,x)$ for $M_{486662,2}(\F{p})$.
  \end{itemize}
412
\end{dfn}
413

414
415
With \tref{thm:montgomery-ladder-correct} we derive the following two lemmas:
\begin{lemma}
benoit's avatar
wip    
benoit committed
416
417
418
  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$.
  $$Curve25519\_Fp(n,x) = \chi_0(n \cdot P)$$
419
\end{lemma}
420
\begin{lemma}
benoit's avatar
wip    
benoit committed
421
422
423
  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$.
  $$Twist25519\_Fp(n,x) = \chi_0(n \cdot P)$$
424
\end{lemma}
425
426
427
As the Montgomery ladder does not depend on $b$, it is trivial to
see that the computations done for points in $M_{486662,1}(\F{p})$ and in
$M_{486662,2}(\F{p})$ are the same.
428
429
430
431
432
433
434
\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}
435
436
437
  \label{lemma:square-or-2square}
  For all $x$ in $\F{p}$, there exists $y$ in $\F{p}$ such that
  $$y^2 = x\ \ \ \lor\ \ 2y^2 = x$$
438
\end{lemma}
439
440
For all $x \in \F{p}$, we can compute $x^3 + ax^2 + x$. Using \lref{lemma:square-or-2square}
we can find a $y$ such that $(x,y)$ is either on the curve or on the quadratic twist:
441
\begin{lemma}
442
  \label{lemma:curve-or-twist}
Benoit Viguier's avatar
Benoit Viguier committed
443
444
  For all $x \in \F{p}$, there exists a point $P$ in $M_{486662,1}(\F{p})$ or
  in $M_{486662,2}(\F{p})$ such that the \xcoord of $P$ is $x$.
445
\end{lemma}
446
\begin{lstlisting}[language=Coq,belowskip=-0.5 \baselineskip]
Benoit Viguier's avatar
Benoit Viguier committed
447
448
Theorem x_is_on_curve_or_twist:
  forall x : Zmodp.type,
449
450
451
452
453
  (exists (p : mc curve25519_mcuType), p#x0 = x) \/
  (exists (p' : mc twist25519_mcuType), p'#x0 = x).
\end{lstlisting}

\subsubsection{Curve25519 over \F{p^2}}
454
\label{subsec:curvep2}
455

456
The quadratic extension $\F{p^2}$ is defined as $\F{p}[\sqrt{2}]$ by~\cite{Ber06}.
Freek Wiedijk's avatar
Freek Wiedijk committed
457
The theory of finite fields already has been formalized in the Mathematical Components
Freek Wiedijk's avatar
Freek Wiedijk committed
458
459
460
461
462
463
464
library,
%ref?
but this formalization is rather abstract, and we need concrete representations of field
elements here.
For this reason we decided to formalize a definition of $\F{p^2}$ ourselves.

We can represent $\F{p^2}$ as the set $\F{p} \times \F{p}$,
Benoit Viguier's avatar
Benoit Viguier committed
465
466
% in other words,
representing polynomials with coefficients in $\F{p}$ modulo $X^2 - 2$. In a similar way
Freek Wiedijk's avatar
Freek Wiedijk committed
467
as for $\F{p}$ we use a module in Coq.
468
\begin{lstlisting}[language=Coq,belowskip=-0.25 \baselineskip]
Benoit Viguier's avatar
Benoit Viguier committed
469
Module Zmodp2.
470
471
472
Inductive type :=
  Zmodp2 (x: Zmodp.type) (y:Zmodp.type).

Benoit Viguier's avatar
Benoit Viguier committed
473
Definition pi (x: Zmodp.type * Zmodp.type) : type :=
474
  Zmodp2 x.1 x.2.
Benoit Viguier's avatar
Benoit Viguier committed
475
Definition mul (x y: type) : type :=
476
477
478
  pi ((x.1 * y.1) + (2%:R * (x.2 * y.2)),
      (x.1 * y.2) + (x.2 * y.1)).
\end{lstlisting}
479
480
481
482
483
484
485
486
487
488
489
% 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).

490
491
492
493
494
495
496
We define the basic operations ($+, -, \times$) with their respective neutral
elements $0$ and $1$. Additionally we verify that for each element of in
$\F{p^2}\backslash\{0\}$, there exists a multiplicative inverse.
\begin{lemma}
  \label{lemma:Zmodp2_inv}
  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)$$
497
\end{lemma}
Benoit Viguier's avatar
Benoit Viguier committed
498
As in $\F{p}$, we define $0^{-1} = 0$ and prove \lref{lemma:Zmodp2_field}.
499
\begin{lemma}
Benoit Viguier's avatar
Benoit Viguier committed
500
501
  \label{lemma:Zmodp2_field}
  $\F{p^2}$ is a commutative field.
502
\end{lemma}
503
504
505

%% TOO LONG
%% If need remove this paragraph
Freek Wiedijk's avatar
Freek Wiedijk committed
506
We then specialize the basic operations in order to speed up the verification
507
of formulas by using rewrite rules:
508
\begin{equation*}
benoit's avatar
wip    
benoit committed
509
510
511
512
513
514
515
516
517
  \begin{split}
    (a,0) + (b,0) &= (a+b, 0)\\
    (a, 0)^{-1} &= (a^{-1}, 0)
  \end{split}
  \qquad
  \begin{split}
    (a,0) \cdot   (b,0) &= (a \cdot b, 0)\\
    (0,a)^{-1} &= (0,(2\cdot a)^{-1})
  \end{split}
518
\end{equation*}
519

520
521
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.
522

523
524
525
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
Freek Wiedijk's avatar
Freek Wiedijk committed
526
$M_{486662,2}(\F{p})$ also corresponds to a point on the curve $M_{486662,1}(\F{p^2})$.
527
528
529
As direct consequence, using \lref{lemma: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,1}(\F{p^2})$ such that $\chi_0(P) = (x,0) = x$.
530

531
\begin{lstlisting}[language=Coq,belowskip=-0.25 \baselineskip]
532
Lemma x_is_on_curve_or_twist_implies_x_in_Fp2:
533
534
535
536
537
538
  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}
benoit's avatar
benoit committed
540
541
542
543
544
545
546
547
548
  Define the functions $\varphi_c$, $\varphi_t$ and $\psi$
  \begin{itemize}
    \item[--] $\varphi_c: M_{486662,1}(\F{p}) \mapsto M_{486662,1}(\F{p^2})$\\
          such that $\varphi((x,y)) = ((x,0), (y,0))$.
    \item[--] $\varphi_t: M_{486662,2}(\F{p}) \mapsto M_{486662,1}(\F{p^2})$\\
          such that $\varphi((x,y)) = ((x,0), (0,y))$.
    \item[--] $\psi: \F{p^2} \mapsto \F{p}$\\
          such that $\psi(x,y) = x$.
  \end{itemize}
Benoit Viguier's avatar
Benoit Viguier committed
549
\end{dfn}
550
551

\begin{lemma}
552
553
554
555
  \label{lemma:proj}
  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*}
benoit's avatar
wip    
benoit committed
556
557
    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)
558
  \end{align*}
559
560
561
\end{lemma}
Notice that:
\begin{align*}
benoit's avatar
wip    
benoit committed
562
563
  \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)
564
565
\end{align*}

566
In summary for all $n \in \N,\ n < 2^{255}$, for any given point $P\in\F{p}\times\F{p}$
Benoit Viguier's avatar
Benoit Viguier committed
567
in $M_{486662,1}(\F{p})$ or $M_{486662,2}(\F{p})$, $Curve25519\_Fp$
568
computes the $\chi_0(n \cdot P)$.
569
We proved that for all $P \in \F{p^2}\times\F{p^2}$ such that $\chi_0(P) \in \F{p}$
570
there exists a corresponding point on the curve or the twist over $\F{p}$.
571
We proved that for any point, on the curve or the twist we can compute the
572
573
574
575
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}:
% No: missing uniqueness !
576
\begin{theorem}
577
578
579
580
  \label{thm:general-scalarmult}
  For all $n \in \N$, such that $n < 2^{255}$,
  for all $x \in \F{p}$ and $P \in M_{486662,1}(\F{p^2})$ such that $\chi_0(P) = x$,
  $Curve25519\_Fp(n,x)$ computes $\chi_0(n \cdot P)$.
581
\end{theorem}
582
583
584
585
586
587
588
589
590
% which is formalized in Coq as:
% \begin{lstlisting}[language=Coq,belowskip=-0.1 \baselineskip]
% Theorem curve25519_Fp2_ladder_ok:
%   forall (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
591

Benoit Viguier's avatar
Benoit Viguier committed
592
593
We then prove the equivalence between of operations in $\Ffield$ and $\Zfield$,
in other words between \coqe{Zmodp} and \coqe{:GF}.
594
This allows us to show that given a clamped value $n$ and normalized \xcoord of $P$,
Benoit Viguier's avatar
Benoit Viguier committed
595
\coqe{RFC} gives the same results as $Curve25519\_Fp$.
Freek Wiedijk's avatar
Freek Wiedijk committed
596
597
598

All put together, this finishes the proof of the mathematical correctness of X25519: the fact that the code in X25519, both in the RFC~7748 and
in TweetNaCl versions, correctly computes multiplication in the elliptic curve.