highlevel.tex 24.7 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   Benoit Viguier committed Sep 30, 2019 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 40 41 42 43 44 45 46 the green tiles represent major lemmas and theorems. We consider elliptic curves over a field $\K$. We assume that the characteristic of $\K$ is neither 2 or 3. We 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 associative finite group. Under the hypothesis that $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 committed Sep 29, 2020 54 We now turn our attention to the details of the proof of the ladder's correctness.  Benoit Viguier committed Jun 21, 2019 55   Benoit Viguier committed Aug 12, 2019 56 \begin{dfn}  benoit committed Sep 18, 2020 57 58 59 60 61 62 63 64 65  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 66 \end{dfn}  Benoit Viguier committed Jun 21, 2019 67   Benoit Viguier committed Oct 01, 2019 68 \subsubsection{Short Weierstra{\ss} curves}  Benoit Viguier committed Aug 12, 2019 69 70 \label{subsec:ECC-Weierstrass}  Benoit Viguier committed Jul 22, 2019 71 This equation $E(x,y)$ can be reduced into its short Weierstra{\ss} form.  Benoit Viguier committed Jun 21, 2019 72   Benoit Viguier committed Aug 12, 2019 73 \begin{dfn}  benoit committed Sep 18, 2020 74 75 76 77 78  Let $a \in \K$ and $b \in \K$ such that $$\Delta(a,b) = -16(4a^3 + 27b^2) \neq 0.$$ The \textit{elliptic curve} $E_{a,b}$ is defined by the equation: $$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 79 \end{dfn}  Benoit Viguier committed Jun 21, 2019 80 81  In this setting, Bartzia and Strub defined the parametric type \texttt{ec} which  Benoit Viguier committed Aug 01, 2019 82 represent the points on a specific curve. It is parameterized by  benoit committed Sep 18, 2020 83 a \texttt{K : ecuFieldType} --- the type of fields whose characteristic is not 2 or 3 ---  Benoit Viguier committed Oct 01, 2019 84 and \texttt{E : ecuType} --- a record that packs the curve parameters $a$ and $b$  Benoit Viguier committed Jun 21, 2019 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 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 Viguier committed Oct 01, 2019 100 Points on an elliptic curve are equipped with the structure of an abelian group.  Benoit Viguier committed Jun 21, 2019 101 \begin{itemize}  Benoit Viguier committed Oct 01, 2019 102  \item The negation of a point $P = (x,y)$ is defined by reflection over the $x$ axis $-P = (x, -y)$.  Freek Wiedijk committed Oct 01, 2019 103  \item The addition of two points $P$ and $Q$ is defined as the negation of the third intersection point  benoit committed Sep 18, 2020 104  of the line passing through $P$ and $Q$, or tangent to $P$ if $P = Q$.  Benoit Viguier committed Aug 01, 2019 105  \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 106 \end{itemize}  Freek Wiedijk committed Oct 01, 2019 107 These operations are defined in Coq as follows (where we omit the code for the tangent case):  Benoit Viguier committed Jun 21, 2019 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 \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 123 The value of \texttt{add} is proven to be on the curve with coercion:  Benoit Viguier committed Jun 21, 2019 124 125 126 127 128 129 130 \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 131 \subsubsection{Montgomery curves}  Benoit Viguier committed Aug 12, 2019 132 133 \label{subsec:ECC-Montgomery}  Benoit Viguier committed Aug 16, 2019 134 135 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 136   Benoit Viguier committed Aug 12, 2019 137 \begin{dfn}  Benoit Viguier committed Jul 22, 2019 138  Let $a \in \K \backslash \{-2, 2\}$, and $b \in \K \backslash \{ 0\}$.  Benoit Viguier committed Oct 01, 2019 139  The \textit{elliptic curve} $M_{a,b}$ is defined by the equation:  Benoit Viguier committed Jun 21, 2019 140  $$by^2 = x^3 + ax^2 + x,$$  Benoit Viguier committed Oct 01, 2019 141  $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 142  along with an additional formal point $\Oinf$, at infinity''.  Benoit Viguier committed Aug 12, 2019 143 \end{dfn}  Freek Wiedijk committed Oct 01, 2019 144 145 146 Similar to the definition of \texttt{ec}, we defined the parametric type \texttt{mc} which represents the points on a specific Montgomery curve. It is parameterized by  benoit committed Sep 18, 2020 147 a \texttt{K : ecuFieldType} --- the type of fields whose characteristic is not  Benoit Viguier committed Oct 01, 2019 148 149 2 or 3 --- and \texttt{M : mcuType} --- a record that packs the curve parameters $a$ and $b$ along with the proofs that $b \neq 0$ and $a^2 \neq 4$.  Benoit Viguier committed Feb 06, 2020 150 \begin{lstlisting}[language=Coq,belowskip=-0.1 \baselineskip]  Benoit Viguier committed Jun 21, 2019 151 152 153 154 155 156 157 158 159 160 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 161 We define the addition on Montgomery curves in a similar way as for the Weierstra{\ss} form.  Benoit Viguier committed Feb 06, 2020 162 \begin{lstlisting}[language=Coq,belowskip=-0.25 \baselineskip]  Benoit Viguier committed Jun 21, 2019 163 164 165 166 167 168 169 170 171 172 173 174 175 176 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 177 And again we prove the result is on the curve: % (again with coercion):  Benoit Viguier committed Jun 21, 2019 178 179 \begin{lstlisting}[language=Coq] Lemma addO (p q : mc) : oncurve (add p q).  benoit committed Sep 28, 2020 180   Benoit Viguier committed Jun 21, 2019 181 182 183 184 Definition addmc (p1 p2 : mc) : mc := MC p1 p2 (addO p1 p2) \end{lstlisting}  benoit committed Sep 28, 2020 185 186 We then define a bijection between a Montgomery curve and its short Weierstra{\ss} form (\lref{lemma:bij-ecc}).  Freek Wiedijk committed Oct 01, 2019 187 188 In this way we get associativity of addition on Montgomery curves from the corresponding property for Weierstra{\ss} curves.  Benoit Viguier committed Jun 21, 2019 189 \begin{lemma}  benoit committed Sep 28, 2020 190  \label{lemma:bij-ecc}  Benoit Viguier committed Oct 01, 2019 191  Let $M_{a,b}$ be a Montgomery curve, define  Benoit Viguier committed Aug 17, 2019 192  $$a' = \frac{3-a^2}{3b^2} \text{\ \ \ \ and\ \ \ \ } b' = \frac{2a^3 - 9a}{27b^3}.$$  Benoit Viguier committed Oct 01, 2019 193 194  then $E_{a',b'}$ is an elliptic curve, and the mapping $\varphi : M_{a,b} \mapsto E_{a',b'}$ defined as:  Benoit Viguier committed Jun 21, 2019 195  \begin{align*}  benoit committed Sep 18, 2020 196 197  \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 198  \end{align*}  Benoit Viguier committed Oct 01, 2019 199  is an isomorphism between elliptic curves.  Benoit Viguier committed Jun 21, 2019 200 \end{lemma}  benoit committed Sep 28, 2020 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 % \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 216   Benoit Viguier committed Sep 30, 2019 217 \subsubsection{Projective coordinates}  Benoit Viguier committed Aug 12, 2019 218 219 \label{subsec:ECC-projective}  Freek Wiedijk committed Oct 01, 2019 220 221 In a projective plane, points are represented with triples $(X:Y:Z)$, with the exception of $(0:0:0)$.  Benoit Viguier committed Aug 16, 2019 222 Scalar multiples are representing the same point, \ie  Freek Wiedijk committed Oct 01, 2019 223 for all $\lambda \neq 0$, the triples $(X:Y:Z)$ and $(\lambda X:\lambda Y:\lambda Z)$ represent  Benoit Viguier committed Aug 16, 2019 224 225 the same point. For $Z\neq 0$, the projective point $(X:Y:Z)$ corresponds to the  Benoit Viguier committed Oct 01, 2019 226 227 point $(X/Z,Y/Z)$ on the affine plane. Likewise the point $(X,Y)$ on the affine plane corresponds to $(X:Y:1)$ on the projective plane.  Benoit Viguier committed Aug 16, 2019 228   Benoit Viguier committed Oct 01, 2019 229 Using fractions as coordinates, the equation for a Montgomery curve $M_{a,b}$  Benoit Viguier committed Aug 16, 2019 230 231 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)$$  Benoit Viguier committed Jun 21, 2019 232 Multiplying both sides by $Z^3$ yields:  Benoit Viguier committed Aug 16, 2019 233 $$b Y^2Z = X^3 + a X^2Z + XZ^2$$  Benoit Viguier committed Jul 22, 2019 234 With this equation we can additionally represent the point at infinity''. By  Benoit Viguier committed Oct 01, 2019 235 setting $Z=0$, we derive $X=0$, giving us the infinite point'' $(0:1:0)$.  Benoit Viguier committed Jun 21, 2019 236   Benoit Viguier committed Aug 01, 2019 237 By restricting the parameter $a$ of $M_{a,b}(\K)$ such that $a^2-4$ is not a  benoit committed Sep 28, 2020 238 239 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 240 \begin{hypothesis}  benoit committed Sep 18, 2020 241 242  \label{hyp:a_minus_4_not_square} $a^2-4$ is not a square in \K.  Benoit Viguier committed Aug 17, 2019 243 \end{hypothesis}  Benoit Viguier committed Jun 21, 2019 244 \begin{lstlisting}[language=Coq]  benoit committed Sep 28, 2020 245 246 Hypothesis mcu_no_square : forall x : K, x^+2 != (M#a)^+2 - 4%:R.  Benoit Viguier committed Jun 21, 2019 247 248 \end{lstlisting}  Benoit Viguier committed Sep 27, 2019 249 We define $\chi$ and $\chi_0$ to return the \xcoord of points on a curve.  Benoit Viguier committed Aug 16, 2019 250 \begin{dfn}Let $\chi$ and $\chi_0$:\\  benoit committed Sep 28, 2020 251 252 253 254 255 256 257  \vspace{-1em} \begin{itemize} \item[--] $\chi : M_{a,b}(\K) \to \K \cup \{\infty\}$\\ such that $\chi(\Oinf) = \infty$ and $\chi((x,y)) = x$. \item[--] $\chi_0 : M_{a,b}(\K) \to \K$\\ such that $\chi_0(\Oinf) = 0$ and $\chi_0((x,y)) = x$. \end{itemize}  Benoit Viguier committed Aug 12, 2019 258 \end{dfn}  Benoit Viguier committed Feb 15, 2020 259 Using projective coordinates we prove the formula for differential addition.% (\lref{lemma:xADD}).  Benoit Viguier committed Jun 21, 2019 260 \begin{lemma}  benoit committed Sep 18, 2020 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275  \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 276 \end{lemma}  Benoit Viguier committed Feb 15, 2020 277 Similarly we also prove the formula for point doubling.% (\lref{lemma:xDBL}).  Benoit Viguier committed Jun 21, 2019 278 \begin{lemma}  benoit committed Sep 18, 2020 279 280 281 282 283 284 285 286 287 288  \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 289 \end{lemma}  Benoit Viguier committed Aug 17, 2019 290 291  With \lref{lemma:xADD} and \lref{lemma:xDBL}, we are able to compute efficiently  Freek Wiedijk committed Oct 01, 2019 292 differential additions and point doublings using projective coordinates.  Benoit Viguier committed Jun 21, 2019 293   Benoit Viguier committed Sep 30, 2019 294 \subsubsection{Scalar multiplication algorithms}  Benoit Viguier committed Aug 12, 2019 295 \label{subsec:ECC-ladder}  Benoit Viguier committed Jun 21, 2019 296   Benoit Viguier committed Feb 06, 2020 297 298 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 299 300 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 301 % shown above.  Benoit Viguier committed Feb 13, 2020 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322  % 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 323 324  This gives us the theorem of the correctness of the Montgomery ladder.  Benoit Viguier committed Jun 21, 2019 325 \begin{theorem}  benoit committed Sep 18, 2020 326 327 328  \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 329 \end{theorem}  Benoit Viguier committed Feb 13, 2020 330 \begin{lstlisting}[language=Coq]  Benoit Viguier committed Jun 21, 2019 331 332 333 334 335 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 336 The definition of \coqe{opt_montgomery} is similar to \coqe{montgomery_rec_swap}  Benoit Viguier committed Feb 13, 2020 337 338 339 340 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 341   Benoit Viguier committed Sep 30, 2019 342 \subsection{Curves, twists and extension fields}  Benoit Viguier committed Feb 12, 2020 343 \label{subsec:curve_twist_fields}  Benoit Viguier committed Jun 21, 2019 344   Benoit Viguier committed Jan 17, 2020 345 \fref{tikz:ProofHighLevel2} gives a high-level view of the proofs presented here.  benoit committed Sep 28, 2020 346 347 The white tiles are definitions while green tiles are important lemmas and theorems.  benoit committed Sep 29, 2020 348 349 350 351 352 353 354 355 \begin{figure}[h] \centering \include{tikz/highlevel2} \caption{Proof dependencies for the correctness of X25519.} \label{tikz:ProofHighLevel2} \end{figure} A brief overview of the complete proof of is described bellow.  benoit committed Sep 28, 2020 356 357 358 359 360 361 362 363 We first pose $a = 486662$, $b = 1$, $b' = 2$, $p = 2^{255}-19$, with the equations $C = M_{a,b}$, and $T = M_{a,b'}$. We prove the primality of $p$ and define the field $\F{p}$. Subsquently we show that neither $2$ nor $a^2 - 2$ are square in $\F{p}$. 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 364 365 366 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 367 368 hypothesis~\ref{hyp:a_minus_4_not_square}:% % $a^2-4$ is not a square in \K:  Benoit Viguier committed Oct 01, 2019 369 $$\forall x \in \K,\ x^2 \neq a^2-4.$$  benoit committed Sep 29, 2020 370 371 372 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 373   Benoit Viguier committed Sep 30, 2019 374 \subsubsection{Curves and twists}  Benoit Viguier committed Sep 21, 2019 375 \label{subsec:Zmodp}  Benoit Viguier committed Jun 21, 2019 376 377 378 379 380 381 382 383 384 385 386  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 387 We define the basic operations ($+, -, \times$) with their respective neutral  Benoit Viguier committed Oct 01, 2019 388 elements ($0, 1$) and prove \lref{lemma:Zmodp_field}.  Benoit Viguier committed Jun 21, 2019 389 \begin{lemma}  Benoit Viguier committed Oct 01, 2019 390  \label{lemma:Zmodp_field}  Benoit Viguier committed Oct 01, 2019 391  $\F{p}$ is a field.  Benoit Viguier committed Jun 21, 2019 392 \end{lemma}  Freek Wiedijk committed Oct 01, 2019 393 For $a = 486662$, by using the Legendre symbol we prove that  Benoit Viguier committed Aug 17, 2019 394 $a^2 - 4$ and $2$ are not squares in $\F{p}$.  Benoit Viguier committed Feb 06, 2020 395 \begin{lstlisting}[language=Coq,belowskip=-0.25 \baselineskip]  Benoit Viguier committed Aug 17, 2019 396 Fact a_not_square : forall x: Zmodp.type,  Benoit Viguier committed Jun 21, 2019 397 398  x^+2 != (Zmodp.pi 486662)^+2 - 4%:R. \end{lstlisting}  Benoit Viguier committed Feb 06, 2020 399 \begin{lstlisting}[language=Coq,label=two_not_square,belowskip=-0.1 \baselineskip]  Benoit Viguier committed Aug 17, 2019 400 Fact two_not_square : forall x: Zmodp.type,  Benoit Viguier committed Jun 21, 2019 401 402  x^+2 != 2%:R. \end{lstlisting}  Freek Wiedijk committed Oct 01, 2019 403 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 404 % \begin{dfn}Let the following instantiations of \aref{alg:montgomery-double-add}:\\  Freek Wiedijk committed Oct 01, 2019 405 \begin{dfn}  benoit committed Sep 18, 2020 406  %Let the following instantiations of \aref{alg:montgomery-ladder}:\\  benoit committed Sep 29, 2020 407 408 409 410 411  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 412 \end{dfn}  Benoit Viguier committed Jun 21, 2019 413   Benoit Viguier committed Aug 17, 2019 414 415 With \tref{thm:montgomery-ladder-correct} we derive the following two lemmas: \begin{lemma}  benoit committed Sep 18, 2020 416 417 418  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 419 \end{lemma}  Benoit Viguier committed Aug 17, 2019 420 \begin{lemma}  benoit committed Sep 18, 2020 421 422 423  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 424 \end{lemma}  Benoit Viguier committed Aug 17, 2019 425 426 427 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 428 429 430 431 432 433 434 \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 435 436 437  \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 438 \end{lemma}  Benoit Viguier committed Aug 17, 2019 439 440 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 441 \begin{lemma}  Benoit Viguier committed Aug 17, 2019 442  \label{lemma:curve-or-twist}  Benoit Viguier committed Oct 01, 2019 443 444  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 445 \end{lemma}  Benoit Viguier committed Feb 06, 2020 446 \begin{lstlisting}[language=Coq,belowskip=-0.5 \baselineskip]  Benoit Viguier committed Sep 18, 2019 447 448 Theorem x_is_on_curve_or_twist: forall x : Zmodp.type,  Benoit Viguier committed Jun 21, 2019 449 450 451 452 453  (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 454 \label{subsec:curvep2}  Benoit Viguier committed Jun 21, 2019 455   Benoit Viguier committed Aug 17, 2019 456 The quadratic extension $\F{p^2}$ is defined as $\F{p}[\sqrt{2}]$ by~\cite{Ber06}.  Freek Wiedijk committed Oct 01, 2019 457 The theory of finite fields already has been formalized in the Mathematical Components  Freek Wiedijk committed Oct 01, 2019 458 459 460 461 462 463 464 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 465 466 % in other words, representing polynomials with coefficients in $\F{p}$ modulo $X^2 - 2$. In a similar way  Freek Wiedijk committed Oct 01, 2019 467 as for $\F{p}$ we use a module in Coq.  Benoit Viguier committed Feb 06, 2020 468 \begin{lstlisting}[language=Coq,belowskip=-0.25 \baselineskip]  Benoit Viguier committed Aug 12, 2019 469 Module Zmodp2.  Benoit Viguier committed Jun 21, 2019 470 471 472 Inductive type := Zmodp2 (x: Zmodp.type) (y:Zmodp.type).  Benoit Viguier committed Sep 18, 2019 473 Definition pi (x: Zmodp.type * Zmodp.type) : type :=  Benoit Viguier committed Jun 21, 2019 474  Zmodp2 x.1 x.2.  Benoit Viguier committed Sep 18, 2019 475 Definition mul (x y: type) : type :=  Benoit Viguier committed Jun 21, 2019 476 477 478  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 479 480 481 482 483 484 485 486 487 488 489 % 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 490 491 492 493 494 495 496 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 497 \end{lemma}  Benoit Viguier committed Feb 15, 2020 498 As in $\F{p}$, we define $0^{-1} = 0$ and prove \lref{lemma:Zmodp2_field}.  Benoit Viguier committed Jun 21, 2019 499 \begin{lemma}  Benoit Viguier committed Oct 01, 2019 500 501  \label{lemma:Zmodp2_field} $\F{p^2}$ is a commutative field.  Benoit Viguier committed Jun 21, 2019 502 \end{lemma}  Benoit Viguier committed Sep 27, 2019 503 504 505  %% TOO LONG %% If need remove this paragraph  Freek Wiedijk committed Oct 01, 2019 506 We then specialize the basic operations in order to speed up the verification  Benoit Viguier committed Aug 17, 2019 507 of formulas by using rewrite rules:  Benoit Viguier committed Sep 30, 2019 508 \begin{equation*}  benoit committed Sep 18, 2020 509 510 511 512 513 514 515 516 517  \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 518 \end{equation*}  Benoit Viguier committed Sep 27, 2019 519   Benoit Viguier committed Aug 17, 2019 520 521 The injection $a \mapsto (a,0)$ from $\F{p}$ to $\F{p^2}$ preserves $0, 1, +, -, \times$. Thus $(a,0)$ can be abbreviated as $a$ without confusions.  Benoit Viguier committed Jun 21, 2019 522   Benoit Viguier committed Aug 17, 2019 523 524 525 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 526 $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 527 528 529 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 530   Benoit Viguier committed Feb 06, 2020 531 \begin{lstlisting}[language=Coq,belowskip=-0.25 \baselineskip]  Benoit Viguier committed Aug 17, 2019 532 Lemma x_is_on_curve_or_twist_implies_x_in_Fp2:  Benoit Viguier committed Jun 21, 2019 533 534 535 536 537 538  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 539 \begin{dfn}  benoit committed Sep 29, 2020 540 541 542 543 544 545 546 547 548  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 549 \end{dfn}  Benoit Viguier committed Jun 21, 2019 550 551  \begin{lemma}  Benoit Viguier committed Aug 17, 2019 552 553 554 555  \label{lemma:proj} For all $n \in \N$, for all point $P\in\F{p}\times\F{p}$ on the curve $M_{486662,1}(\F{p})$ (respectively on the quadratic twist $M_{486662,2}(\F{p})$), we have: \begin{align*}  benoit committed Sep 18, 2020 556 557  P \in M_{486662,1}(\F{p}) & \implies \varphi_c(n \cdot P) = n \cdot \varphi_c(P) \\ P \in M_{486662,2}(\F{p}) & \implies \varphi_t(n \cdot P) = n \cdot \varphi_t(P)  Benoit Viguier committed Aug 17, 2019 558  \end{align*}  Benoit Viguier committed Jun 21, 2019 559 560 561 \end{lemma} Notice that: \begin{align*}  benoit committed Sep 18, 2020 562 563  \forall P \in M_{486662,1}(\F{p}),\ \ \psi(\chi_0(\varphi_c(P))) = \chi_0(P) \\ \forall P \in M_{486662,2}(\F{p}),\ \ \psi(\chi_0(\varphi_t(P))) = \chi_0(P)  Benoit Viguier committed Jun 21, 2019 564 565 \end{align*}  Benoit Viguier committed Aug 17, 2019 566 In summary for all $n \in \N,\ n < 2^{255}$, for any given point $P\in\F{p}\times\F{p}$  Benoit Viguier committed Oct 01, 2019 567 in $M_{486662,1}(\F{p})$ or $M_{486662,2}(\F{p})$, $Curve25519\_Fp$  Benoit Viguier committed Aug 17, 2019 568 computes the $\chi_0(n \cdot P)$.  Benoit Viguier committed Sep 30, 2019 569 We 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 570 there exists a corresponding point on the curve or the twist over $\F{p}$.  Benoit Viguier committed Sep 30, 2019 571 We proved that for any point, on the curve or the twist we can compute the  Benoit Viguier committed Aug 17, 2019 572 573 574 575 scalar multiplication by $n$ and yield to the same result as if we did the 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 576 \begin{theorem}  Benoit Viguier committed Aug 17, 2019 577 578 579 580  \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 581 \end{theorem}  benoit committed Sep 28, 2020 582 583 584 585 586 587 588 589 590 % 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 591   Benoit Viguier committed Sep 21, 2019 592 593 We then prove the equivalence between of operations in $\Ffield$ and $\Zfield$, in other words between \coqe{Zmodp} and \coqe{:GF}.  Benoit Viguier committed Sep 27, 2019 594 This allows us to show that given a clamped value $n$ and normalized \xcoord of $P$,  Benoit Viguier committed Sep 21, 2019 595 \coqe{RFC} gives the same results as $Curve25519\_Fp$.  Freek Wiedijk committed Oct 01, 2019 596 597 598  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.