highlevel.tex 25.3 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
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})
28
with projective coordinates (\ref{subsec:ECC-projective}) and prove the
Benoit Viguier's avatar
Benoit Viguier committed
29
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

Timmy Weerwag's avatar
Timmy Weerwag committed
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
the green tiles represent major lemmas and theorems.

benoit's avatar
minor    
benoit committed
40
41
% The plan is as follows.
% (This is part of the description of the picture).
Timmy Weerwag's avatar
Timmy Weerwag committed
42
43
We consider the field $\K$ and 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,
44
we prove that $M_{a,b}(\K)$ forms an commutative group.
Timmy Weerwag's avatar
Timmy Weerwag committed
45
Under the hypothesis that
46
47
$a^2 - 4$ is not a square in $\K$, we prove the correctness of the ladder (\tref{thm:montgomery-ladder-correct}).

48
49
50
\begin{figure}[h]
  \centering
  \include{tikz/highlevel1}
benoit's avatar
benoit committed
51
  \vspace{-0.5cm}
52
53
54
55
  \caption{Overview of the proof of Montgomery ladder's correctness}
  \label{tikz:ProofHighLevel1}
\end{figure}

benoit's avatar
minor    
benoit committed
56
57
58
% this is for the flow of the text otherwise someone will again complain of a definition poping out of nowhere.
We now turn our attention to the details of the proof of the ladder's correctness.

Benoit Viguier's avatar
Benoit Viguier committed
59
\begin{dfn}
benoit's avatar
wip    
benoit committed
60
61
62
63
64
65
66
67
68
  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
69
\end{dfn}
70

Benoit Viguier's avatar
WIP    
Benoit Viguier committed
71
\subsubsection{Short Weierstra{\ss} curves}
Benoit Viguier's avatar
Benoit Viguier committed
72
73
\label{subsec:ECC-Weierstrass}

Timmy Weerwag's avatar
Timmy Weerwag committed
74
75
For the remainder of this text, we assume that the characteristic of $\K$ is neither 2 nor 3.
Then, this equation $E(x,y)$ can be reduced into its short Weierstra{\ss} form.
76

Benoit Viguier's avatar
Benoit Viguier committed
77
\begin{dfn}
benoit's avatar
wip    
benoit committed
78
  Let $a \in \K$ and $b \in \K$ such that $$\Delta(a,b) = -16(4a^3 + 27b^2) \neq 0.$$
Timmy Weerwag's avatar
Timmy Weerwag committed
79
  The \textit{elliptic curve} $E_{a,b}$ is defined by the equation
benoit's avatar
wip    
benoit committed
80
81
82
  $$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
83
\end{dfn}
84
85

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

135
\subsubsection{Montgomery curves}
Benoit Viguier's avatar
Benoit Viguier committed
136
137
\label{subsec:ECC-Montgomery}

138
Speedups can be obtained by switching to projective coordinates and other forms
Benoit Viguier's avatar
Benoit Viguier committed
139
than the Weierstra{\ss} form. We consider the Montgomery form \cite{MontgomerySpeeding}.
140

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

185
186
187
188
Definition addmc (p1 p2 : mc) : mc :=
  MC p1 p2 (addO p1 p2)
\end{lstlisting}

Timmy Weerwag's avatar
Timmy Weerwag committed
189
We define a bijection between a Montgomery curve and its short Weierstra{\ss} form
benoit's avatar
minor    
benoit committed
190
191
(\lref{lemma:bij-ecc}) and prove that it respects the addition as defined on the
respective curves. In this way we get all the group laws for Montgomery curves from the Weierstra{\ss} ones.
Timmy Weerwag's avatar
Timmy Weerwag committed
192

benoit's avatar
minor    
benoit committed
193
After having verified the group properties, it follows that the bijection is a group isomorphism.
194
\begin{lemma}
195
  \label{lemma:bij-ecc}
Benoit Viguier's avatar
Benoit Viguier committed
196
  Let $M_{a,b}$ be a Montgomery curve, define
benoit's avatar
benoit committed
197
  \vspace{-0.3em}
198
  $$a' = \frac{3-a^2}{3b^2} \text{\ \ \ \ and\ \ \ \ } b' = \frac{2a^3 - 9a}{27b^3}.$$
benoit's avatar
minor    
benoit committed
199
200
  then $E_{a',b'}$ is a Weierstra{\ss} curve, and the mapping
  $\varphi : M_{a,b} \mapsto E_{a',b'}$ defined as:
benoit's avatar
benoit committed
201
  \vspace{-0.5em}
202
  \begin{align*}
benoit's avatar
benoit committed
203
    \varphi(\Oinf_M)   & = \Oinf_E                                                 \\[-0.5ex]
benoit's avatar
wip    
benoit committed
204
    \varphi( (x , y) ) & = \left( \frac{x}{b} + \frac{a}{3b} , \frac{y}{b} \right)
205
  \end{align*}
Timmy Weerwag's avatar
Timmy Weerwag committed
206
  is a group isomorphism between elliptic curves.
207
\end{lemma}
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
% \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}
223

224
\subsubsection{Projective coordinates}
Benoit Viguier's avatar
Benoit Viguier committed
225
226
\label{subsec:ECC-projective}

Timmy Weerwag's avatar
Timmy Weerwag committed
227
In a projective plane, points are represented by the triples $(X:Y:Z)$ excluding $(0:0:0)$.
benoit's avatar
minor    
benoit committed
228
Scalar multiples of triples are identified with each other, \ie
229
for all $\lambda \neq 0$, the triples $(X:Y:Z)$ and $(\lambda X:\lambda Y:\lambda Z)$ represent
Timmy Weerwag's avatar
Timmy Weerwag committed
230
231
232
233
the same point in the projective plane.
For $Z\neq 0$, the point $(X:Y:Z)$ corresponds to the
point $(X/Z,Y/Z)$ in the affine plane.
Likewise, the point $(X,Y)$ in the affine plane corresponds to $(X:Y:1)$ in the projective plane.
benoit's avatar
minor    
benoit committed
234
% The points $(X : Y : 0)$ can be considered as points at infinity.
Benoit Viguier's avatar
Benoit Viguier committed
235

Benoit Viguier's avatar
Benoit Viguier committed
236
Using fractions as coordinates, the equation for a Montgomery curve $M_{a,b}$
Timmy Weerwag's avatar
Timmy Weerwag committed
237
238
239
240
241
242
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).$$
Multiplying both sides by $Z^3$ yields
$$b Y^2Z = X^3 + a X^2Z + XZ^2.$$
Setting $Z = 0$ in this equation, we derive $X = 0$.
Hence, $(0 : 1 : 0)$ is the unique point on the curve at infinity.
243

Benoit Viguier's avatar
Benoit Viguier committed
244
By restricting the parameter $a$ of $M_{a,b}(\K)$ such that $a^2-4$ is not a
245
246
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$.
247
\begin{hypothesis}
benoit's avatar
wip    
benoit committed
248
  \label{hyp:a_minus_4_not_square}
Timmy Weerwag's avatar
Timmy Weerwag committed
249
  The number $a^2-4$ is not a square in \K.
250
\end{hypothesis}
251
\begin{lstlisting}[language=Coq]
252
253
Hypothesis mcu_no_square :
  forall x : K, x^+2 != (M#a)^+2 - 4%:R.
254
255
\end{lstlisting}

256
We define $\chi$ and $\chi_0$ to return the \xcoord of points on a curve.
Timmy Weerwag's avatar
Timmy Weerwag committed
257
\begin{dfn}
benoit's avatar
minor    
benoit committed
258
  Let $\chi : M_{a,b}(\K) \mapsto \K \cup \{\infty\}$ and $\chi_0 : M_{a,b}(\K) \mapsto \K$ such that
benoit's avatar
benoit committed
259
  \vspace{-0.5em}
benoit's avatar
minor    
benoit committed
260
261
262
263
  \begin{align*}
    \chi((x,y))   & = x, & \chi(\Oinf)   & = \infty, &  & \text{and} \\[-0.5ex]
    \chi_0((x,y)) & = x, & \chi_0(\Oinf) & = 0.
  \end{align*}
Benoit Viguier's avatar
Benoit Viguier committed
264
\end{dfn}
Timmy Weerwag's avatar
Timmy Weerwag committed
265

266
Using projective coordinates we prove the formula for differential addition.% (\lref{lemma:xADD}).
267
\begin{lemma}
benoit's avatar
wip    
benoit committed
268
269
270
271
272
  \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
benoit's avatar
benoit committed
273
  \vspace{-0.5em}
benoit's avatar
wip    
benoit committed
274
  \begin{align*}
benoit's avatar
minor    
benoit committed
275
276
    X_3 & = Z_4((X_1 - Z_1)(X_2+Z_2) + (X_1+Z_1)(X_2-Z_2))^2 \\[-0.5ex]
    Z_3 & = X_4((X_1 - Z_1)(X_2+Z_2) - (X_1+Z_1)(X_2-Z_2))^2
benoit's avatar
wip    
benoit committed
277
278
279
280
281
282
283
  \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$.
284
\end{lemma}
Timmy Weerwag's avatar
Timmy Weerwag committed
285
Similarly, we also prove the formula for point doubling.% (\lref{lemma:xDBL}).
286
\begin{lemma}
benoit's avatar
wip    
benoit committed
287
288
289
290
  \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*}
benoit's avatar
benoit committed
291
292
    c   & = (X_1 + Z_1)^2 - (X_1 - Z_1)^2                   \\[-0.5ex]
    X_3 & = (X_1 + Z_1)^2(X_1-Z_1)^2                        \\[-0.5ex]
benoit's avatar
wip    
benoit committed
293
294
295
296
    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)$.
297
\end{lemma}
298
299

With \lref{lemma:xADD} and \lref{lemma:xDBL}, we are able to compute efficiently
300
differential additions and point doublings using projective coordinates.
301

302
\subsubsection{Scalar multiplication algorithms}
Benoit Viguier's avatar
Benoit Viguier committed
303
\label{subsec:ECC-ladder}
304

305
306
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
307
308
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
309
% shown above.
Benoit Viguier's avatar
Benoit Viguier committed
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330

% 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
331
332

This gives us the theorem of the correctness of the Montgomery ladder.
333
\begin{theorem}
benoit's avatar
wip    
benoit committed
334
335
336
  \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)$
337
\end{theorem}
Benoit Viguier's avatar
Benoit Viguier committed
338
\begin{lstlisting}[language=Coq]
339
340
341
342
343
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
344
The definition of \coqe{opt_montgomery} is similar to \coqe{montgomery_rec_swap}
Benoit Viguier's avatar
Benoit Viguier committed
345
346
347
348
that was used in \coqe{RFC}.
We proved their equivalence, and used it in our
final proof of \coqe{Theorem RFC_Correct}.

349

350
\subsection{Curves, twists and extension fields}
Benoit Viguier's avatar
Benoit Viguier committed
351
\label{subsec:curve_twist_fields}
352

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

benoit's avatar
benoit committed
356
357
358
\begin{figure}[h]
  \centering
  \include{tikz/highlevel2}
benoit's avatar
benoit committed
359
  \vspace{-0.5cm}
benoit's avatar
benoit committed
360
361
362
363
  \caption{Proof dependencies for the correctness of X25519.}
  \label{tikz:ProofHighLevel2}
\end{figure}

Timmy Weerwag's avatar
Timmy Weerwag committed
364
A brief overview of the complete proof is described below.
365
366
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}$.
Timmy Weerwag's avatar
Timmy Weerwag committed
367
Subsequently, we show that neither $2$ nor $a^2 - 2$ are square in $\F{p}$.
368
We consider $\F{p^2}$ and define $C(\F{p})$, $T(\F{p})$, and $C(\F{p^2})$.
benoit's avatar
WIP    
benoit committed
369
We prove that for all $x \in \F{p}$ there exists a point of \xcoord $x$ either on $C(\F{p})$ or on the quadratic twist $T(\F{p})$.
370
371
372
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
373
374
375
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
376
377
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
378
$$\forall x \in \K,\ x^2 \neq a^2-4.$$
benoit's avatar
benoit committed
379
380
381
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}.
382

383
\subsubsection{Curves and twists}
Benoit Viguier's avatar
Benoit Viguier committed
384
\label{subsec:Zmodp}
385
386
387
388
389
390
391
392
393
394
395

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}

396
We define the basic operations ($+, -, \times$) with their respective neutral
Benoit Viguier's avatar
Benoit Viguier committed
397
elements ($0, 1$) and prove \lref{lemma:Zmodp_field}.
398
\begin{lemma}
Benoit Viguier's avatar
Benoit Viguier committed
399
  \label{lemma:Zmodp_field}
Benoit Viguier's avatar
Benoit Viguier committed
400
  $\F{p}$ is a field.
401
\end{lemma}
Freek Wiedijk's avatar
Freek Wiedijk committed
402
For $a = 486662$, by using the Legendre symbol we prove that
403
$a^2 - 4$ and $2$ are not squares in $\F{p}$.
404
\begin{lstlisting}[language=Coq,belowskip=-0.25 \baselineskip]
405
Fact a_not_square : forall x: Zmodp.type,
406
407
  x^+2 != (Zmodp.pi 486662)^+2 - 4%:R.
\end{lstlisting}
408
\begin{lstlisting}[language=Coq,label=two_not_square,belowskip=-0.1 \baselineskip]
409
Fact two_not_square : forall x: Zmodp.type,
410
411
  x^+2 != 2%:R.
\end{lstlisting}
Freek Wiedijk's avatar
Freek Wiedijk committed
412
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
413
% \begin{dfn}Let the following instantiations of \aref{alg:montgomery-double-add}:\\
Freek Wiedijk's avatar
Freek Wiedijk committed
414
\begin{dfn}
benoit's avatar
wip    
benoit committed
415
  %Let the following instantiations of \aref{alg:montgomery-ladder}:\\
benoit's avatar
benoit committed
416
417
418
419
420
  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}
421
\end{dfn}
422

423
424
With \tref{thm:montgomery-ladder-correct} we derive the following two lemmas:
\begin{lemma}
benoit's avatar
wip    
benoit committed
425
426
427
  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)$$
428
\end{lemma}
429
\begin{lemma}
benoit's avatar
wip    
benoit committed
430
431
432
  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)$$
433
\end{lemma}
434
435
436
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.
437
438
439
440
441
442
443
\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}
444
445
446
  \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$$
447
\end{lemma}
448
449
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:
450
\begin{lemma}
451
  \label{lemma:curve-or-twist}
Benoit Viguier's avatar
Benoit Viguier committed
452
453
  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$.
454
\end{lemma}
455
\begin{lstlisting}[language=Coq,belowskip=-0.5 \baselineskip]
Benoit Viguier's avatar
Benoit Viguier committed
456
457
Theorem x_is_on_curve_or_twist:
  forall x : Zmodp.type,
458
459
460
461
462
  (exists (p : mc curve25519_mcuType), p#x0 = x) \/
  (exists (p' : mc twist25519_mcuType), p'#x0 = x).
\end{lstlisting}

\subsubsection{Curve25519 over \F{p^2}}
463
\label{subsec:curvep2}
464

465
The quadratic extension $\F{p^2}$ is defined as $\F{p}[\sqrt{2}]$ by~\cite{Ber06}.
Freek Wiedijk's avatar
Freek Wiedijk committed
466
The theory of finite fields already has been formalized in the Mathematical Components
Freek Wiedijk's avatar
Freek Wiedijk committed
467
468
469
470
471
472
473
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
474
475
% 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
476
as for $\F{p}$ we use a module in Coq.
477
\begin{lstlisting}[language=Coq,belowskip=-0.25 \baselineskip]
Benoit Viguier's avatar
Benoit Viguier committed
478
Module Zmodp2.
479
480
481
Inductive type :=
  Zmodp2 (x: Zmodp.type) (y:Zmodp.type).

Benoit Viguier's avatar
Benoit Viguier committed
482
Definition pi (x: Zmodp.type * Zmodp.type) : type :=
483
  Zmodp2 x.1 x.2.
Benoit Viguier's avatar
Benoit Viguier committed
484
Definition mul (x y: type) : type :=
485
486
487
  pi ((x.1 * y.1) + (2%:R * (x.2 * y.2)),
      (x.1 * y.2) + (x.2 * y.1)).
\end{lstlisting}
488
489
490
491
492
493
494
495
496
497
498
% 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).

499
500
501
502
503
504
505
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)$$
506
\end{lemma}
Benoit Viguier's avatar
Benoit Viguier committed
507
As in $\F{p}$, we define $0^{-1} = 0$ and prove \lref{lemma:Zmodp2_field}.
508
\begin{lemma}
Benoit Viguier's avatar
Benoit Viguier committed
509
510
  \label{lemma:Zmodp2_field}
  $\F{p^2}$ is a commutative field.
511
\end{lemma}
512
513
514

%% TOO LONG
%% If need remove this paragraph
Freek Wiedijk's avatar
Freek Wiedijk committed
515
We then specialize the basic operations in order to speed up the verification
516
of formulas by using rewrite rules:
517
\begin{equation*}
benoit's avatar
wip    
benoit committed
518
  \begin{split}
benoit's avatar
benoit committed
519
    (a,0) + (b,0) &= (a+b, 0)\\[-0.5ex]
benoit's avatar
wip    
benoit committed
520
521
522
523
    (a, 0)^{-1} &= (a^{-1}, 0)
  \end{split}
  \qquad
  \begin{split}
benoit's avatar
benoit committed
524
    (a,0) \cdot   (b,0) &= (a \cdot b, 0)\\[-0.5ex]
benoit's avatar
wip    
benoit committed
525
526
    (0,a)^{-1} &= (0,(2\cdot a)^{-1})
  \end{split}
527
\end{equation*}
528

529
The injection $a \mapsto (a,0)$ from $\F{p}$ to $\F{p^2}$ preserves
Timmy Weerwag's avatar
Timmy Weerwag committed
530
$0, 1, +, -, \times$. Thus $(a,0)$ can be abbreviated as $a$ without confusion.
531

532
533
534
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
535
$M_{486662,2}(\F{p})$ also corresponds to a point on the curve $M_{486662,1}(\F{p^2})$.
536
537
538
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$.
539

540
\begin{lstlisting}[language=Coq,belowskip=-0.25 \baselineskip]
541
Lemma x_is_on_curve_or_twist_implies_x_in_Fp2:
542
543
544
545
546
547
  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
548
\begin{dfn}
benoit's avatar
benoit committed
549
550
551
552
553
554
  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))$.
benoit's avatar
minor    
benoit committed
555
    \item[--] $\psi: \F{p^2} \mapsto \F{p}$ such that $\psi(x,y) = x$.
benoit's avatar
benoit committed
556
  \end{itemize}
Benoit Viguier's avatar
Benoit Viguier committed
557
\end{dfn}
558
559

\begin{lemma}
560
561
  \label{lemma:proj}
  For all $n \in \N$, for all point $P\in\F{p}\times\F{p}$ on the curve
Timmy Weerwag's avatar
Timmy Weerwag committed
562
  $M_{486662,1}(\F{p})$ (respectively on the quadratic twist $M_{486662,2}(\F{p})$), we have
benoit's avatar
benoit committed
563
  \vspace{-0.3em}
564
  \begin{align*}
benoit's avatar
benoit committed
565
    P & \in M_{486662,1}(\F{p}) & \implies \varphi_c(n \cdot P) & = n \cdot \varphi_c(P), &  & \text{and} \\[-0.5ex]
benoit's avatar
minor    
benoit committed
566
    P & \in M_{486662,2}(\F{p}) & \implies \varphi_t(n \cdot P) & = n \cdot \varphi_t(P).
567
  \end{align*}
568
\end{lemma}
Timmy Weerwag's avatar
Timmy Weerwag committed
569
Notice that
benoit's avatar
benoit committed
570
\vspace{-0.5em}
571
\begin{align*}
benoit's avatar
benoit committed
572
  \forall P \in M_{486662,1}(\F{p}), &  & \psi(\chi_0(\varphi_c(P))) & = \chi_0(P), &  & \text{and} \\[-0.5ex]
benoit's avatar
minor    
benoit committed
573
  \forall P \in M_{486662,2}(\F{p}), &  & \psi(\chi_0(\varphi_t(P))) & = \chi_0(P).
574
575
\end{align*}

Timmy Weerwag's avatar
Timmy Weerwag committed
576
In summary, for all $n \in \N$, $n < 2^{255}$, for any point $P\in\F{p}\times\F{p}$
Benoit Viguier's avatar
Benoit Viguier committed
577
in $M_{486662,1}(\F{p})$ or $M_{486662,2}(\F{p})$, $Curve25519\_Fp$
Timmy Weerwag's avatar
Timmy Weerwag committed
578
579
computes $\chi_0(n \cdot P)$.
We have proved that for all $P \in \F{p^2}\times\F{p^2}$ such that $\chi_0(P) \in \F{p}$,
580
there exists a corresponding point on the curve or the twist over $\F{p}$.
Timmy Weerwag's avatar
Timmy Weerwag committed
581
582
Moreover, we have proved that for any point on the curve or the twist, we can compute the
scalar multiplication by $n$ and obtain the same result as if we did the
583
584
585
computation in $\F{p^2}$.
% As a result we have proved theorem 2.1 of \cite{Ber06}:
% No: missing uniqueness !
586
\begin{theorem}
587
588
589
590
  \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)$.
591
\end{theorem}
592
593
594
595
596
597
598
599
600
% 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
601

Timmy Weerwag's avatar
Timmy Weerwag committed
602
We then prove the equivalence of operations between $\Ffield$ and $\Zfield$,
Benoit Viguier's avatar
Benoit Viguier committed
603
in other words between \coqe{Zmodp} and \coqe{:GF}.
604
This allows us to show that given a clamped value $n$ and normalized \xcoord of $P$,
Benoit Viguier's avatar
Benoit Viguier committed
605
\coqe{RFC} gives the same results as $Curve25519\_Fp$.
Freek Wiedijk's avatar
Freek Wiedijk committed
606
607
608

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.