highlevel.tex 24.6 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 Aug 16, 2019 4 5 6 7 8 9 In this section we prove the following theorem: \begin{theorem} \label{thm:Elliptic-CSM} The implementation of X25519 in TweetNaCl (\TNaCle{crypto_scalarmult}) computes the $\F{p}$-restricted $x$-coordinate 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 Aug 12, 2019 10 11 \end{theorem}  Benoit Viguier committed Aug 16, 2019 12 13 14 15 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 Jun 21, 2019 16 17  \subsection{Formalization of Elliptic Curves}  Benoit Viguier committed Aug 12, 2019 18 \label{subsec:ECC}  Benoit Viguier committed Jun 21, 2019 19 20 21 22  We consider elliptic curves over a field $\K$. We assume that the characteristic of $\K$ is neither 2 or 3.  Benoit Viguier committed Aug 12, 2019 23 \begin{dfn}  Benoit Viguier committed Jun 21, 2019 24 Let a field $\K$, using an appropriate choice of coordinates, an elliptic curve $E$  Benoit Viguier committed Jul 22, 2019 25 is a plane cubic algebraic curve $E(x,y)$ defined by an equation of the form:  Benoit Viguier committed Jun 21, 2019 26 27 28 29 30 $$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, written $E(\K)$, is formed by the solutions $(x,y)$ of $E$ augmented by 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 31 \end{dfn}  Benoit Viguier committed Jun 21, 2019 32 33  \subsubsection{Weierstra{\ss} Curves}  Benoit Viguier committed Aug 12, 2019 34 35 \label{subsec:ECC-Weierstrass}  Benoit Viguier committed Jul 22, 2019 36 This equation $E(x,y)$ can be reduced into its short Weierstra{\ss} form.  Benoit Viguier committed Jun 21, 2019 37   Benoit Viguier committed Aug 12, 2019 38 \begin{dfn}  Benoit Viguier committed Jul 22, 2019 39 40 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}(\K)$ is the set of all points $(x,y) \in \K^2$ satisfying the equation:  Benoit Viguier committed Jun 21, 2019 41 $$y^2 = x^3 + ax + b,$$  Benoit Viguier committed Aug 16, 2019 42 along with an additional formal point $\Oinf$, at infinity''. Such a curve does not present any singularity.  Benoit Viguier committed Aug 12, 2019 43 \end{dfn}  Benoit Viguier committed Jun 21, 2019 44 45  In this setting, Bartzia and Strub defined the parametric type \texttt{ec} which  Benoit Viguier committed Aug 01, 2019 46 represent the points on a specific curve. It is parameterized by  Benoit Viguier committed Jun 21, 2019 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 a \texttt{K : ecuFieldType} -- the type of fields which characteristic is not 2 or 3 -- and \texttt{E : ecuType} -- a record that packs the curve parameters $a$ and $b$ 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 Aug 16, 2019 64 Points of an elliptic curve are equipped with a structure of an abelian group.  Benoit Viguier committed Jun 21, 2019 65 \begin{itemize}  Benoit Viguier committed Aug 01, 2019 66  \item The negation of a point $P = (x,y)$ by taking the symmetric with respect to the x axis $-P = (x, -y)$.  Benoit Viguier committed Jun 21, 2019 67 68  \item The addition of two points $P$ and $Q$ is defined by the negation of third intersection of the line passing by $P$ and $Q$ or tangent to $P$ if $P = Q$.  Benoit Viguier committed Aug 01, 2019 69  \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 70 71 \end{itemize}  Benoit Viguier committed Aug 16, 2019 72 These operations are defined in Coq as follow:  Benoit Viguier committed Jun 21, 2019 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 \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 Viguier committed Aug 16, 2019 89 And are proven internal to the curve (with coercion):  Benoit Viguier committed Jun 21, 2019 90 91 92 93 94 95 96 97 \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} \subsubsection{Montgomery Curves}  Benoit Viguier committed Aug 12, 2019 98 99 \label{subsec:ECC-Montgomery}  Benoit Viguier committed Aug 16, 2019 100 101 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 102   Benoit Viguier committed Aug 12, 2019 103 \begin{dfn}  Benoit Viguier committed Jul 22, 2019 104 105  Let $a \in \K \backslash \{-2, 2\}$, and $b \in \K \backslash \{ 0\}$. The \textit{Montgomery curve} $M_{a,b}(\K)$ is the set of all points $(x,y) \in \K^2$ satisfying the equation:  Benoit Viguier committed Jun 21, 2019 106 107  $$by^2 = x^3 + ax^2 + x,$$ along with an additional formal point $\Oinf$, at infinity''.  Benoit Viguier committed Aug 12, 2019 108 \end{dfn}  Benoit Viguier committed Jun 21, 2019 109 Using a similar representation, we defined the parametric type \texttt{mc} which  Benoit Viguier committed Aug 01, 2019 110 represent the points on a specific Montgomery curve. It is parameterized by  Benoit Viguier committed Jun 21, 2019 111 a \texttt{K : ecuFieldType} -- the type of fields which characteristic is not 2 or 3 --  Benoit Viguier committed Aug 01, 2019 112 and \texttt{M : mcuType} -- a record that packs the curve parameters $a$ and $b$  Benoit Viguier committed Jul 22, 2019 113 along with the proofs that $b \neq 0$ and $a^2 \neq 4$.  Benoit Viguier committed Jun 21, 2019 114 115 116 117 118 119 120 121 122 123 124 \begin{lstlisting}[language=Coq] 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 Jul 22, 2019 125 We define the addition on Montgomery curves the same way as it is in the Weierstra{\ss} form,  Benoit Viguier committed Jun 21, 2019 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 however the actual computations will be slightly different. \begin{lstlisting}[language=Coq] 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} But we prove it is internal to the curve (again with coercion): \begin{lstlisting}[language=Coq] Lemma addO (p q : mc) : oncurve (add p q). Definition addmc (p1 p2 : mc) : mc := MC p1 p2 (addO p1 p2) \end{lstlisting} We then prove a bijection between a Montgomery curve and its Weierstra{\ss} equation. \begin{lemma} Let $M_{a,b}(\K)$ be a Montgomery curve, define $$a' = \frac{3-a^2}{3b^2} \text{\ \ \ \ and\ \ \ \ } b' = \frac{2a^3 - 9a}{27b^3}.$$ then $E_{a',b'}(\K)$ is an elliptic curve, and the mapping $\varphi : M_{a,b}(\K) \mapsto E_{a',b'}(\K)$ defined as: \begin{align*} \varphi(\Oinf_M) &= \Oinf_E\\ \varphi( (x , y) ) &= ( \frac{x}{b} + \frac{a}{3b} , \frac{y}{b} ) \end{align*} is an isomorphism between groups. \end{lemma} \begin{lstlisting}[language=Coq] 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} \subsubsection{Projective Coordinates}  Benoit Viguier committed Aug 12, 2019 176 177 \label{subsec:ECC-projective}  Benoit Viguier committed Aug 16, 2019 178 179 180 181 182 183 184 185 186 187 188 189 On a projective plane, points are represented with a triple $(X:Y:Z)$. With the exception of $(0:0:0)$, any points can be projected. Scalar multiples are representing the same point, \ie for all $\lambda \neq 0$, $(X:Y:Z)$ are $(\lambda X:\lambda Y:\lambda Z)$ defining the same point. For $Z\neq 0$, the projective point $(X:Y:Z)$ corresponds to the point $(X/Z,Y/Z)$ on the Euclidean plane, likewise the point $(X,Y)$ on the Euclidean plane corresponds to $(X:Y:1)$ on the projective plane. Using fractions as coordinates, the equation for a Montgomery curve $M_{a,b}(\K)$ 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 190 Multiplying both sides by $Z^3$ yields:  Benoit Viguier committed Aug 16, 2019 191 $$b Y^2Z = X^3 + a X^2Z + XZ^2$$  Benoit Viguier committed Jul 22, 2019 192 193 With this equation we can additionally represent the point at infinity''. By setting $Z=0$, we derive $X=0$, giving us the infinite points'' $(0:Y:0)$ with $Y\neq 0$.  Benoit Viguier committed Jun 21, 2019 194   Benoit Viguier committed Aug 01, 2019 195 By restricting the parameter $a$ of $M_{a,b}(\K)$ such that $a^2-4$ is not a  Benoit Viguier committed Jul 22, 2019 196 square in \K, we ensure that $(0,0)$ is the only point with a $y$-coordinate of $0$.  Benoit Viguier committed Jun 21, 2019 197 198 199 200 \begin{lstlisting}[language=Coq] Hypothesis mcu_no_square : forall x : K, x^+2 != (M#a)^+2 - 4%:R. \end{lstlisting}  Benoit Viguier committed Aug 16, 2019 201 202 We define $\chi$ and $\chi_0$ to return the $x$-coordinate of points on a curve. \begin{dfn}Let $\chi$ and $\chi_0$:\\  Benoit Viguier committed Jun 21, 2019 203 204 205 206 -- $\chi : M_{a,b}(\K) \to \K \cup \{\infty\}$\\ such that $\chi(\Oinf) = \infty$ and $\chi((x,y)) = x$.\\ -- $\chi_0 : M_{a,b}(\K) \to \K$\\ such that $\chi_0(\Oinf) = 0$ and $\chi_0((x,y)) = x$.  Benoit Viguier committed Aug 12, 2019 207 \end{dfn}  Benoit Viguier committed Aug 16, 2019 208 209 Using projective coordinates we prove the With those coordinates we prove the following lemmas for the addition of two points.  Benoit Viguier committed Jun 21, 2019 210 \begin{lemma}  Benoit Viguier committed Aug 14, 2019 211 \label{lemma:add}  Benoit Viguier committed Jul 22, 2019 212 213 Let $M_{a,b}(\K)$ be a Montgomery curve such that $a^2-4$ is not a square, and let $X_1, Z_1, X_2, Z_2, X_3, Z_3 \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$.  Benoit Viguier committed Jun 21, 2019 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 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$ on $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:} For any $x \in \K \backslash\{0\}, x/0$ should be understood as $\infty$. \end{lemma} % This can be formalized as follow: % \begin{lstlisting}[language=Coq] % Inductive K_infty := % | K_Inf : K_infty % | K_Fin : K -> K_infty. % % Definition point_x (p : point K) := % if p is (|x, _|) then K_Fin x else K_Inf. % Local Notation "p '#x'" := (point_x p) (at level 30). % Definition point_x0 (p : point K) := % if p is (|x, _|) then x else 0. % Local Notation "p '#x0'" := (point_x0 p) (at level 30). % % Definition inf_div (x z : K) := % if z == 0 then K_Inf else K_Fin (x / z). % Definition hom_ok (x z : K) := (x != 0) || (z != 0). % Lemma montgomery_hom_neq : % forall x1 x2 x4 z1 z2 z4 : K, % hom_ok x1 z1 -> hom_ok x2 z2 -> % (x4 != 0) && (z4 != 0) -> % let x3 := z4 * ((x1 - z1)*(x2 + z2) % + (x1 + z1)*(x2 - z2))^+2 in % let z3 := x4 * ((x1 - z1)*(x2 + z2) % - (x1 + z1)*(x2 - z2))^+2 in % forall p1 p2 : point K, % oncurve M p1 -> oncurve M p2 -> % p1#x = inf_div x1 z1 -> % p2#x = inf_div x2 z2 -> % (p1 \- p2)#x = inf_div x4 z4 -> % hom_ok x3 z3 && ((p1 \+ p2)#x == inf_div x3 z3). % \end{lstlisting} With those coordinates we also prove a similar lemma for point doubling. \begin{lemma}  Benoit Viguier committed Aug 14, 2019 256 \label{lemma:double}  Benoit Viguier committed Jul 22, 2019 257 258 Let $M_{a,b}(\K)$ be a Montgomery curve such that $a^2-4$ is not a square, and let $X_1, Z_1, X_2, Z_2, X_3, Z_3 \in \K$, such that $(X_1,Z_1) \neq (0,0)$. Define  Benoit Viguier committed Jun 21, 2019 259 260 261 262 263 \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*}  Benoit Viguier committed Jul 22, 2019 264 265 then for any point $P_1$ on $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 266 267 268 269 270 271 272 273 274 275 276 277 278 279 \end{lemma} % Which is formalized as follow: % \begin{lstlisting}[language=Coq] % Lemma montgomery_hom_eq : % forall x1 z1 : K, % hom_ok x1 z1 -> % let c := (x1 + z1)^+2 - (x1 - z1)^+2 in % let x3 := (x1 + z1)^+2 * (x1 - z1)^+2 in % let z3 := c * ((x1 + z1)^+2 + (((M#a) - 2%:R)/4%:R) * c) in % forall p : point K, oncurve M p -> % p#x = inf_div x1 z1 -> % (p \+ p)#x = inf_div x3 z3. % \end{lstlisting}  Benoit Viguier committed Aug 14, 2019 280 With these two lemmas (\ref{lemma:add} and \ref{lemma:double}), we have the basic  Benoit Viguier committed Jul 22, 2019 281 tools to compute efficiently additions and point doubling on projective coordinates.  Benoit Viguier committed Jun 21, 2019 282 283  \subsubsection{Scalar Multiplication Algorithms}  Benoit Viguier committed Aug 12, 2019 284 \label{subsec:ECC-ladder}  Benoit Viguier committed Jun 21, 2019 285   Benoit Viguier committed Jul 22, 2019 286 287 288 289 Suppose we have a scalar $n$ and a point $P$ on some curve. The most straightforward way to compute $n \cdot P$ is to repetitively add $P$ \ie computing $P + \ldots + P$. However there is an more efficient algorithm which makes use of the binary representation of $n$ and by combining doubling and adding and starting from $\Oinf$.  Benoit Viguier committed Jun 21, 2019 290 291 \eg for $n=11$, we compute $2(2(2(2\Oinf + P)) + P)+ P$.  Benoit Viguier committed Jul 22, 2019 292 293 294 With a simple double-and-add algorithm, with careful timing, an attacker could reconstruct $n$. In the case of X25519, $n$ is the private key. With the Montgomery's ladder, while it provides slightly more computations and an extra variable, we can prevent such weakness.  Benoit Viguier committed Aug 12, 2019 295 See \aref{alg:montgomery-ladder}.  Benoit Viguier committed Jun 21, 2019 296 297  \begin{lemma}  Benoit Viguier committed Aug 14, 2019 298 \label{lemma:montgomery-ladder}  Benoit Viguier committed Aug 12, 2019 299 \aref{alg:montgomery-ladder} is correct, \ie it respects its output conditions given the input conditions.  Benoit Viguier committed Jun 21, 2019 300 301 \end{lemma}  Benoit Viguier committed Jul 22, 2019 302 In Curve25519 we are only interested in the $x$ coordinate of points, using  Benoit Viguier committed Aug 14, 2019 303 Lemmas \ref{lemma:add} and \ref{lemma:double}, and replacing the if statements  Benoit Viguier committed Jul 22, 2019 304 with conditional swapping we can define a ladder similar to the one used in TweetNaCl.  Benoit Viguier committed Aug 12, 2019 305 See \aref{alg:montgomery-double-add}  Benoit Viguier committed Jun 21, 2019 306 307 308  \begin{algorithm} \caption{Montgomery ladder for scalar multiplication on $M_{a,b}(\K)$ with optimizations}  Benoit Viguier committed Aug 12, 2019 309 \label{alg:montgomery-double-add}  Benoit Viguier committed Jun 21, 2019 310 311 \begin{algorithmic} \REQUIRE{$x \in \K\backslash \{0\}$, scalars $n$ and $m$, $n < 2^m$}  Benoit Viguier committed Jul 22, 2019 312 \ENSURE{$a/c = \chi_0(n \cdot P)$ for any $P$ such that $\chi_0(P) = x$}  Benoit Viguier committed Jun 21, 2019 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 \STATE $(a,b,c,d) \leftarrow (1,x,0,1)$ \FOR{$k$ := $m$ downto $1$} \IF{$k^{\text{th}}$ bit of $n$ is $1$} \STATE $(a,b) \leftarrow (b,a)$ \STATE $(c,d) \leftarrow (d,c)$ \ENDIF \STATE $e \leftarrow a + c$ \STATE $a \leftarrow a - c$ \STATE $c \leftarrow b + d$ \STATE $b \leftarrow b - d$ \STATE $d \leftarrow e^2$ \STATE $f \leftarrow a^2$ \STATE $a \leftarrow c \times a$ \STATE $c \leftarrow b \times e$ \STATE $e \leftarrow a + c$ \STATE $a \leftarrow a - c$ \STATE $b \leftarrow a^2$ \STATE $c \leftarrow d-f$ \STATE $a \leftarrow c\times\frac{A - 2}{4}$ \STATE $a \leftarrow a + d$ \STATE $c \leftarrow c \times a$ \STATE $a \leftarrow d \times f$ \STATE $d \leftarrow b \times x$ \STATE $b \leftarrow e^2$ \IF{$k^{\text{th}}$ bit of $n$ is $1$} \STATE $(a,b) \leftarrow (b,a)$ \STATE $(c,d) \leftarrow (d,c)$ \ENDIF \ENDFOR \end{algorithmic} \end{algorithm} \begin{lemma}  Benoit Viguier committed Aug 14, 2019 346 \label{lemma:montgomery-double-add}  Benoit Viguier committed Aug 12, 2019 347 \aref{alg:montgomery-double-add} is correct, \ie it respects its output  Benoit Viguier committed Jul 22, 2019 348 conditions given the input conditions.  Benoit Viguier committed Jun 21, 2019 349 350 351 352 \end{lemma} %% here we have \chi and \chi_0 ...  Benoit Viguier committed Aug 14, 2019 353 We formalized this lemma (\ref{lemma:montgomery-double-add}):  Benoit Viguier committed Jun 21, 2019 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 \begin{lstlisting}[language=Coq] 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] Lemma opt_montgomery_0: forall (n m : nat), opt_montgomery n m 0 = 0. \end{lstlisting} Also \Oinf\ is the neutral element over $M_{a,b}(\K)$, we have: $$\forall P, P + \Oinf\ = P$$ thus we derive the following lemma. % \begin{lemma}  Benoit Viguier committed Aug 14, 2019 371 % \label{lemma:montgomery-double-add}  Benoit Viguier committed Jun 21, 2019 372 373 374 375 376 377 378 379 380 381 % Algorithm \ref{montgomery-double-add} is correct even if $x=0$, \ie it respects its output conditions given the input conditions or $x=0$. % \end{lemma} \begin{lstlisting}[language=Coq] Lemma p_x0_0_eq_0 : forall (n : nat) (p : mc M), p #x0 = 0%:R -> (p *+ n) #x0 = 0%R. \end{lstlisting} And thus the theorem of the correctness of the Montgomery ladder. \begin{theorem} \label{montgomery-ladder-correct} For all $n, m \in \N$, $x \in \K$, $P \in M_{a,b}(\K)$,  Benoit Viguier committed Aug 12, 2019 382 if $\chi_0(P) = x$ then \aref{alg:montgomery-double-add} returns $\chi_0(n \cdot P)$  Benoit Viguier committed Jun 21, 2019 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 \end{theorem} \begin{lstlisting}[language=Coq] 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} \subsection{Curves, Twists and Extension Fields} One hypothesis to be able to use the above theorem is that $a^2-4$ is not a square: $$\forall x \in \K,\ x^2 \neq a^2-4$$ As Curve25519 is defined over the field $\K = \F{p^2}$, there exists $x$ such that $x^2 = a^2-4$. We first study Curve25519 and one of the quadratic twist Twist25519, first defined over \F{p}. \subsubsection{Curves and Twists} 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. Lemma Z_mod_betweenb (x y : Z) : y > 0 -> betweenb 0 y (x mod y). Definition pi (x : Z) : type := Zmodp (Z_mod_betweenb x Hp_gt0). Coercion repr (x : type) : Z := let: @Zmodp x _ := x in x. End Zmodp. \end{lstlisting} We define the basic operations ($+, -, \times$) with their respective neutral elements ($0, 1$). \begin{lemma} $\F{p}$ is a commutative ring. \end{lemma} % \begin{lstlisting}[language=Coq] % Definition zero : type := pi 0. % Definition one : type := pi 1. % Definition opp (x : type) : type := pi (p - x). % Definition add (x y : type) : type := pi (x + y). % Definition sub (x y : type) : type := pi (x - y). % Definition mul (x y : type) : type := pi (x * y). % % Lemma Zmodp_ring : % ring_theory zero one add mul sub opp eq. % \end{lstlisting} And finally for $a = 486662$, by using the Legendre symbol we prove that $a^2 - 4$ and $2$ are not squares in $\F{p}$. \begin{lstlisting}[language=Coq] Lemma a_not_square : forall x: Zmodp.type, x^+2 != (Zmodp.pi 486662)^+2 - 4%:R. \end{lstlisting} \begin{lstlisting}[language=Coq,label=two_not_square] Lemma two_not_square : forall x : Zmodp.type, x^+2 != 2%:R. \end{lstlisting} We consider $M_{486662,1}(\F{p})$ and $M_{486662,2}(\F{p})$, one of its quadratic twist. % $M_{486662,1}(\F{p})$ has the same equation as $M_{486662,1}(\F{p^2})$ while $M_{486662,2}(\F{p})$ is one of its quadratic twist.  Benoit Viguier committed Aug 01, 2019 447 By instantiating theorem \ref{montgomery-ladder-correct} we derive the following two lemmas:  Benoit Viguier committed Jun 21, 2019 448 449 \begin{lemma} 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$.  Benoit Viguier committed Jul 22, 2019 450 Given $n$ and $x$, $Curve25519\_Fp(n,x) = \chi_0(n \cdot P)$.  Benoit Viguier committed Jun 21, 2019 451 452 453 \end{lemma} \begin{lemma} 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$.  Benoit Viguier committed Jul 22, 2019 454 Given $n$ and $x$, $Twist25519\_Fp(n,x) = \chi_0(n \cdot P)$.  Benoit Viguier committed Jun 21, 2019 455 \end{lemma}  Benoit Viguier committed Aug 16, 2019 456 As the Montgomery ladder defined above does not depend on $b$, it is trivial to see that the computations done for points of $M_{486662,1}(\F{p})$ and of $M_{486662,2}(\F{p})$ are the same.  Benoit Viguier committed Jun 21, 2019 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 \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} \label{square-or-2square} For all $x$ in $\F{p}$, there exists $y$ in $\F{p}$ such that $$y^2 = x\ \ \ \lor\ \ 2y^2 = x$$ \end{lemma} For all $x \in \F{p}$, we can compute $x^3 + ax^2 + x$. Using Lemma \ref{square-or-2square} we can find a $y$ such that $(x,y)$ is either on the curve or on the quadratic twist: \begin{lemma} \label{curve-or-twist} For all $x \in \F{p}$, there exists a point $P$ over $M_{486662,1}(\F{p})$ or over $M_{486662,2}(\F{p})$ such that the $x$-coordinate of $P$ is $x$. \end{lemma} \begin{lstlisting}[language=Coq] Theorem x_is_on_curve_or_twist: forall x : Zmodp.type, (exists (p : mc curve25519_mcuType), p#x0 = x) \/ (exists (p' : mc twist25519_mcuType), p'#x0 = x). \end{lstlisting} \subsubsection{Curve25519 over \F{p^2}} We use the same definitions as in \cite{Ber06}. We consider the extension field $\F{p^2}$ as the set $\F{p} \times \F{p}$ with $\delta = 2$, in other words, the polynomial with coefficients in $\F{p}$ modulo $X^2 - 2$. In a similar way as for $\F{p}$ we use Module in Coq. \begin{lstlisting}[language=Coq]  Benoit Viguier committed Aug 12, 2019 484 Module Zmodp2.  Benoit Viguier committed Jun 21, 2019 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 Inductive type := Zmodp2 (x: Zmodp.type) (y:Zmodp.type). Definition pi (x : Zmodp.type * Zmodp.type) : type := Zmodp2 x.1 x.2. Coercion repr (x : type) : Zmodp.type*Zmodp.type := let: Zmodp2 u v := x in (u, v). 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). Definition mul (x y : type) : type := pi ((x.1 * y.1) + (2%:R * (x.2 * y.2)), (x.1 * y.2) + (x.2 * y.1)). \end{lstlisting} We define the basic operations ($+, -, \times$) with their respective neutral elements ($0, 1$). Additionally we verify that for each element of in $\F{p^2}\backslash\{0\}$, there exists a multiplicative inverse. \begin{lemma} 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)$$ \end{lemma}  Benoit Viguier committed Aug 01, 2019 512 Similarly as in $\F{p}$, we define $0^{-1} = 0$.  Benoit Viguier committed Jun 21, 2019 513 514 515 \begin{lemma} $\F{p^2}$ is a commutative ring. \end{lemma}  Benoit Viguier committed Aug 01, 2019 516 We can then specialize the basic operations in order to speed up the verification of formulas by using rewrite rules:  Benoit Viguier committed Jun 21, 2019 517 518 519 520 521 522 523 524 525 526 527 \begin{align*} (a,0) + (b,0) &= (a+b, 0)\\ (a,0) \cdot (b,0) &= (a \cdot b, 0)\\ (a, 0)^n &= (a^n, 0)\\ (a, 0)^{-1} &= (a^{-1}, 0)\\ (a, 0)\cdot (0,b) &= (0, a\cdot b)\\ (0, a)\cdot (0,b) &= (2\cdot a\cdot b, 0)\\ (0,a)^{-1} &= ((2\cdot a)^{-1},0) \end{align*} 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 Aug 01, 2019 528 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 $M_{486662,2}(\F{p})$ is also on the curve $M_{486662,1}(\F{p^2})$.  Benoit Viguier committed Jun 21, 2019 529 530 531 532 533 534 535 536 537 538 As direct consequence, using lemma \ref{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,2}(\F{p})$ such that $\chi_0(P)$ is $(x,0)$ \begin{lstlisting}[language=Coq] Theorem x_is_on_curve_or_twist_implies_x_in_Fp2: 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 Viguier committed Jun 21, 2019 540 541 542 543 544 545 546 Define the functions $\varphi_c$, $\varphi_t$ and $\psi$\\ -- $\varphi_c: M_{486662,1}(\F{p}) \mapsto M_{486662,1}(\F{p^2})$\\ such that $\varphi((x,y)) = ((x,0), (y,0))$.\\ -- $\varphi_t: M_{486662,2}(\F{p}) \mapsto M_{486662,1}(\F{p^2})$\\ such that $\varphi((x,y)) = ((x,0), (0,y))$.\\ -- $\psi: \F{p^2} \mapsto \F{p}$\\ such that $\psi(x,y) = (x)$.  Benoit Viguier committed Aug 12, 2019 547 \end{dfn}  Benoit Viguier committed Jun 21, 2019 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562  \begin{lemma} 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*} 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) \end{align*} \end{lemma} Notice that: \begin{align*} \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) \end{align*}  Benoit Viguier committed Jul 22, 2019 563 In summary for all $n \in \N,\ n < 2^{255}$, for any given point $P\in\F{p}\times\F{p}$ on $M_{486662,1}(\F{p})$ or $M_{486662,2}(\F{p})$ \texttt{curve25519\_Fp\_ladder} computes the $\chi_0(n \cdot P)$.  Benoit Viguier committed Jun 21, 2019 564 565 566 We have proved that for all $P \in \F{p^2}\times\F{p^2}$ such that $\chi_0(P) \in \F{p}$ there exists a corresponding point on the curve or the twist over $\F{p}$. We have proved that for any point, on the curve or the twist we can compute the 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}: \begin{theorem}  Benoit Viguier committed Jul 22, 2019 567 For all $n \in \N$, $x \in \F{P}$, $P \in M_{486662,1}(\F{p^2})$, such that $n < 2^{255}$ and $\chi_0(P) = \varphi(x)$, \texttt{curve25519\_Fp\_ladder}$(n, x)$ computes $\psi(\chi_0(n \cdot P))$.  Benoit Viguier committed Jun 21, 2019 568 569 570 571 572 573 574 575 576 \end{theorem} which can be formalized in Coq as: \begin{lstlisting}[language=Coq] Lemma curve25519_Fp2_ladder_ok (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 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604  By converting those array of 32 bytes into their respective little-endian value we prove the correctness of \TNaCle{crypto_scalarmult} (Theorem \ref{CSM-correct}) in Coq (for the sake of simplicity we do not display the conversion in the theorem). \begin{theorem} \label{CSM-correct} For all $n \in \N, n < 2^{255}$ and where the bits 1, 2, 5 248, 249, 250 are cleared and bit 6 is set, for all $P \in E(\F{p^2})$, for all $p \in \F{p}$ such that $P.x = p$, there exists $Q \in E(\F{p^2})$ such that $Q = \cdot P$ where $Q.x = q$ and $q$ = \VSTe{CSM} $n$ $p$. \end{theorem} A more complete description in Coq of Theorem \ref{CSM-correct} with the associated conversions is as follow: \begin{lstlisting}[language=Coq] Theorem Crypto_Scalarmult_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 (ZUnpack25519 (ZofList 8 p)) = P#x0 -> ZofList 8 (Crypto_Scalarmult n p) = (P *+ (Z.to_nat (Zclamp (ZofList 8 n)))) _x0. \end{lstlisting}