highlevel.tex 25.2 KB
 Peter Schwabe committed Jun 20, 2019 1 \section{Proving that X25519 in Coq matches the mathematical model}  Benoit Viguier committed Aug 12, 2019 2 \label{sec:maths}  Benoit Viguier committed Jun 21, 2019 3   Benoit Viguier committed Sep 20, 2019 4 In this section we prove the following informal theorem:  Benoit Viguier committed Sep 18, 2019 5 6  \begin{informaltheorem}  benoit committed Sep 18, 2020 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 committed Sep 18, 2019 10 11 \end{informaltheorem}  Benoit Viguier committed Sep 20, 2019 12 More precisely, we prove that our formalization of the RFC matches the definitions of Curve25519 by Bernstein:  Benoit Viguier committed Sep 18, 2019 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 committed Sep 19, 2019 22 23  encodeUCoordinate ((P *+ (Z.to_nat (decodeScalar25519 n))) _x0).  Benoit Viguier committed Sep 18, 2019 24 \end{lstlisting}  Benoit Viguier committed Aug 12, 2019 25   Benoit Viguier committed Aug 16, 2019 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})  Timmy Weerwag committed Oct 02, 2020 28 with projective coordinates (\ref{subsec:ECC-projective}) and prove the  Benoit Viguier committed Aug 16, 2019 29 correctness of the ladder (\ref{subsec:ECC-ladder}).  Benoit Viguier committed Feb 15, 2020 30 31 We discuss the twist of Curve25519 (\ref{subsec:Zmodp}) and explain how we deal with it in the proofs (\ref{subsec:curvep2}).  Benoit Viguier committed Jun 21, 2019 32   Timmy Weerwag committed Oct 02, 2020 33 \subsection{Formalization of elliptic curves}  Benoit Viguier committed Aug 12, 2019 34 \label{subsec:ECC}  Benoit Viguier committed Jun 21, 2019 35   Benoit Viguier committed Feb 15, 2020 36 \fref{tikz:ProofHighLevel1} presents the structure of the proof of the ladder's  benoit committed Sep 29, 2020 37 correctness. The white tiles are definitions, the orange ones are hypothesis and  benoit committed Sep 28, 2020 38 39 the green tiles represent major lemmas and theorems.  benoit committed Oct 02, 2020 40 41 % The plan is as follows. % (This is part of the description of the picture).  Timmy Weerwag committed Oct 02, 2020 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,  Timmy Weerwag committed Oct 02, 2020 44 we prove that $M_{a,b}(\K)$ forms an commutative group.  Timmy Weerwag committed Oct 02, 2020 45 Under the hypothesis that  benoit committed Sep 28, 2020 46 47 $a^2 - 4$ is not a square in $\K$, we prove the correctness of the ladder (\tref{thm:montgomery-ladder-correct}).  Benoit Viguier committed Jan 17, 2020 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 committed Oct 02, 2020 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 committed Aug 12, 2019 58 \begin{dfn}  benoit committed Sep 18, 2020 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 committed Aug 12, 2019 68 \end{dfn}  Benoit Viguier committed Jun 21, 2019 69   Benoit Viguier committed Oct 01, 2019 70 \subsubsection{Short Weierstra{\ss} curves}  Benoit Viguier committed Aug 12, 2019 71 72 \label{subsec:ECC-Weierstrass}  Timmy Weerwag committed Oct 02, 2020 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.  Benoit Viguier committed Jun 21, 2019 75   Benoit Viguier committed Aug 12, 2019 76 \begin{dfn}  benoit committed Sep 18, 2020 77  Let $a \in \K$ and $b \in \K$ such that $$\Delta(a,b) = -16(4a^3 + 27b^2) \neq 0.$$  Timmy Weerwag committed Oct 02, 2020 78  The \textit{elliptic curve} $E_{a,b}$ is defined by the equation  benoit committed Sep 18, 2020 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 committed Aug 12, 2019 82 \end{dfn}  Benoit Viguier committed Jun 21, 2019 83 84  In this setting, Bartzia and Strub defined the parametric type \texttt{ec} which  Timmy Weerwag committed Oct 02, 2020 85 represents the points on a specific curve. It is parameterized by  benoit committed Oct 02, 2020 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$---  Benoit Viguier committed Jun 21, 2019 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 committed Oct 02, 2020 103 Points on an elliptic curve form an abelian group when equipped with the following structure.%  Benoit Viguier committed Jun 21, 2019 104 \begin{itemize}  Timmy Weerwag committed Oct 02, 2020 105  \item The negation of a point $P = (x,y)$ is defined by reflection over the $x$-axis, \ie $-P = (x, -y)$.  benoit committed Oct 02, 2020 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$  Benoit Viguier committed Jun 21, 2019 109 \end{itemize}  Freek Wiedijk committed Oct 01, 2019 110 These operations are defined in Coq as follows (where we omit the code for the tangent case):  Benoit Viguier committed Jun 21, 2019 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 committed Sep 18, 2020 126 The value of \texttt{add} is proven to be on the curve with coercion:  Benoit Viguier committed Jun 21, 2019 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}  Benoit Viguier committed Sep 30, 2019 134 \subsubsection{Montgomery curves}  Benoit Viguier committed Aug 12, 2019 135 136 \label{subsec:ECC-Montgomery}  Timmy Weerwag committed Oct 02, 2020 137 Speedups can be obtained by switching to projective coordinates and other forms  Benoit Viguier committed Aug 16, 2019 138 than the Weierstra{\ss} form. We consider the Montgomery form \cite{MontgomerySpeeding}.  Benoit Viguier committed Jun 21, 2019 139   Benoit Viguier committed Aug 12, 2019 140 \begin{dfn}  Benoit Viguier committed Jul 22, 2019 141  Let $a \in \K \backslash \{-2, 2\}$, and $b \in \K \backslash \{ 0\}$.  Benoit Viguier committed Oct 01, 2019 142  The \textit{elliptic curve} $M_{a,b}$ is defined by the equation:  Benoit Viguier committed Jun 21, 2019 143  $$by^2 = x^3 + ax^2 + x,$$  Benoit Viguier committed Oct 01, 2019 144  $M_{a,b}(\K)$ is the set of all points $(x,y) \in \K^2$ satisfying the $M_{a,b}$  Benoit Viguier committed Jun 21, 2019 145  along with an additional formal point $\Oinf$, at infinity''.  Benoit Viguier committed Aug 12, 2019 146 \end{dfn}  Timmy Weerwag committed Oct 02, 2020 147 Similar to the definition of \texttt{ec}, we define the parametric type \texttt{mc} which  Freek Wiedijk committed Oct 01, 2019 148 149 represents the points on a specific Montgomery curve. It is parameterized by  benoit committed Oct 02, 2020 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 committed Oct 01, 2019 152 parameters $a$ and $b$ along with the proofs that $b \neq 0$ and $a^2 \neq 4$.  Benoit Viguier committed Feb 06, 2020 153 \begin{lstlisting}[language=Coq,belowskip=-0.1 \baselineskip]  Benoit Viguier committed Jun 21, 2019 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 committed Feb 15, 2020 164 We define the addition on Montgomery curves in a similar way as for the Weierstra{\ss} form.  Benoit Viguier committed Feb 06, 2020 165 \begin{lstlisting}[language=Coq,belowskip=-0.25 \baselineskip]  Benoit Viguier committed Jun 21, 2019 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 committed Oct 02, 2020 180 And again we prove the result is on the curve:  Benoit Viguier committed Jun 21, 2019 181 182 \begin{lstlisting}[language=Coq] Lemma addO (p q : mc) : oncurve (add p q).  benoit committed Sep 28, 2020 183   Benoit Viguier committed Jun 21, 2019 184 185 186 187 Definition addmc (p1 p2 : mc) : mc := MC p1 p2 (addO p1 p2) \end{lstlisting}  Timmy Weerwag committed Oct 02, 2020 188 We define a bijection between a Montgomery curve and its short Weierstra{\ss} form  benoit committed Oct 02, 2020 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 committed Oct 02, 2020 191   benoit committed Oct 02, 2020 192 After having verified the group properties, it follows that the bijection is a group isomorphism.  Benoit Viguier committed Jun 21, 2019 193 \begin{lemma}  benoit committed Sep 28, 2020 194  \label{lemma:bij-ecc}  Benoit Viguier committed Oct 01, 2019 195  Let $M_{a,b}$ be a Montgomery curve, define  benoit committed Oct 02, 2020 196  \vspace{-0.3em}  Benoit Viguier committed Aug 17, 2019 197  $$a' = \frac{3-a^2}{3b^2} \text{\ \ \ \ and\ \ \ \ } b' = \frac{2a^3 - 9a}{27b^3}.$$  benoit committed Oct 02, 2020 198 199 200  then $E_{a',b'}$ is a Weierstra{\ss} curve, and the mapping $\varphi : M_{a,b} \mapsto E_{a',b'}$ defined as: \vspace{-0.5em}  Benoit Viguier committed Jun 21, 2019 201  \begin{align*}  benoit committed Sep 18, 2020 202 203  \varphi(\Oinf_M) & = \Oinf_E \\ \varphi( (x , y) ) & = \left( \frac{x}{b} + \frac{a}{3b} , \frac{y}{b} \right)  Benoit Viguier committed Jun 21, 2019 204  \end{align*}  Timmy Weerwag committed Oct 02, 2020 205  is a group isomorphism between elliptic curves.  Benoit Viguier committed Jun 21, 2019 206 \end{lemma}  benoit committed Sep 28, 2020 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}  Benoit Viguier committed Jun 21, 2019 222   Timmy Weerwag committed Oct 02, 2020 223 \subsubsection{Projective coordinates}  Benoit Viguier committed Aug 12, 2019 224 225 \label{subsec:ECC-projective}  Timmy Weerwag committed Oct 02, 2020 226 In a projective plane, points are represented by the triples $(X:Y:Z)$ excluding $(0:0:0)$.  benoit committed Oct 02, 2020 227 Scalar multiples of triples are identified with each other, \ie  Freek Wiedijk committed Oct 01, 2019 228 for all $\lambda \neq 0$, the triples $(X:Y:Z)$ and $(\lambda X:\lambda Y:\lambda Z)$ represent  Timmy Weerwag committed Oct 02, 2020 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 committed Oct 02, 2020 233 % The points $(X : Y : 0)$ can be considered as points at infinity.  Benoit Viguier committed Aug 16, 2019 234   Benoit Viguier committed Oct 01, 2019 235 Using fractions as coordinates, the equation for a Montgomery curve $M_{a,b}$  Timmy Weerwag committed Oct 02, 2020 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.  Benoit Viguier committed Jun 21, 2019 242   Benoit Viguier committed Aug 01, 2019 243 By restricting the parameter $a$ of $M_{a,b}(\K)$ such that $a^2-4$ is not a  benoit committed Sep 28, 2020 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$.  Benoit Viguier committed Aug 17, 2019 246 \begin{hypothesis}  benoit committed Sep 18, 2020 247  \label{hyp:a_minus_4_not_square}  Timmy Weerwag committed Oct 02, 2020 248  The number $a^2-4$ is not a square in \K.  Benoit Viguier committed Aug 17, 2019 249 \end{hypothesis}  Benoit Viguier committed Jun 21, 2019 250 \begin{lstlisting}[language=Coq]  benoit committed Sep 28, 2020 251 252 Hypothesis mcu_no_square : forall x : K, x^+2 != (M#a)^+2 - 4%:R.  Benoit Viguier committed Jun 21, 2019 253 254 \end{lstlisting}  Benoit Viguier committed Sep 27, 2019 255 We define $\chi$ and $\chi_0$ to return the \xcoord of points on a curve.  Timmy Weerwag committed Oct 02, 2020 256 \begin{dfn}  benoit committed Oct 02, 2020 257 258 259 260 261 262  Let $\chi : M_{a,b}(\K) \mapsto \K \cup \{\infty\}$ and $\chi_0 : M_{a,b}(\K) \mapsto \K$ such that \vspace{-0.5em} \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 committed Aug 12, 2019 263 \end{dfn}  Timmy Weerwag committed Oct 02, 2020 264   Timmy Weerwag committed Oct 02, 2020 265 Using projective coordinates we prove the formula for differential addition.% (\lref{lemma:xADD}).  Benoit Viguier committed Jun 21, 2019 266 \begin{lemma}  benoit committed Sep 18, 2020 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  benoit committed Oct 02, 2020 272  \vspace{-0.5em}  benoit committed Sep 18, 2020 273  \begin{align*}  benoit committed Oct 02, 2020 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 committed Sep 18, 2020 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$.  Benoit Viguier committed Jun 21, 2019 283 \end{lemma}  Timmy Weerwag committed Oct 02, 2020 284 Similarly, we also prove the formula for point doubling.% (\lref{lemma:xDBL}).  Benoit Viguier committed Jun 21, 2019 285 \begin{lemma}  benoit committed Sep 18, 2020 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)$.  Benoit Viguier committed Jun 21, 2019 296 \end{lemma}  Benoit Viguier committed Aug 17, 2019 297 298  With \lref{lemma:xADD} and \lref{lemma:xDBL}, we are able to compute efficiently  Timmy Weerwag committed Oct 02, 2020 299 differential additions and point doublings using projective coordinates.  Benoit Viguier committed Jun 21, 2019 300   Benoit Viguier committed Sep 30, 2019 301 \subsubsection{Scalar multiplication algorithms}  Benoit Viguier committed Aug 12, 2019 302 \label{subsec:ECC-ladder}  Benoit Viguier committed Jun 21, 2019 303   Benoit Viguier committed Feb 06, 2020 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 committed Feb 13, 2020 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 committed Sep 18, 2020 308 % shown above.  Benoit Viguier committed Feb 13, 2020 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 committed Oct 01, 2019 330 331  This gives us the theorem of the correctness of the Montgomery ladder.  Benoit Viguier committed Jun 21, 2019 332 \begin{theorem}  benoit committed Sep 18, 2020 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)$  Benoit Viguier committed Jun 21, 2019 336 \end{theorem}  Benoit Viguier committed Feb 13, 2020 337 \begin{lstlisting}[language=Coq]  Benoit Viguier committed Jun 21, 2019 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 committed Feb 15, 2020 343 The definition of \coqe{opt_montgomery} is similar to \coqe{montgomery_rec_swap}  Benoit Viguier committed Feb 13, 2020 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}.  Benoit Viguier committed Jun 21, 2019 348   Benoit Viguier committed Sep 30, 2019 349 \subsection{Curves, twists and extension fields}  Benoit Viguier committed Feb 12, 2020 350 \label{subsec:curve_twist_fields}  Benoit Viguier committed Jun 21, 2019 351   Benoit Viguier committed Jan 17, 2020 352 \fref{tikz:ProofHighLevel2} gives a high-level view of the proofs presented here.  benoit committed Sep 28, 2020 353 354 The white tiles are definitions while green tiles are important lemmas and theorems.  benoit committed Sep 29, 2020 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 committed Oct 02, 2020 362 A brief overview of the complete proof is described below.  benoit committed Sep 28, 2020 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 committed Oct 02, 2020 365 Subsequently, we show that neither $2$ nor $a^2 - 2$ are square in $\F{p}$.  benoit committed Sep 28, 2020 366 367 368 369 370 We consider $\F{p^2}$ and define $C(\F{p})$, $T(\F{p})$, and $C(\F{p^2})$. We prove that for all $x \in \F{p}$ there exist a point of \xcoord $x$ either on $C(\F{p})$ or on the quadratic twist $T(\F{p})$. We prove that all points in $M(\F{p})$ and $T(\F{p})$ can be projected in $M(\F{p^2})$ and derive that computations done in $M(\F{p})$ and $T(\F{p})$ yield to the same results if projected to $M(\F{p^2})$. Using \tref{thm:montgomery-ladder-correct} we prove that the ladder is correct for $M(\F{p})$ and $T(\F{p})$; with the previous results, this results in the correctness of the ladder for $M(\F{p^2})$, in other words the correctness of X25519.  benoit committed Sep 29, 2020 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 committed Jan 21, 2020 374 375 hypothesis~\ref{hyp:a_minus_4_not_square}:% % $a^2-4$ is not a square in \K:  Benoit Viguier committed Oct 01, 2019 376 $$\forall x \in \K,\ x^2 \neq a^2-4.$$  benoit committed Sep 29, 2020 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}.  Benoit Viguier committed Jun 21, 2019 380   Benoit Viguier committed Sep 30, 2019 381 \subsubsection{Curves and twists}  Benoit Viguier committed Sep 21, 2019 382 \label{subsec:Zmodp}  Benoit Viguier committed Jun 21, 2019 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 0. Inductive type := Zmodp x of betweenb 0 p x. \end{lstlisting}  Benoit Viguier committed Aug 17, 2019 394 We define the basic operations ($+, -, \times$) with their respective neutral  Benoit Viguier committed Oct 01, 2019 395 elements ($0, 1$) and prove \lref{lemma:Zmodp_field}.  Benoit Viguier committed Jun 21, 2019 396 \begin{lemma}  Benoit Viguier committed Oct 01, 2019 397  \label{lemma:Zmodp_field}  Benoit Viguier committed Oct 01, 2019 398  $\F{p}$ is a field.  Benoit Viguier committed Jun 21, 2019 399 \end{lemma}  Freek Wiedijk committed Oct 01, 2019 400 For $a = 486662$, by using the Legendre symbol we prove that  Benoit Viguier committed Aug 17, 2019 401 $a^2 - 4$ and $2$ are not squares in $\F{p}$.  Benoit Viguier committed Feb 06, 2020 402 \begin{lstlisting}[language=Coq,belowskip=-0.25 \baselineskip]  Benoit Viguier committed Aug 17, 2019 403 Fact a_not_square : forall x: Zmodp.type,  Benoit Viguier committed Jun 21, 2019 404 405  x^+2 != (Zmodp.pi 486662)^+2 - 4%:R. \end{lstlisting}  Benoit Viguier committed Feb 06, 2020 406 \begin{lstlisting}[language=Coq,label=two_not_square,belowskip=-0.1 \baselineskip]  Benoit Viguier committed Aug 17, 2019 407 Fact two_not_square : forall x: Zmodp.type,  Benoit Viguier committed Jun 21, 2019 408 409  x^+2 != 2%:R. \end{lstlisting}  Freek Wiedijk committed Oct 01, 2019 410 We now consider $M_{486662,1}(\F{p})$ and $M_{486662,2}(\F{p})$, one of its quadratic twists.  Benoit Viguier committed Sep 30, 2019 411 % \begin{dfn}Let the following instantiations of \aref{alg:montgomery-double-add}:\\  Freek Wiedijk committed Oct 01, 2019 412 \begin{dfn}  benoit committed Sep 18, 2020 413  %Let the following instantiations of \aref{alg:montgomery-ladder}:\\  benoit committed Sep 29, 2020 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}  Benoit Viguier committed Aug 17, 2019 419 \end{dfn}  Benoit Viguier committed Jun 21, 2019 420   Benoit Viguier committed Aug 17, 2019 421 422 With \tref{thm:montgomery-ladder-correct} we derive the following two lemmas: \begin{lemma}  benoit committed Sep 18, 2020 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)$$  Benoit Viguier committed Jun 21, 2019 426 \end{lemma}  Benoit Viguier committed Aug 17, 2019 427 \begin{lemma}  benoit committed Sep 18, 2020 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)$$  Benoit Viguier committed Jun 21, 2019 431 \end{lemma}  Benoit Viguier committed Aug 17, 2019 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.  Benoit Viguier committed Jun 21, 2019 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}  Benoit Viguier committed Aug 17, 2019 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$$  Benoit Viguier committed Jun 21, 2019 445 \end{lemma}  Benoit Viguier committed Aug 17, 2019 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:  Benoit Viguier committed Jun 21, 2019 448 \begin{lemma}  Benoit Viguier committed Aug 17, 2019 449  \label{lemma:curve-or-twist}  Benoit Viguier committed Oct 01, 2019 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$.  Benoit Viguier committed Jun 21, 2019 452 \end{lemma}  Benoit Viguier committed Feb 06, 2020 453 \begin{lstlisting}[language=Coq,belowskip=-0.5 \baselineskip]  Benoit Viguier committed Sep 18, 2019 454 455 Theorem x_is_on_curve_or_twist: forall x : Zmodp.type,  Benoit Viguier committed Jun 21, 2019 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}}  Benoit Viguier committed Jan 17, 2020 461 \label{subsec:curvep2}  Benoit Viguier committed Jun 21, 2019 462   Benoit Viguier committed Aug 17, 2019 463 The quadratic extension $\F{p^2}$ is defined as $\F{p}[\sqrt{2}]$ by~\cite{Ber06}.  Freek Wiedijk committed Oct 01, 2019 464 The theory of finite fields already has been formalized in the Mathematical Components  Freek Wiedijk committed Oct 01, 2019 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 committed Feb 15, 2020 472 473 % in other words, representing polynomials with coefficients in $\F{p}$ modulo $X^2 - 2$. In a similar way  Freek Wiedijk committed Oct 01, 2019 474 as for $\F{p}$ we use a module in Coq.  Benoit Viguier committed Feb 06, 2020 475 \begin{lstlisting}[language=Coq,belowskip=-0.25 \baselineskip]  Benoit Viguier committed Aug 12, 2019 476 Module Zmodp2.  Benoit Viguier committed Jun 21, 2019 477 478 479 Inductive type := Zmodp2 (x: Zmodp.type) (y:Zmodp.type).  Benoit Viguier committed Sep 18, 2019 480 Definition pi (x: Zmodp.type * Zmodp.type) : type :=  Benoit Viguier committed Jun 21, 2019 481  Zmodp2 x.1 x.2.  Benoit Viguier committed Sep 18, 2019 482 Definition mul (x y: type) : type :=  Benoit Viguier committed Jun 21, 2019 483 484 485  pi ((x.1 * y.1) + (2%:R * (x.2 * y.2)), (x.1 * y.2) + (x.2 * y.1)). \end{lstlisting}  Benoit Viguier committed Sep 30, 2019 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).  Benoit Viguier committed Aug 17, 2019 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)$$  Benoit Viguier committed Jun 21, 2019 504 \end{lemma}  Benoit Viguier committed Feb 15, 2020 505 As in $\F{p}$, we define $0^{-1} = 0$ and prove \lref{lemma:Zmodp2_field}.  Benoit Viguier committed Jun 21, 2019 506 \begin{lemma}  Benoit Viguier committed Oct 01, 2019 507 508  \label{lemma:Zmodp2_field} $\F{p^2}$ is a commutative field.  Benoit Viguier committed Jun 21, 2019 509 \end{lemma}  Benoit Viguier committed Sep 27, 2019 510 511 512  %% TOO LONG %% If need remove this paragraph  Freek Wiedijk committed Oct 01, 2019 513 We then specialize the basic operations in order to speed up the verification  Benoit Viguier committed Aug 17, 2019 514 of formulas by using rewrite rules:  Benoit Viguier committed Sep 30, 2019 515 \begin{equation*}  benoit committed Sep 18, 2020 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}  Benoit Viguier committed Sep 30, 2019 525 \end{equation*}  Benoit Viguier committed Sep 27, 2019 526   Benoit Viguier committed Aug 17, 2019 527 The injection $a \mapsto (a,0)$ from $\F{p}$ to $\F{p^2}$ preserves  Timmy Weerwag committed Oct 02, 2020 528 $0, 1, +, -, \times$. Thus $(a,0)$ can be abbreviated as $a$ without confusion.  Benoit Viguier committed Jun 21, 2019 529   Benoit Viguier committed Aug 17, 2019 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 committed Oct 01, 2019 533 $M_{486662,2}(\F{p})$ also corresponds to a point on the curve $M_{486662,1}(\F{p^2})$.  Benoit Viguier committed Aug 17, 2019 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$.  Benoit Viguier committed Jun 21, 2019 537   Benoit Viguier committed Feb 06, 2020 538 \begin{lstlisting}[language=Coq,belowskip=-0.25 \baselineskip]  Benoit Viguier committed Aug 17, 2019 539 Lemma x_is_on_curve_or_twist_implies_x_in_Fp2:  Benoit Viguier committed Jun 21, 2019 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 committed Aug 12, 2019 546 \begin{dfn}  benoit committed Sep 29, 2020 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 committed Oct 02, 2020 553  \item[--] $\psi: \F{p^2} \mapsto \F{p}$ such that $\psi(x,y) = x$.  benoit committed Sep 29, 2020 554  \end{itemize}  Benoit Viguier committed Aug 12, 2019 555 \end{dfn}  Benoit Viguier committed Jun 21, 2019 556 557  \begin{lemma}  Benoit Viguier committed Aug 17, 2019 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 committed Oct 02, 2020 560  $M_{486662,1}(\F{p})$ (respectively on the quadratic twist $M_{486662,2}(\F{p})$), we have  benoit committed Oct 02, 2020 561  \vspace{-0.3em}  Benoit Viguier committed Aug 17, 2019 562  \begin{align*}  benoit committed Oct 02, 2020 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).  Benoit Viguier committed Aug 17, 2019 565  \end{align*}  Benoit Viguier committed Jun 21, 2019 566 \end{lemma}  Timmy Weerwag committed Oct 02, 2020 567 Notice that  benoit committed Oct 02, 2020 568 \vspace{-0.5em}  Benoit Viguier committed Jun 21, 2019 569 \begin{align*}  benoit committed Oct 02, 2020 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).  Benoit Viguier committed Jun 21, 2019 572 573 \end{align*}  Timmy Weerwag committed Oct 02, 2020 574 In summary, for all $n \in \N$, $n < 2^{255}$, for any point $P\in\F{p}\times\F{p}$  Benoit Viguier committed Oct 01, 2019 575 in $M_{486662,1}(\F{p})$ or $M_{486662,2}(\F{p})$, $Curve25519\_Fp$  Timmy Weerwag committed Oct 02, 2020 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}$,  Benoit Viguier committed Aug 17, 2019 578 there exists a corresponding point on the curve or the twist over $\F{p}$.  Timmy Weerwag committed Oct 02, 2020 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  Benoit Viguier committed Aug 17, 2019 581 582 583 computation in $\F{p^2}$. % As a result we have proved theorem 2.1 of \cite{Ber06}: % No: missing uniqueness !  Benoit Viguier committed Jun 21, 2019 584 \begin{theorem}  Benoit Viguier committed Aug 17, 2019 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)$.  Benoit Viguier committed Jun 21, 2019 589 \end{theorem}  benoit committed Sep 28, 2020 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 committed Aug 12, 2019 599   Timmy Weerwag committed Oct 02, 2020 600 We then prove the equivalence of operations between $\Ffield$ and $\Zfield$,  Benoit Viguier committed Sep 21, 2019 601 in other words between \coqe{Zmodp} and \coqe{:GF}.  Benoit Viguier committed Sep 27, 2019 602 This allows us to show that given a clamped value $n$ and normalized \xcoord of $P$,  Benoit Viguier committed Sep 21, 2019 603 \coqe{RFC} gives the same results as $Curve25519\_Fp$.  Freek Wiedijk committed Oct 01, 2019 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.