highlevel.tex 25.2 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
51
52
53
54
\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
minor    
benoit committed
55
56
57
% 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
58
\begin{dfn}
benoit's avatar
wip    
benoit committed
59
60
61
62
63
64
65
66
67
  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
68
\end{dfn}
69

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

Timmy Weerwag's avatar
Timmy Weerwag committed
73
74
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.
75

Benoit Viguier's avatar
Benoit Viguier committed
76
\begin{dfn}
benoit's avatar
wip    
benoit committed
77
  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
78
  The \textit{elliptic curve} $E_{a,b}$ is defined by the equation
benoit's avatar
wip    
benoit committed
79
80
81
  $$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
82
\end{dfn}
83
84

In this setting, Bartzia and Strub defined the parametric type \texttt{ec} which
Timmy Weerwag's avatar
Timmy Weerwag committed
85
represents the points on a specific curve. It is parameterized by
benoit's avatar
minor    
benoit committed
86
87
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$---
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
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
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]
154
155
156
157
158
159
160
161
162
163
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
164
We define the addition on Montgomery curves in a similar way as for the Weierstra{\ss} form.
165
\begin{lstlisting}[language=Coq,belowskip=-0.25 \baselineskip]
166
167
168
169
170
171
172
173
174
175
176
177
178
179
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
180
And again we prove the result is on the curve:
181
182
\begin{lstlisting}[language=Coq]
Lemma addO (p q : mc) : oncurve (add p q).
183

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

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

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

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

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

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

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

255
We define $\chi$ and $\chi_0$ to return the \xcoord of points on a curve.
Timmy Weerwag's avatar
Timmy Weerwag committed
256
\begin{dfn}
benoit's avatar
minor    
benoit committed
257
  Let $\chi : M_{a,b}(\K) \mapsto \K \cup \{\infty\}$ and $\chi_0 : M_{a,b}(\K) \mapsto \K$ such that
258
  %\vspace{-0.5em}
benoit's avatar
minor    
benoit committed
259
260
261
262
  \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
263
\end{dfn}
Timmy Weerwag's avatar
Timmy Weerwag committed
264

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

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

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

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

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

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

348

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

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

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

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

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

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}

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

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

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

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

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

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

%% TOO LONG
%% If need remove this paragraph
Freek Wiedijk's avatar
Freek Wiedijk committed
513
We then specialize the basic operations in order to speed up the verification
514
of formulas by using rewrite rules:
515
\begin{equation*}
benoit's avatar
wip    
benoit committed
516
517
518
519
520
521
522
523
524
  \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}
525
\end{equation*}
526

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

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

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

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

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

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

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.