@@ -105,7 +105,7 @@ Points on an elliptic curve form an abelian group when equipped with the followi

\item The negation of a point $P =(x,y)$ is defined by reflection over the $x$-axis, \ie$-P =(x, -y)$.

\item The addition of two points $P$ 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$

\item$\Oinf$ is the neutral element under this law: if 3 points are collinear, their sum is equal to $\Oinf$.

\end{itemize}

These operations are defined in Coq as follows (where we omit the code for the tangent case):

\begin{lstlisting}[language=Coq]

...

...

@@ -293,14 +293,14 @@ Similarly, we also prove the formula for point doubling.% (\lref{lemma:xDBL}).

we have $X_3/Z_3=\chi(2P_1)$.

\end{lemma}

With \lref{lemma:xADD} and \lref{lemma:xDBL}, we are able to compute efficiently

With \lref{lemma:xADD} and \lref{lemma:xDBL}, we are able to efficiently compute

differential additions and point doublings using projective coordinates.

\subsubsection{Scalar multiplication algorithms}

\label{subsec:ECC-ladder}

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},

combination of the formulas from \lref{lemma:xADD} and \lref{lemma:xDBL},% formula/s/ to make it consistent with the rest of the text -T

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}).

% shown above.

...

...

@@ -361,18 +361,18 @@ The white tiles are definitions while green tiles are important lemmas and theor

A brief overview of the complete proof is described below.

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}$.

Subsequently, we show that neither $2$ nor $a^2-2$are square in $\F{p}$.

Subsequently, we show that neither $2$ nor $a^2-2$is a 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 exists 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})$.

We prove that for all $x \in\F{p}$ there exists a point with\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 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.

Now that we have an red line for the proof, we turn our attention to the details.

Now that we have a 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

hypothesis~\ref{hyp:a_minus_4_not_square}:%

Hypothesis~\ref{hyp:a_minus_4_not_square}:%

% $a^2-4$ is not a square in \K:

$$\forall x \in\K,\ x^2\neq a^2-4.$$

$$\forall x \in\K,\ x^2\neq a^2-4,$$

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}.

...

...

@@ -419,14 +419,15 @@ This allows us to study $M_{486662,1}(\F{p})$ and $M_{486662,2}(\F{p})$, one of

With \tref{thm:montgomery-ladder-correct} we derive the following two lemmas:

\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$.

$$Curve25519\_Fp(n,x)=\chi_0(n \cdot P)$$

Let $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$, then

$$Curve25519\_Fp(n,x)=\chi_0(n \cdot P).$$

% I was thrown off by the full stop about what the actual statement was. -T

\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$.