highlevel.tex 25.3 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 28 29 We first review the work of Bartzia and Strub \cite{BartziaS14} (\ref{subsec:ECC-Weierstrass}). We extend it to support Montgomery curves (\ref{subsec:ECC-Montgomery}) with homogeneous coordinates (\ref{subsec:ECC-projective}) and prove the correctness of the ladder (\ref{subsec:ECC-ladder}).  Benoit Viguier 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.  Timmy Weerwag committed Oct 02, 2020 40 41 42 43 44 The plan is as follows. 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, we prove that $M_{a,b}(\K)$ forms an abelian group. Under the hypothesis that  benoit committed Sep 28, 2020 45 46 $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 47 48 49 50 51 52 53 \begin{figure}[h] \centering \include{tikz/highlevel1} \caption{Overview of the proof of Montgomery ladder's correctness} \label{tikz:ProofHighLevel1} \end{figure}  Benoit Viguier committed Aug 12, 2019 54 \begin{dfn}  benoit committed Sep 18, 2020 55 56 57 58 59 60 61 62 63  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 64 \end{dfn}  Benoit Viguier committed Jun 21, 2019 65   Benoit Viguier committed Oct 01, 2019 66 \subsubsection{Short Weierstra{\ss} curves}  Benoit Viguier committed Aug 12, 2019 67 68 \label{subsec:ECC-Weierstrass}  Timmy Weerwag committed Oct 02, 2020 69 70 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 71   Benoit Viguier committed Aug 12, 2019 72 \begin{dfn}  benoit committed Sep 18, 2020 73  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 74  The \textit{elliptic curve} $E_{a,b}$ is defined by the equation  benoit committed Sep 18, 2020 75 76 77  $$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 78 \end{dfn}  Benoit Viguier committed Jun 21, 2019 79 80  In this setting, Bartzia and Strub defined the parametric type \texttt{ec} which  Timmy Weerwag committed Oct 02, 2020 81 82 83 represents the points on a specific curve. It is parameterized by 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 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 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}  Timmy Weerwag committed Oct 02, 2020 99 Points on an elliptic curve form an abelian group when equipped with the following structure.  Benoit Viguier committed Jun 21, 2019 100 \begin{itemize}  Timmy Weerwag committed Oct 02, 2020 101 102 103 104 105 106 107 108  \item The negation of a point $P = (x,y)$ is defined by reflection over the $x$-axis, \ie $-P = (x, -y)$. \item The addition of two points $P, Q \in E_{a,b}(\K) \setminus \{\Oinf\}$ with $P \neq Q$ and $P \neq -Q$ is defined as the negation of the third intersection point of the line through $P$ and $Q$. In case $P = Q$, we either use the line tangent to $P$ if $P$ is not an inflection point, and define $P + Q = -P = -Q$ otherwise. In case $P = -Q$, we define $P + Q = \Oinf$. \item The point $\Oinf$ acts as the neutral element. Hence, we define $-\Oinf = \Oinf$, $P + \Oinf = P$ and $\Oinf + P = P$.  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}  Benoit Viguier committed Aug 16, 2019 137 138 Speedups can be obtained by switching to homogeneous coordinates and other forms 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  Timmy Weerwag 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 Viguier committed Feb 15, 2020 180 And again we prove the result is on the curve: % (again with coercion):  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 189 190 191 192 193 194 195 196 Remarkably, of all the group properties, associativity is the hardest one to prove for elliptic curves. Instead of reproving this property for Montgomery curves, we transfer it from the Weierstra{\ss} curves with a trick. We define a bijection between a Montgomery curve and its short Weierstra{\ss} form (as in \lref{lemma:bij-ecc}) and prove that it respects the addition as defined on the respective curves. It is then easy to verify all the group laws for Montgomery curves from the Weierstra{\ss} ones. After we have verified the group properties, it follows that the bijection is a group isomorphism.  Benoit Viguier committed Jun 21, 2019 197 \begin{lemma}  benoit committed Sep 28, 2020 198  \label{lemma:bij-ecc}  Benoit Viguier committed Oct 01, 2019 199  Let $M_{a,b}$ be a Montgomery curve, define  Benoit Viguier committed Aug 17, 2019 200  $$a' = \frac{3-a^2}{3b^2} \text{\ \ \ \ and\ \ \ \ } b' = \frac{2a^3 - 9a}{27b^3}.$$  Timmy Weerwag committed Oct 02, 2020 201 202  then $E_{a',b'}$ is a Weierstra{\ss} curve, and the mapping $\varphi : M_{a,b} \to E_{a',b'}$ defined as:  Benoit Viguier committed Jun 21, 2019 203  \begin{align*}  benoit committed Sep 18, 2020 204 205  \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 206  \end{align*}  Timmy Weerwag committed Oct 02, 2020 207  is a group isomorphism between elliptic curves.  Benoit Viguier committed Jun 21, 2019 208 \end{lemma}  benoit committed Sep 28, 2020 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 % \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 224   Timmy Weerwag committed Oct 02, 2020 225 \subsubsection{Homogeneous coordinates}  Benoit Viguier committed Aug 12, 2019 226 227 \label{subsec:ECC-projective}  Timmy Weerwag committed Oct 02, 2020 228 229 In a projective plane, points are represented by the triples $(X:Y:Z)$ excluding $(0:0:0)$. Scalar multiples of triples are identified with eachother, \ie  Freek Wiedijk committed Oct 01, 2019 230 for all $\lambda \neq 0$, the triples $(X:Y:Z)$ and $(\lambda X:\lambda Y:\lambda Z)$ represent  Timmy Weerwag committed Oct 02, 2020 231 232 233 234 235 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. The points $(X : Y : 0)$ can be considered as points at infinity.  Benoit Viguier committed Aug 16, 2019 236   Benoit Viguier committed Oct 01, 2019 237 Using fractions as coordinates, the equation for a Montgomery curve $M_{a,b}$  Timmy Weerwag committed Oct 02, 2020 238 239 240 241 242 243 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 244   Benoit Viguier committed Aug 01, 2019 245 By restricting the parameter $a$ of $M_{a,b}(\K)$ such that $a^2-4$ is not a  benoit committed Sep 28, 2020 246 247 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 248 \begin{hypothesis}  benoit committed Sep 18, 2020 249  \label{hyp:a_minus_4_not_square}  Timmy Weerwag committed Oct 02, 2020 250  The number $a^2-4$ is not a square in \K.  Benoit Viguier committed Aug 17, 2019 251 \end{hypothesis}  Benoit Viguier committed Jun 21, 2019 252 \begin{lstlisting}[language=Coq]  benoit committed Sep 28, 2020 253 254 Hypothesis mcu_no_square : forall x : K, x^+2 != (M#a)^+2 - 4%:R.  Benoit Viguier committed Jun 21, 2019 255 256 \end{lstlisting}  Benoit Viguier committed Sep 27, 2019 257 We define $\chi$ and $\chi_0$ to return the \xcoord of points on a curve.  Timmy Weerwag committed Oct 02, 2020 258 259 260 261 262 263 \begin{dfn} Let $\chi : M_{a,b}(\K) \to \K \cup \{\infty\}$ and $\chi_0 : M_{a,b}(\K) \to \K$ such that \begin{align*} \chi((x,y)) &= x, & \chi(\Oinf) &= \infty, &&\text{and} \\ \chi_0((x,y)) &= x, & \chi_0(\Oinf) &= 0. \end{align*}  Benoit Viguier committed Aug 12, 2019 264 \end{dfn}  Timmy Weerwag committed Oct 02, 2020 265 266  Using homogeneous coordinates we prove the formula for differential addition.% (\lref{lemma:xADD}).  Benoit Viguier committed Jun 21, 2019 267 \begin{lemma}  benoit committed Sep 18, 2020 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282  \label{lemma:xADD} Let $M_{a,b}$ be a Montgomery curve such that $a^2-4$ is not a square in \K, and let $X_1, Z_1, X_2, Z_2, X_4, Z_4 \in \K$, such that $(X_1,Z_1) \neq (0,0)$, $(X_2,Z_2) \neq (0,0)$, $X_4 \neq 0$ and $Z_4 \neq 0$. Define \begin{align*} X_3 & = Z_4((X_1 - Z_1)(X_2+Z_2) + (X_1+Z_1)(X_2-Z_2))^2 \\ Z_3 & = X_4((X_1 - Z_1)(X_2+Z_2) - (X_1+Z_1)(X_2-Z_2))^2, \end{align*} then for any point $P_1$ and $P_2$ in $M_{a,b}(\K)$ such that $X_1/Z_1 = \chi(P_1), X_2/Z_2 = \chi(P_2)$, and $X_4/Z_4 = \chi(P_1 - P_2)$, we have $X_3/Z_3 = \chi(P_1+P_2)$.\\ \textbf{Remark:} These definitions should be understood in $\K \cup \{\infty\}$. If $x\ne 0$ then we define $x/0 = \infty$.  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 homogeneous 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 553 554 555  Define the functions $\varphi_c$, $\varphi_t$ and $\psi$ \begin{itemize} \item[--] $\varphi_c: M_{486662,1}(\F{p}) \mapsto M_{486662,1}(\F{p^2})$\\ such that $\varphi((x,y)) = ((x,0), (y,0))$. \item[--] $\varphi_t: M_{486662,2}(\F{p}) \mapsto M_{486662,1}(\F{p^2})$\\ such that $\varphi((x,y)) = ((x,0), (0,y))$. \item[--] $\psi: \F{p^2} \mapsto \F{p}$\\ such that $\psi(x,y) = x$. \end{itemize}  Benoit Viguier committed Aug 12, 2019 556 \end{dfn}  Benoit Viguier committed Jun 21, 2019 557 558  \begin{lemma}  Benoit Viguier committed Aug 17, 2019 559 560  \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 561  $M_{486662,1}(\F{p})$ (respectively on the quadratic twist $M_{486662,2}(\F{p})$), we have  Benoit Viguier committed Aug 17, 2019 562  \begin{align*}  Timmy Weerwag 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 Viguier committed Jun 21, 2019 568 \begin{align*}  Timmy Weerwag committed Oct 02, 2020 569 570  \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 571 572 \end{align*}  Timmy Weerwag committed Oct 02, 2020 573 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 574 in $M_{486662,1}(\F{p})$ or $M_{486662,2}(\F{p})$, $Curve25519\_Fp$  Timmy Weerwag committed Oct 02, 2020 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}$,  Benoit Viguier committed Aug 17, 2019 577 there exists a corresponding point on the curve or the twist over $\F{p}$.  Timmy Weerwag committed Oct 02, 2020 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  Benoit Viguier committed Aug 17, 2019 580 581 582 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 583 \begin{theorem}  Benoit Viguier committed Aug 17, 2019 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)$.  Benoit Viguier committed Jun 21, 2019 588 \end{theorem}  benoit committed Sep 28, 2020 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 committed Aug 12, 2019 598   Timmy Weerwag committed Oct 02, 2020 599 We then prove the equivalence of operations between $\Ffield$ and $\Zfield$,  Benoit Viguier committed Sep 21, 2019 600 in other words between \coqe{Zmodp} and \coqe{:GF}.  Benoit Viguier committed Sep 27, 2019 601 This allows us to show that given a clamped value $n$ and normalized \xcoord of $P$,  Benoit Viguier committed Sep 21, 2019 602 \coqe{RFC} gives the same results as $Curve25519\_Fp$.  Freek Wiedijk committed Oct 01, 2019 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.