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 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 \begin{figure}[h] \centering \include{tikz/highlevel1}  benoit committed Jan 19, 2021 51  \vspace{-0.5cm}  Benoit Viguier committed Jan 17, 2020 52 53 54 55  \caption{Overview of the proof of Montgomery ladder's correctness} \label{tikz:ProofHighLevel1} \end{figure}  benoit committed Oct 02, 2020 56 57 58 % this is for the flow of the text otherwise someone will again complain of a definition poping out of nowhere. We now turn our attention to the details of the proof of the ladder's correctness.  Benoit Viguier committed Aug 12, 2019 59 \begin{dfn}  benoit committed Sep 18, 2020 60 61 62 63 64 65 66 67 68  Given a field $\K$, using an appropriate choice of coordinates, an elliptic curve $E$ is a plane cubic algebraic curve defined by an equation $E(x,y)$ of the form: $$E : y^2 + a_1 xy + a_3 y = x^3 + a_2 x^2 + a_4 x + a_6$$ where the $a_i$'s are in \K\ and the curve has no singular point (\ie no cusps or self-intersections). The set of points defined over \K, written $E(\K)$, is formed by the solutions $(x,y)$ of $E$ together with a distinguished point $\Oinf$ called point at infinity: $$E(\K) = \{ (x,y) \in \K \times \K ~|~E(x,y)\} \cup \{\Oinf\}$$  Benoit Viguier committed Aug 12, 2019 69 \end{dfn}  Benoit Viguier committed Jun 21, 2019 70   Benoit Viguier committed Oct 01, 2019 71 \subsubsection{Short Weierstra{\ss} curves}  Benoit Viguier committed Aug 12, 2019 72 73 \label{subsec:ECC-Weierstrass}  Timmy Weerwag committed Oct 02, 2020 74 75 For the remainder of this text, we assume that the characteristic of $\K$ is neither 2 nor 3. Then, this equation $E(x,y)$ can be reduced into its short Weierstra{\ss} form.  Benoit Viguier committed Jun 21, 2019 76   Benoit Viguier committed Aug 12, 2019 77 \begin{dfn}  benoit committed Sep 18, 2020 78  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 79  The \textit{elliptic curve} $E_{a,b}$ is defined by the equation  benoit committed Sep 18, 2020 80 81 82  $$y^2 = x^3 + ax + b.$$ $E_{a,b}(\K)$ is the set of all points $(x,y) \in \K^2$ satisfying the $E_{a,b}$ along with an additional formal point $\Oinf$, at infinity''. Such a curve does not have any singularity.  Benoit Viguier committed Aug 12, 2019 83 \end{dfn}  Benoit Viguier committed Jun 21, 2019 84 85  In this setting, Bartzia and Strub defined the parametric type \texttt{ec} which  Timmy Weerwag committed Oct 02, 2020 86 represents the points on a specific curve. It is parameterized by  benoit committed Oct 02, 2020 87 88 a \texttt{K : ecuFieldType} ---the type of fields whose characteristic is neither 2 nor 3--- and \texttt{E : ecuType} ---a record that packs the curve parameters $a$ and $b$---  Benoit Viguier committed Jun 21, 2019 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 along with the proof that $\Delta(a,b) \neq 0$. \begin{lstlisting}[language=Coq] Inductive point := EC_Inf | EC_In of K * K. Notation "(| x, y |)" := (EC_In x y). Notation "\infty" := (EC_Inf). Record ecuType := { A : K; B : K; _ : 4 * A^3 + 27 * B^2 != 0}. Definition oncurve (p : point) := if p is (| x, y |) then y^2 == x^3 + A * x + B else true. Inductive ec : Type := EC p of oncurve p. \end{lstlisting}  benoit committed Oct 02, 2020 104 Points on an elliptic curve form an abelian group when equipped with the following structure.%  Benoit Viguier committed Jun 21, 2019 105 \begin{itemize}  Timmy Weerwag committed Oct 02, 2020 106  \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 107 108 109  \item The addition of two points $P$ and $Q$ is defined as the negation of the third intersection point of the line passing through $P$ and $Q$, or tangent to $P$ if $P = Q$. \item $\Oinf$ is the neutral element under this law: if 3 points are collinear, their sum is equal to $\Oinf$  Benoit Viguier committed Jun 21, 2019 110 \end{itemize}  Freek Wiedijk committed Oct 01, 2019 111 These operations are defined in Coq as follows (where we omit the code for the tangent case):  Benoit Viguier committed Jun 21, 2019 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 \begin{lstlisting}[language=Coq] Definition neg (p : point) := if p is (| x, y |) then (| x, -y |) else EC_Inf. Definition add (p1 p2 : point) := match p1, p2 with | \infty , _ => p2 | _ , \infty => p1 | (| x1, y1 |), (| x2, y2 |) => if x1 == x2 then ... else let s := (y2 - y1) / (x2 - x1) in let xs := s^2 - x1 - x2 in (| xs, - s * (xs - x1 ) - y1 |) end. \end{lstlisting}  benoit committed Sep 18, 2020 127 The value of \texttt{add} is proven to be on the curve with coercion:  Benoit Viguier committed Jun 21, 2019 128 129 130 131 132 133 134 \begin{lstlisting}[language=Coq] Lemma addO (p q : ec): oncurve (add p q). Definition addec (p1 p2 : ec) : ec := EC p1 p2 (addO p1 p2) \end{lstlisting}  Benoit Viguier committed Sep 30, 2019 135 \subsubsection{Montgomery curves}  Benoit Viguier committed Aug 12, 2019 136 137 \label{subsec:ECC-Montgomery}  Timmy Weerwag committed Oct 02, 2020 138 Speedups can be obtained by switching to projective coordinates and other forms  Benoit Viguier committed Aug 16, 2019 139 than the Weierstra{\ss} form. We consider the Montgomery form \cite{MontgomerySpeeding}.  Benoit Viguier committed Jun 21, 2019 140   Benoit Viguier committed Aug 12, 2019 141 \begin{dfn}  Benoit Viguier committed Jul 22, 2019 142  Let $a \in \K \backslash \{-2, 2\}$, and $b \in \K \backslash \{ 0\}$.  Benoit Viguier committed Oct 01, 2019 143  The \textit{elliptic curve} $M_{a,b}$ is defined by the equation:  Benoit Viguier committed Jun 21, 2019 144  $$by^2 = x^3 + ax^2 + x,$$  Benoit Viguier committed Oct 01, 2019 145  $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 146  along with an additional formal point $\Oinf$, at infinity''.  Benoit Viguier committed Aug 12, 2019 147 \end{dfn}  Timmy Weerwag committed Oct 02, 2020 148 Similar to the definition of \texttt{ec}, we define the parametric type \texttt{mc} which  Freek Wiedijk committed Oct 01, 2019 149 150 represents the points on a specific Montgomery curve. It is parameterized by  benoit committed Oct 02, 2020 151 152 a \texttt{K : ecuFieldType} ---the type of fields whose characteristic is neither 2 nor 3--- and \texttt{M : mcuType} ---a record that packs the curve  Benoit Viguier committed Oct 01, 2019 153 parameters $a$ and $b$ along with the proofs that $b \neq 0$ and $a^2 \neq 4$.  Benoit Viguier committed Feb 06, 2020 154 \begin{lstlisting}[language=Coq,belowskip=-0.1 \baselineskip]  Benoit Viguier committed Jun 21, 2019 155 156 157 158 159 160 161 162 163 164 Record mcuType := { cA : K; cB : K; _ : cB != 0; _ : cA^2 != 4}. Definition oncurve (p : point K) := if p is (| x, y |) then cB * y^+2 == x^+3 + cA * x^+2 + x else true. Inductive mc : Type := MC p of oncurve p. Lemma oncurve_mc: forall p : mc, oncurve p. \end{lstlisting}  Benoit Viguier committed Feb 15, 2020 165 We define the addition on Montgomery curves in a similar way as for the Weierstra{\ss} form.  Benoit Viguier committed Feb 06, 2020 166 \begin{lstlisting}[language=Coq,belowskip=-0.25 \baselineskip]  Benoit Viguier committed Jun 21, 2019 167 168 169 170 171 172 173 174 175 176 177 178 179 180 Definition add (p1 p2 : point K) := match p1, p2 with | \infty, _ => p2 | _, \infty => p1 | (|x1, y1|), (|x2, y2|) => if x1 == x2 then if (y1 == y2) && (y1 != 0) then ... else \infty else let s := (y2 - y1) / (x2 - x1) in let xs := s^+2 * cB - cA - x1 - x2 in (| xs, - s * (xs - x1) - y1 |) end. \end{lstlisting}  benoit committed Oct 02, 2020 181 And again we prove the result is on the curve:  Benoit Viguier committed Jun 21, 2019 182 183 \begin{lstlisting}[language=Coq] Lemma addO (p q : mc) : oncurve (add p q).  benoit committed Sep 28, 2020 184   Benoit Viguier committed Jun 21, 2019 185 186 187 188 Definition addmc (p1 p2 : mc) : mc := MC p1 p2 (addO p1 p2) \end{lstlisting}  Timmy Weerwag committed Oct 02, 2020 189 We define a bijection between a Montgomery curve and its short Weierstra{\ss} form  benoit committed Oct 02, 2020 190 191 (\lref{lemma:bij-ecc}) and prove that it respects the addition as defined on the respective curves. In this way we get all the group laws for Montgomery curves from the Weierstra{\ss} ones.  Timmy Weerwag committed Oct 02, 2020 192   benoit committed Oct 02, 2020 193 After having verified the group properties, it follows that the bijection is a group isomorphism.  Benoit Viguier committed Jun 21, 2019 194 \begin{lemma}  benoit committed Sep 28, 2020 195  \label{lemma:bij-ecc}  Benoit Viguier committed Oct 01, 2019 196  Let $M_{a,b}$ be a Montgomery curve, define  benoit committed Jan 19, 2021 197  \vspace{-0.3em}  Benoit Viguier committed Aug 17, 2019 198  $$a' = \frac{3-a^2}{3b^2} \text{\ \ \ \ and\ \ \ \ } b' = \frac{2a^3 - 9a}{27b^3}.$$  benoit committed Oct 02, 2020 199 200  then $E_{a',b'}$ is a Weierstra{\ss} curve, and the mapping $\varphi : M_{a,b} \mapsto E_{a',b'}$ defined as:  benoit committed Jan 19, 2021 201  \vspace{-0.5em}  Benoit Viguier committed Jun 21, 2019 202  \begin{align*}  benoit committed Jan 19, 2021 203  \varphi(\Oinf_M) & = \Oinf_E \\[-0.5ex]  benoit committed Sep 18, 2020 204  \varphi( (x , y) ) & = \left( \frac{x}{b} + \frac{a}{3b} , \frac{y}{b} \right)  Benoit Viguier committed Jun 21, 2019 205  \end{align*}  Timmy Weerwag committed Oct 02, 2020 206  is a group isomorphism between elliptic curves.  Benoit Viguier committed Jun 21, 2019 207 \end{lemma}  benoit committed Sep 28, 2020 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 % \begin{lstlisting}[language=Coq,belowskip=-0.25 \baselineskip] % Definition ec_of_mc_point p := % match p with % | \infty => \infty % | (|x, y|) => (|x/(M#b) + (M#a)/(3%:R * (M#b)), y/(M#b)|) % end. % Lemma ec_of_mc_point_ok p : % oncurve M p -> % ec.oncurve E (ec_of_mc_point p). % Definition ec_of_mc p := % EC (ec_of_mc_point_ok (oncurve_mc p)). % Lemma ec_of_mc_bij : bijective ec_of_mc. % \end{lstlisting}  Benoit Viguier committed Jun 21, 2019 223   Timmy Weerwag committed Oct 02, 2020 224 \subsubsection{Projective coordinates}  Benoit Viguier committed Aug 12, 2019 225 226 \label{subsec:ECC-projective}  Timmy Weerwag committed Oct 02, 2020 227 In a projective plane, points are represented by the triples $(X:Y:Z)$ excluding $(0:0:0)$.  benoit committed Oct 02, 2020 228 Scalar multiples of triples are identified with each other, \ie  Freek Wiedijk committed Oct 01, 2019 229 for all $\lambda \neq 0$, the triples $(X:Y:Z)$ and $(\lambda X:\lambda Y:\lambda Z)$ represent  Timmy Weerwag committed Oct 02, 2020 230 231 232 233 the same point in the projective plane. For $Z\neq 0$, the point $(X:Y:Z)$ corresponds to the point $(X/Z,Y/Z)$ in the affine plane. Likewise, the point $(X,Y)$ in the affine plane corresponds to $(X:Y:1)$ in the projective plane.  benoit committed Oct 02, 2020 234 % The points $(X : Y : 0)$ can be considered as points at infinity.  Benoit Viguier committed Aug 16, 2019 235   Benoit Viguier committed Oct 01, 2019 236 Using fractions as coordinates, the equation for a Montgomery curve $M_{a,b}$  Timmy Weerwag committed Oct 02, 2020 237 238 239 240 241 242 becomes $$b \bigg(\frac{Y}{Z}\bigg)^2 = \bigg(\frac{X}{Z}\bigg)^3 + a \bigg(\frac{X}{Z}\bigg)^2 + \bigg(\frac{X}{Z}\bigg).$$ Multiplying both sides by $Z^3$ yields $$b Y^2Z = X^3 + a X^2Z + XZ^2.$$ Setting $Z = 0$ in this equation, we derive $X = 0$. Hence, $(0 : 1 : 0)$ is the unique point on the curve at infinity.  Benoit Viguier committed Jun 21, 2019 243   Benoit Viguier committed Aug 01, 2019 244 By restricting the parameter $a$ of $M_{a,b}(\K)$ such that $a^2-4$ is not a  benoit committed Sep 28, 2020 245 246 square in \K (Hypothesis \ref{hyp:a_minus_4_not_square}), we ensure that $(0,0)$ is the only point with a $y$-coordinate of $0$.  Benoit Viguier committed Aug 17, 2019 247 \begin{hypothesis}  benoit committed Sep 18, 2020 248  \label{hyp:a_minus_4_not_square}  Timmy Weerwag committed Oct 02, 2020 249  The number $a^2-4$ is not a square in \K.  Benoit Viguier committed Aug 17, 2019 250 \end{hypothesis}  Benoit Viguier committed Jun 21, 2019 251 \begin{lstlisting}[language=Coq]  benoit committed Sep 28, 2020 252 253 Hypothesis mcu_no_square : forall x : K, x^+2 != (M#a)^+2 - 4%:R.  Benoit Viguier committed Jun 21, 2019 254 255 \end{lstlisting}  Benoit Viguier committed Sep 27, 2019 256 We define $\chi$ and $\chi_0$ to return the \xcoord of points on a curve.  Timmy Weerwag committed Oct 02, 2020 257 \begin{dfn}  benoit committed Oct 02, 2020 258  Let $\chi : M_{a,b}(\K) \mapsto \K \cup \{\infty\}$ and $\chi_0 : M_{a,b}(\K) \mapsto \K$ such that  benoit committed Jan 19, 2021 259  \vspace{-0.5em}  benoit committed Oct 02, 2020 260 261 262 263  \begin{align*} \chi((x,y)) & = x, & \chi(\Oinf) & = \infty, & & \text{and} \\[-0.5ex] \chi_0((x,y)) & = x, & \chi_0(\Oinf) & = 0. \end{align*}  Benoit Viguier committed Aug 12, 2019 264 \end{dfn}  Timmy Weerwag committed Oct 02, 2020 265   Timmy Weerwag committed Oct 02, 2020 266 Using projective 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  \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 Jan 19, 2021 273  \vspace{-0.5em}  benoit committed Sep 18, 2020 274  \begin{align*}  benoit committed Oct 02, 2020 275 276  X_3 & = Z_4((X_1 - Z_1)(X_2+Z_2) + (X_1+Z_1)(X_2-Z_2))^2 \\[-0.5ex] Z_3 & = X_4((X_1 - Z_1)(X_2+Z_2) - (X_1+Z_1)(X_2-Z_2))^2  benoit committed Sep 18, 2020 277 278 279 280 281 282 283  \end{align*} then for any point $P_1$ and $P_2$ in $M_{a,b}(\K)$ such that $X_1/Z_1 = \chi(P_1), X_2/Z_2 = \chi(P_2)$, and $X_4/Z_4 = \chi(P_1 - P_2)$, we have $X_3/Z_3 = \chi(P_1+P_2)$.\\ \textbf{Remark:} These definitions should be understood in $\K \cup \{\infty\}$. If $x\ne 0$ then we define $x/0 = \infty$.  Benoit Viguier committed Jun 21, 2019 284 \end{lemma}  Timmy Weerwag committed Oct 02, 2020 285 Similarly, we also prove the formula for point doubling.% (\lref{lemma:xDBL}).  Benoit Viguier committed Jun 21, 2019 286 \begin{lemma}  benoit committed Sep 18, 2020 287 288 289 290  \label{lemma:xDBL} Let $M_{a,b}$ be a Montgomery curve such that $a^2-4$ is not a square in \K, and let $X_1, Z_1 \in \K$, such that $(X_1,Z_1) \neq (0,0)$. Define \begin{align*}  benoit committed Jan 19, 2021 291 292  c & = (X_1 + Z_1)^2 - (X_1 - Z_1)^2 \\[-0.5ex] X_3 & = (X_1 + Z_1)^2(X_1-Z_1)^2 \\[-0.5ex]  benoit committed Sep 18, 2020 293 294 295 296  Z_3 & = c\Big((X_1 + Z_1)^2+\frac{a-2}{4}\times c\Big), \end{align*} then for any point $P_1$ in $M_{a,b}(\K)$ such that $X_1/Z_1 = \chi(P_1)$, we have $X_3/Z_3 = \chi(2P_1)$.  Benoit Viguier committed Jun 21, 2019 297 \end{lemma}  Benoit Viguier committed Aug 17, 2019 298 299  With \lref{lemma:xADD} and \lref{lemma:xDBL}, we are able to compute efficiently  Timmy Weerwag committed Oct 02, 2020 300 differential additions and point doublings using projective coordinates.  Benoit Viguier committed Jun 21, 2019 301   Benoit Viguier committed Sep 30, 2019 302 \subsubsection{Scalar multiplication algorithms}  Benoit Viguier committed Aug 12, 2019 303 \label{subsec:ECC-ladder}  Benoit Viguier committed Jun 21, 2019 304   Benoit Viguier committed Feb 06, 2020 305 306 By taking \aref{alg:montgomery-ladder} and replacing \texttt{xDBL\&ADD} by a combination of the formulae from \lref{lemma:xADD} and \lref{lemma:xDBL},  Benoit Viguier committed Feb 13, 2020 307 308 we define a ladder \coqe{opt_montgomery} (in which $\K$ has not been fixed yet). % similar to the one used in TweetNaCl (with \coqe{montgomery_rec}).  benoit committed Sep 18, 2020 309 % shown above.  Benoit Viguier committed Feb 13, 2020 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330  % We prove its correctness for any point whose \xcoord is not 0. % % \begin{lstlisting}[language=Coq,belowskip=-0.25 \baselineskip] % Lemma opt_montgomery_x : % forall (n m : nat) (x : K), % n < 2^m -> x != 0 -> % forall (p : mc M), p#x0 = x -> % opt_montgomery n m x = (p *+ n)#x0. % \end{lstlisting} % We can remark that for an input $x = 0$, the ladder returns $0$. % \begin{lstlisting}[language=Coq,belowskip=-0.25 \baselineskip] % Lemma opt_montgomery_0: % forall (n m : nat), opt_montgomery n m 0 = 0. % \end{lstlisting} % Also \Oinf\ is the neutral element of $M_{a,b}(\K)$. % \begin{lstlisting}[language=Coq,belowskip=-0.25 \baselineskip] % Lemma p_x0_0_eq_0 : forall (n : nat) (p : mc M), % p #x0 = 0%:R -> (p *+ n) #x0 = 0%R. % \end{lstlisting} % This gives us the theorem of the correctness of the Montgomery ladder.  Freek Wiedijk committed Oct 01, 2019 331 332  This gives us the theorem of the correctness of the Montgomery ladder.  Benoit Viguier committed Jun 21, 2019 333 \begin{theorem}  benoit committed Sep 18, 2020 334 335 336  \label{thm:montgomery-ladder-correct} For all $n, m \in \N$, $x \in \K$, $P \in M_{a,b}(\K)$, if $\chi_0(P) = x$ then \coqe{opt_montgomery} returns $\chi_0(n \cdot P)$  Benoit Viguier committed Jun 21, 2019 337 \end{theorem}  Benoit Viguier committed Feb 13, 2020 338 \begin{lstlisting}[language=Coq]  Benoit Viguier committed Jun 21, 2019 339 340 341 342 343 Theorem opt_montgomery_ok (n m: nat) (x : K) : n < 2^m -> forall (p : mc M), p#x0 = x -> opt_montgomery n m x = (p *+ n)#x0. \end{lstlisting}  Benoit Viguier committed Feb 15, 2020 344 The definition of \coqe{opt_montgomery} is similar to \coqe{montgomery_rec_swap}  Benoit Viguier committed Feb 13, 2020 345 346 347 348 that was used in \coqe{RFC}. We proved their equivalence, and used it in our final proof of \coqe{Theorem RFC_Correct}.  Benoit Viguier committed Jun 21, 2019 349   Benoit Viguier committed Sep 30, 2019 350 \subsection{Curves, twists and extension fields}  Benoit Viguier committed Feb 12, 2020 351 \label{subsec:curve_twist_fields}  Benoit Viguier committed Jun 21, 2019 352   Benoit Viguier committed Jan 17, 2020 353 \fref{tikz:ProofHighLevel2} gives a high-level view of the proofs presented here.  benoit committed Sep 28, 2020 354 355 The white tiles are definitions while green tiles are important lemmas and theorems.  benoit committed Sep 29, 2020 356 357 358 \begin{figure}[h] \centering \include{tikz/highlevel2}  benoit committed Jan 19, 2021 359  \vspace{-0.5cm}  benoit committed Sep 29, 2020 360 361 362 363  \caption{Proof dependencies for the correctness of X25519.} \label{tikz:ProofHighLevel2} \end{figure}  Timmy Weerwag committed Oct 02, 2020 364 A brief overview of the complete proof is described below.  benoit committed Sep 28, 2020 365 366 We first pose $a = 486662$, $b = 1$, $b' = 2$, $p = 2^{255}-19$, with the equations $C = M_{a,b}$, and $T = M_{a,b'}$. We prove the primality of $p$ and define the field $\F{p}$.  Timmy Weerwag committed Oct 02, 2020 367 Subsequently, we show that neither $2$ nor $a^2 - 2$ are square in $\F{p}$.  benoit committed Sep 28, 2020 368 We consider $\F{p^2}$ and define $C(\F{p})$, $T(\F{p})$, and $C(\F{p^2})$.  benoit committed Jan 18, 2021 369 We prove that for all $x \in \F{p}$ there exists a point of \xcoord $x$ either on $C(\F{p})$ or on the quadratic twist $T(\F{p})$.  benoit committed Sep 28, 2020 370 371 372 We prove that all points in $M(\F{p})$ and $T(\F{p})$ can be projected in $M(\F{p^2})$ and derive that computations done in $M(\F{p})$ and $T(\F{p})$ yield to the same results if projected to $M(\F{p^2})$. Using \tref{thm:montgomery-ladder-correct} we prove that the ladder is correct for $M(\F{p})$ and $T(\F{p})$; with the previous results, this results in the correctness of the ladder for $M(\F{p^2})$, in other words the correctness of X25519.  benoit committed Sep 29, 2020 373 374 375 Now that we have an red line for the proof, we turn our attention to the details. Indeed \tref{thm:montgomery-ladder-correct} cannot be applied directly to prove that X25519 is doing the computations over $M(\F{p^2})$. This would infer that $\K = \F{p^2}$ and we would need to satisfy  Benoit Viguier committed Jan 21, 2020 376 377 hypothesis~\ref{hyp:a_minus_4_not_square}:% % $a^2-4$ is not a square in \K:  Benoit Viguier committed Oct 01, 2019 378 $$\forall x \in \K,\ x^2 \neq a^2-4.$$  benoit committed Sep 29, 2020 379 380 381 which is not possible as there always exists $x \in \F{p^2}$ such that $x^2 = a^2-4$. Consequently, we first study Curve25519 and one of its quadratic twists Twist25519, both defined over \F{p}.  Benoit Viguier committed Jun 21, 2019 382   Benoit Viguier committed Sep 30, 2019 383 \subsubsection{Curves and twists}  Benoit Viguier committed Sep 21, 2019 384 \label{subsec:Zmodp}  Benoit Viguier committed Jun 21, 2019 385 386 387 388 389 390 391 392 393 394 395  We define $\F{p}$ as the numbers between $0$ and $p = \p$. We create a \coqe{Zmodp} module to encapsulate those definitions. \begin{lstlisting}[language=Coq] Module Zmodp. Definition betweenb x y z := (x <=? z) && (z 0. Inductive type := Zmodp x of betweenb 0 p x. \end{lstlisting}  Benoit Viguier committed Aug 17, 2019 396 We define the basic operations ($+, -, \times$) with their respective neutral  Benoit Viguier committed Oct 01, 2019 397 elements ($0, 1$) and prove \lref{lemma:Zmodp_field}.  Benoit Viguier committed Jun 21, 2019 398 \begin{lemma}  Benoit Viguier committed Oct 01, 2019 399  \label{lemma:Zmodp_field}  Benoit Viguier committed Oct 01, 2019 400  $\F{p}$ is a field.  Benoit Viguier committed Jun 21, 2019 401 \end{lemma}  Freek Wiedijk committed Oct 01, 2019 402 For $a = 486662$, by using the Legendre symbol we prove that  Benoit Viguier committed Aug 17, 2019 403 $a^2 - 4$ and $2$ are not squares in $\F{p}$.  Benoit Viguier committed Feb 06, 2020 404 \begin{lstlisting}[language=Coq,belowskip=-0.25 \baselineskip]  Benoit Viguier committed Aug 17, 2019 405 Fact a_not_square : forall x: Zmodp.type,  Benoit Viguier committed Jun 21, 2019 406 407  x^+2 != (Zmodp.pi 486662)^+2 - 4%:R. \end{lstlisting}  Benoit Viguier committed Feb 06, 2020 408 \begin{lstlisting}[language=Coq,label=two_not_square,belowskip=-0.1 \baselineskip]  Benoit Viguier committed Aug 17, 2019 409 Fact two_not_square : forall x: Zmodp.type,  Benoit Viguier committed Jun 21, 2019 410 411  x^+2 != 2%:R. \end{lstlisting}  Freek Wiedijk committed Oct 01, 2019 412 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 413 % \begin{dfn}Let the following instantiations of \aref{alg:montgomery-double-add}:\\  Freek Wiedijk committed Oct 01, 2019 414 \begin{dfn}  benoit committed Sep 18, 2020 415  %Let the following instantiations of \aref{alg:montgomery-ladder}:\\  benoit committed Sep 29, 2020 416 417 418 419 420  We instantiate \coqe{opt_montgomery} in two specific ways: \begin{itemize} \item[--] $Curve25519\_Fp(n,x)$ for $M_{486662,1}(\F{p})$. \item[--] $Twist25519\_Fp(n,x)$ for $M_{486662,2}(\F{p})$. \end{itemize}  Benoit Viguier committed Aug 17, 2019 421 \end{dfn}  Benoit Viguier committed Jun 21, 2019 422   Benoit Viguier committed Aug 17, 2019 423 424 With \tref{thm:montgomery-ladder-correct} we derive the following two lemmas: \begin{lemma}  benoit committed Sep 18, 2020 425 426 427  For all $x \in \F{p},\ n \in \N,\ P \in \F{p} \times \F{p}$,\\ such that $P \in M_{486662,1}(\F{p})$ and $\chi_0(P) = x$. $$Curve25519\_Fp(n,x) = \chi_0(n \cdot P)$$  Benoit Viguier committed Jun 21, 2019 428 \end{lemma}  Benoit Viguier committed Aug 17, 2019 429 \begin{lemma}  benoit committed Sep 18, 2020 430 431 432  For all $x \in \F{p},\ n \in \N,\ P \in \F{p} \times \F{p}$\\ such that $P \in M_{486662,2}(\F{p})$ and $\chi_0(P) = x$. $$Twist25519\_Fp(n,x) = \chi_0(n \cdot P)$$  Benoit Viguier committed Jun 21, 2019 433 \end{lemma}  Benoit Viguier committed Aug 17, 2019 434 435 436 As the Montgomery ladder does not depend on $b$, it is trivial to see that the computations done for points in $M_{486662,1}(\F{p})$ and in $M_{486662,2}(\F{p})$ are the same.  Benoit Viguier committed Jun 21, 2019 437 438 439 440 441 442 443 \begin{lstlisting}[language=Coq] Theorem curve_twist_eq: forall n x, curve25519_Fp_ladder n x = twist25519_Fp_ladder n x. \end{lstlisting} Because $2$ is not a square in $\F{p}$, it allows us split $\F{p}$ into two sets. \begin{lemma}  Benoit Viguier committed Aug 17, 2019 444 445 446  \label{lemma:square-or-2square} For all $x$ in $\F{p}$, there exists $y$ in $\F{p}$ such that $$y^2 = x\ \ \ \lor\ \ 2y^2 = x$$  Benoit Viguier committed Jun 21, 2019 447 \end{lemma}  Benoit Viguier committed Aug 17, 2019 448 449 For all $x \in \F{p}$, we can compute $x^3 + ax^2 + x$. Using \lref{lemma:square-or-2square} we can find a $y$ such that $(x,y)$ is either on the curve or on the quadratic twist:  Benoit Viguier committed Jun 21, 2019 450 \begin{lemma}  Benoit Viguier committed Aug 17, 2019 451  \label{lemma:curve-or-twist}  Benoit Viguier committed Oct 01, 2019 452 453  For all $x \in \F{p}$, there exists a point $P$ in $M_{486662,1}(\F{p})$ or in $M_{486662,2}(\F{p})$ such that the \xcoord of $P$ is $x$.  Benoit Viguier committed Jun 21, 2019 454 \end{lemma}  Benoit Viguier committed Feb 06, 2020 455 \begin{lstlisting}[language=Coq,belowskip=-0.5 \baselineskip]  Benoit Viguier committed Sep 18, 2019 456 457 Theorem x_is_on_curve_or_twist: forall x : Zmodp.type,  Benoit Viguier committed Jun 21, 2019 458 459 460 461 462  (exists (p : mc curve25519_mcuType), p#x0 = x) \/ (exists (p' : mc twist25519_mcuType), p'#x0 = x). \end{lstlisting} \subsubsection{Curve25519 over \F{p^2}}  Benoit Viguier committed Jan 17, 2020 463 \label{subsec:curvep2}  Benoit Viguier committed Jun 21, 2019 464   Benoit Viguier committed Aug 17, 2019 465 The quadratic extension $\F{p^2}$ is defined as $\F{p}[\sqrt{2}]$ by~\cite{Ber06}.  Freek Wiedijk committed Oct 01, 2019 466 The theory of finite fields already has been formalized in the Mathematical Components  Freek Wiedijk committed Oct 01, 2019 467 468 469 470 471 472 473 library, %ref? but this formalization is rather abstract, and we need concrete representations of field elements here. For this reason we decided to formalize a definition of $\F{p^2}$ ourselves. We can represent $\F{p^2}$ as the set $\F{p} \times \F{p}$,  Benoit Viguier committed Feb 15, 2020 474 475 % in other words, representing polynomials with coefficients in $\F{p}$ modulo $X^2 - 2$. In a similar way  Freek Wiedijk committed Oct 01, 2019 476 as for $\F{p}$ we use a module in Coq.  Benoit Viguier committed Feb 06, 2020 477 \begin{lstlisting}[language=Coq,belowskip=-0.25 \baselineskip]  Benoit Viguier committed Aug 12, 2019 478 Module Zmodp2.  Benoit Viguier committed Jun 21, 2019 479 480 481 Inductive type := Zmodp2 (x: Zmodp.type) (y:Zmodp.type).  Benoit Viguier committed Sep 18, 2019 482 Definition pi (x: Zmodp.type * Zmodp.type) : type :=  Benoit Viguier committed Jun 21, 2019 483  Zmodp2 x.1 x.2.  Benoit Viguier committed Sep 18, 2019 484 Definition mul (x y: type) : type :=  Benoit Viguier committed Jun 21, 2019 485 486 487  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 488 489 490 491 492 493 494 495 496 497 498 % Definition zero : type := % pi ( 0%:R, 0%:R ). % Definition one : type := % pi ( 1, 0%:R ). % Definition opp (x: type) : type := % pi (- x.1 , - x.2). % Definition add (x y: type) : type := % pi (x.1 + y.1, x.2 + y.2). % Definition sub (x y: type) : type := % pi (x.1 - y.1, x.2 - y.2).  Benoit Viguier committed Aug 17, 2019 499 500 501 502 503 504 505 We define the basic operations ($+, -, \times$) with their respective neutral elements $0$ and $1$. Additionally we verify that for each element of in $\F{p^2}\backslash\{0\}$, there exists a multiplicative inverse. \begin{lemma} \label{lemma:Zmodp2_inv} For all $x \in \F{p^2}\backslash\{0\}$ and $a,b \in \F{p}$ such that $x = (a,b)$, $$x^{-1} = \Big(\frac{a}{a^2-2b^2}\ , \frac{-b}{a^2-2b^2}\Big)$$  Benoit Viguier committed Jun 21, 2019 506 \end{lemma}  Benoit Viguier committed Feb 15, 2020 507 As in $\F{p}$, we define $0^{-1} = 0$ and prove \lref{lemma:Zmodp2_field}.  Benoit Viguier committed Jun 21, 2019 508 \begin{lemma}  Benoit Viguier committed Oct 01, 2019 509 510  \label{lemma:Zmodp2_field} $\F{p^2}$ is a commutative field.  Benoit Viguier committed Jun 21, 2019 511 \end{lemma}  Benoit Viguier committed Sep 27, 2019 512 513 514  %% TOO LONG %% If need remove this paragraph  Freek Wiedijk committed Oct 01, 2019 515 We then specialize the basic operations in order to speed up the verification  Benoit Viguier committed Aug 17, 2019 516 of formulas by using rewrite rules:  Benoit Viguier committed Sep 30, 2019 517 \begin{equation*}  benoit committed Sep 18, 2020 518  \begin{split}  benoit committed Jan 19, 2021 519  (a,0) + (b,0) &= (a+b, 0)\\[-0.5ex]  benoit committed Sep 18, 2020 520 521 522 523  (a, 0)^{-1} &= (a^{-1}, 0) \end{split} \qquad \begin{split}  benoit committed Jan 19, 2021 524  (a,0) \cdot (b,0) &= (a \cdot b, 0)\\[-0.5ex]  benoit committed Sep 18, 2020 525 526  (0,a)^{-1} &= (0,(2\cdot a)^{-1}) \end{split}  Benoit Viguier committed Sep 30, 2019 527 \end{equation*}  Benoit Viguier committed Sep 27, 2019 528   Benoit Viguier committed Aug 17, 2019 529 The injection $a \mapsto (a,0)$ from $\F{p}$ to $\F{p^2}$ preserves  Timmy Weerwag committed Oct 02, 2020 530 $0, 1, +, -, \times$. Thus $(a,0)$ can be abbreviated as $a$ without confusion.  Benoit Viguier committed Jun 21, 2019 531   Benoit Viguier committed Aug 17, 2019 532 533 534 We define $M_{486662,1}(\F{p^2})$. With the rewrite rule above, it is straightforward to prove that any point on the curve $M_{486662,1}(\F{p})$ is also on the curve $M_{486662,1}(\F{p^2})$. Similarly, any point on the quadratic twist  Freek Wiedijk committed Oct 01, 2019 535 $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 536 537 538 As direct consequence, using \lref{lemma:curve-or-twist}, we prove that for all $x \in \F{p}$, there exists a point $P \in \F{p^2}\times\F{p^2}$ on $M_{486662,1}(\F{p^2})$ such that $\chi_0(P) = (x,0) = x$.  Benoit Viguier committed Jun 21, 2019 539   Benoit Viguier committed Feb 06, 2020 540 \begin{lstlisting}[language=Coq,belowskip=-0.25 \baselineskip]  Benoit Viguier committed Aug 17, 2019 541 Lemma x_is_on_curve_or_twist_implies_x_in_Fp2:  Benoit Viguier committed Jun 21, 2019 542 543 544 545 546 547  forall (x:Zmodp.type), exists (p: mc curve25519_Fp2_mcuType), p#x0 = Zmodp2.Zmodp2 x 0. \end{lstlisting} We now study the case of the scalar multiplication and show similar proofs.  Benoit Viguier committed Aug 12, 2019 548 \begin{dfn}  benoit committed Sep 29, 2020 549 550 551 552 553 554  Define the functions $\varphi_c$, $\varphi_t$ and $\psi$ \begin{itemize} \item[--] $\varphi_c: M_{486662,1}(\F{p}) \mapsto M_{486662,1}(\F{p^2})$\\ such that $\varphi((x,y)) = ((x,0), (y,0))$. \item[--] $\varphi_t: M_{486662,2}(\F{p}) \mapsto M_{486662,1}(\F{p^2})$\\ such that $\varphi((x,y)) = ((x,0), (0,y))$.  benoit committed Oct 02, 2020 555  \item[--] $\psi: \F{p^2} \mapsto \F{p}$ such that $\psi(x,y) = x$.  benoit committed Sep 29, 2020 556  \end{itemize}  Benoit Viguier committed Aug 12, 2019 557 \end{dfn}  Benoit Viguier committed Jun 21, 2019 558 559  \begin{lemma}  Benoit Viguier committed Aug 17, 2019 560 561  \label{lemma:proj} For all $n \in \N$, for all point $P\in\F{p}\times\F{p}$ on the curve  Timmy Weerwag committed Oct 02, 2020 562  $M_{486662,1}(\F{p})$ (respectively on the quadratic twist $M_{486662,2}(\F{p})$), we have  benoit committed Jan 19, 2021 563  \vspace{-0.3em}  Benoit Viguier committed Aug 17, 2019 564  \begin{align*}  benoit committed Jan 19, 2021 565  P & \in M_{486662,1}(\F{p}) & \implies \varphi_c(n \cdot P) & = n \cdot \varphi_c(P), & & \text{and} \\[-0.5ex]  benoit committed Oct 02, 2020 566  P & \in M_{486662,2}(\F{p}) & \implies \varphi_t(n \cdot P) & = n \cdot \varphi_t(P).  Benoit Viguier committed Aug 17, 2019 567  \end{align*}  Benoit Viguier committed Jun 21, 2019 568 \end{lemma}  Timmy Weerwag committed Oct 02, 2020 569 Notice that  benoit committed Jan 19, 2021 570 \vspace{-0.5em}  Benoit Viguier committed Jun 21, 2019 571 \begin{align*}  benoit committed Jan 19, 2021 572  \forall P \in M_{486662,1}(\F{p}), & & \psi(\chi_0(\varphi_c(P))) & = \chi_0(P), & & \text{and} \\[-0.5ex]  benoit committed Oct 02, 2020 573  \forall P \in M_{486662,2}(\F{p}), & & \psi(\chi_0(\varphi_t(P))) & = \chi_0(P).  Benoit Viguier committed Jun 21, 2019 574 575 \end{align*}  Timmy Weerwag committed Oct 02, 2020 576 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 577 in $M_{486662,1}(\F{p})$ or $M_{486662,2}(\F{p})$, $Curve25519\_Fp$  Timmy Weerwag committed Oct 02, 2020 578 579 computes $\chi_0(n \cdot P)$. We have proved that for all $P \in \F{p^2}\times\F{p^2}$ such that $\chi_0(P) \in \F{p}$,  Benoit Viguier committed Aug 17, 2019 580 there exists a corresponding point on the curve or the twist over $\F{p}$.  Timmy Weerwag committed Oct 02, 2020 581 582 Moreover, we have proved that for any point on the curve or the twist, we can compute the scalar multiplication by $n$ and obtain the same result as if we did the  Benoit Viguier committed Aug 17, 2019 583 584 585 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 586 \begin{theorem}  Benoit Viguier committed Aug 17, 2019 587 588 589 590  \label{thm:general-scalarmult} For all $n \in \N$, such that $n < 2^{255}$, for all $x \in \F{p}$ and $P \in M_{486662,1}(\F{p^2})$ such that $\chi_0(P) = x$, $Curve25519\_Fp(n,x)$ computes $\chi_0(n \cdot P)$.  Benoit Viguier committed Jun 21, 2019 591 \end{theorem}  benoit committed Sep 28, 2020 592 593 594 595 596 597 598 599 600 % which is formalized in Coq as: % \begin{lstlisting}[language=Coq,belowskip=-0.1 \baselineskip] % Theorem curve25519_Fp2_ladder_ok: % forall (n : nat) (x:Zmodp.type), % (n < 2^255)%nat -> % forall (p : mc curve25519_Fp2_mcuType), % p #x0 = Zmodp2.Zmodp2 x 0 -> % curve25519_Fp_ladder n x = (p *+ n)#x0 /p. % \end{lstlisting}  Benoit Viguier committed Aug 12, 2019 601   Timmy Weerwag committed Oct 02, 2020 602 We then prove the equivalence of operations between $\Ffield$ and $\Zfield$,  Benoit Viguier committed Sep 21, 2019 603 in other words between \coqe{Zmodp} and \coqe{:GF}.  Benoit Viguier committed Sep 27, 2019 604 This allows us to show that given a clamped value $n$ and normalized \xcoord of $P$,  Benoit Viguier committed Sep 21, 2019 605 \coqe{RFC} gives the same results as $Curve25519\_Fp$.  Freek Wiedijk committed Oct 01, 2019 606 607 608  All put together, this finishes the proof of the mathematical correctness of X25519: the fact that the code in X25519, both in the RFC~7748 and in TweetNaCl versions, correctly computes multiplication in the elliptic curve.