In this section we first present the work of Bartzia and Strub \cite{DBLP:conf/itp/BartziaS14} (\ref{Weierstrass}).

We extend it to support Montgomery curves (\ref{montgomery}) with homogeneous coordinates (\ref{projective}) and prove the correctness of the ladder (\ref{ladder}).

We then prove the montgomery ladder computes

We then prove the Montgomery ladder computes

the x-coordinate of scalar multiplication over $\F{p^2}$

(Theorem 2.1 by Bernstein \cite{Ber06}) where $p$ is the prime $\p$.

...

...

@@ -35,7 +35,7 @@ along with an additional formal point $\Oinf$, ``at infinity''. Such curve does

\end{definition}

In this setting, Bartzia and Strub defined the parametric type \texttt{ec} which

represent the points on a specific curve. It is parametrized by

represent the points on a specific curve. It is parameterized by

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$

We can then specialize the basic operations in order to speed up the verifications of formulas by using rewrite rules:

We can then specialize the basic operations in order to speed up the verification of formulas by using rewrite rules:

\begin{align*}

(a,0) + (b,0) &= (a+b, 0)\\

(a,0) \cdot (b,0) &= (a \cdot b, 0)\\

...

...

@@ -556,7 +556,7 @@ We can then specialize the basic operations in order to speed up the verificatio

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

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})$. Similarily, any point on the quadratic twist $M_{486662,2}(\F{p})$ is also on the curve $M_{486662,1}(\F{p^2})$.

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

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)$

The Verifiable Software Toolchain uses a strongest postcondition strategy.

The user must first write a formal specification of the function he wants to verify in Coq.

This should be as close as possible to the C implementation behavior.

This will simplify the proof and help with stepping throught the CLight version of the software.

With the range of inputes defined, VST steps mechanically through each instruction

This will simplify the proof and help with stepping through the CLight version of the software.

With the range of inputs defined, VST steps mechanically through each instruction

and ask the user to verify auxiliary goals such as array bound access, or absence of overflows/underflows.

We call this specification a low level specification. A user will then have an easier

time to prove that his low level specification matches a simpler higher level one.

...

...

@@ -528,7 +537,7 @@ $\{0,1,2,3\}$:

\end{itemize}

This solution allows us to make cases analysis over possible aliasing.

\subsection{Verifiying \texttt{for} loops}

\subsection{Verifying \texttt{for} loops}

Final state of \texttt{for} loops are usually computed by simple recursive functions.

However we must define invariants which are true for each iteration.

...

...

@@ -580,4 +589,4 @@ Lemma Tail_Head_equiv :

forall (n:nat) (s:T),

rec_fn n s = rec_fn_rev n s.

\end{Coq}

Using this formalization, we prove that the 255 steps of the montgomery ladder in C provide the same computations are the one defined in Algorithm \ref{montgomery-double-add}.

Using this formalization, we prove that the 255 steps of the Montgomery ladder in C provide the same computations are the one defined in Algorithm \ref{montgomery-double-add}.