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}
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
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).

benoit's avatar
benoit committed
95
Record ecuType := { A : K; B : K; _: 4 * A^3 + 27 * B^2 != 0}.
96
97
98
99
100
101
102
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
103
Points on an elliptic curve form an abelian group when equipped with the following structure.%
104
\begin{itemize}
Timmy Weerwag's avatar
Timmy Weerwag committed
105
  \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
106
107
108
  \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$
109
\end{itemize}
110
These operations are defined in Coq as follows (where we omit the code for the tangent case):
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
\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
126
The value of \texttt{add} is proven to be on the curve with coercion:
127
128
129
130
131
132
133
\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}

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

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

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

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

Timmy Weerwag's avatar
Timmy Weerwag committed
187
We define a bijection between a Montgomery curve and its short Weierstra{\ss} form
benoit's avatar
minor    
benoit committed
188
189
(\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
190

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

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

Timmy Weerwag's avatar
Timmy Weerwag committed
225
In a projective plane, points are represented by the triples $(X:Y:Z)$ excluding $(0:0:0)$.
benoit's avatar
minor    
benoit committed
226
Scalar multiples of triples are identified with each other, \ie
227
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
228
229
230
231
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
232
% The points $(X : Y : 0)$ can be considered as points at infinity.
Benoit Viguier's avatar
Benoit Viguier committed
233

Benoit Viguier's avatar
Benoit Viguier committed
234
Using fractions as coordinates, the equation for a Montgomery curve $M_{a,b}$
Timmy Weerwag's avatar
Timmy Weerwag committed
235
236
237
238
239
240
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.
241

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

253
We define $\chi$ and $\chi_0$ to return the \xcoord of points on a curve.
Timmy Weerwag's avatar
Timmy Weerwag committed
254
\begin{dfn}
benoit's avatar
minor    
benoit committed
255
  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
256
  \vspace{-0.5em}
benoit's avatar
minor    
benoit committed
257
258
259
260
  \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
261
\end{dfn}
Timmy Weerwag's avatar
Timmy Weerwag committed
262

263
Using projective coordinates we prove the formula for differential addition.% (\lref{lemma:xADD}).
264
\begin{lemma}
benoit's avatar
wip    
benoit committed
265
266
267
268
269
  \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
270
  \vspace{-0.5em}
benoit's avatar
wip    
benoit committed
271
  \begin{align*}
benoit's avatar
minor    
benoit committed
272
273
    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
274
275
276
277
278
279
280
  \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$.
281
\end{lemma}
Timmy Weerwag's avatar
Timmy Weerwag committed
282
Similarly, we also prove the formula for point doubling.% (\lref{lemma:xDBL}).
283
\begin{lemma}
benoit's avatar
wip    
benoit committed
284
285
286
287
  \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
288
289
    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
290
291
292
293
    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)$.
294
\end{lemma}
295
296

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

299
\subsubsection{Scalar multiplication algorithms}
Benoit Viguier's avatar
Benoit Viguier committed
300
\label{subsec:ECC-ladder}
301

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

% 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
328
329

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

346

347
\subsection{Curves, twists and extension fields}
Benoit Viguier's avatar
Benoit Viguier committed
348
\label{subsec:curve_twist_fields}
349

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

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

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

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

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}

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

420
421
With \tref{thm:montgomery-ladder-correct} we derive the following two lemmas:
\begin{lemma}
benoit's avatar
wip    
benoit committed
422
423
424
  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)$$
425
\end{lemma}
426
\begin{lemma}
benoit's avatar
wip    
benoit committed
427
428
429
  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)$$
430
\end{lemma}
431
432
433
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.
benoit's avatar
benoit committed
434
435
436
437
% \begin{lstlisting}[language=Coq]
% Theorem curve_twist_eq: forall n x,
%   curve25519_Fp_ladder n x = twist25519_Fp_ladder n x.
% \end{lstlisting}
438
439
440

Because $2$ is not a square in $\F{p}$, it allows us split $\F{p}$ into two sets.
\begin{lemma}
441
442
443
  \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$$
444
\end{lemma}
445
446
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:
447
\begin{lemma}
448
  \label{lemma:curve-or-twist}
Benoit Viguier's avatar
Benoit Viguier committed
449
450
  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$.
451
\end{lemma}
452
\begin{lstlisting}[language=Coq,belowskip=-0.5 \baselineskip]
Benoit Viguier's avatar
Benoit Viguier committed
453
454
Theorem x_is_on_curve_or_twist:
  forall x : Zmodp.type,
455
456
457
458
459
  (exists (p : mc curve25519_mcuType), p#x0 = x) \/
  (exists (p' : mc twist25519_mcuType), p'#x0 = x).
\end{lstlisting}

\subsubsection{Curve25519 over \F{p^2}}
460
\label{subsec:curvep2}
461

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

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

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

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

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

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

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

\begin{lemma}
557
558
  \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
559
  $M_{486662,1}(\F{p})$ (respectively on the quadratic twist $M_{486662,2}(\F{p})$), we have
benoit's avatar
benoit committed
560
  \vspace{-0.3em}
561
  \begin{align*}
benoit's avatar
benoit committed
562
    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
563
    P & \in M_{486662,2}(\F{p}) & \implies \varphi_t(n \cdot P) & = n \cdot \varphi_t(P).
564
  \end{align*}
565
\end{lemma}
Timmy Weerwag's avatar
Timmy Weerwag committed
566
Notice that
benoit's avatar
benoit committed
567
\vspace{-0.5em}
568
\begin{align*}
benoit's avatar
benoit committed
569
  \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
570
  \forall P \in M_{486662,2}(\F{p}), &  & \psi(\chi_0(\varphi_t(P))) & = \chi_0(P).
571
572
\end{align*}

Timmy Weerwag's avatar
Timmy Weerwag committed
573
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
574
in $M_{486662,1}(\F{p})$ or $M_{486662,2}(\F{p})$, $Curve25519\_Fp$
Timmy Weerwag's avatar
Timmy Weerwag committed
575
576
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}$,
577
there exists a corresponding point on the curve or the twist over $\F{p}$.
Timmy Weerwag's avatar
Timmy Weerwag committed
578
579
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
580
581
582
computation in $\F{p^2}$.
% As a result we have proved theorem 2.1 of \cite{Ber06}:
% No: missing uniqueness !
583
\begin{theorem}
584
585
586
587
  \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)$.
588
\end{theorem}
589
590
591
592
593
594
595
596
597
% 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
598

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

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.