Commit aa0a1f9a authored by Benoit Viguier's avatar Benoit Viguier
Browse files

simplifies proof and writting

parent 7e0ccd7c
......@@ -46,19 +46,19 @@ Definition curve25519_ladder n x :=
Local Notation "p '#x0'" := (point_x0 p) (at level 30).
Theorem curve25519_ladder_ok (n : nat) x :
(n < 2^255)%nat -> x != 0 ->
(n < 2^255)%nat ->
forall (p : mc curve25519_mcuType), p#x0 = x -> curve25519_ladder n x = (p *+ n)#x0.
Proof.
move => Hn Hx p Hp.
move => Hn p Hp.
rewrite /curve25519_ladder.
apply opt_montgomery_ok=> //=.
rewrite /a.
apply a_not_square.
Qed.
Lemma curve25519_0 (n : nat) :
(* Lemma curve25519_0 (n : nat) :
curve25519_ladder n 0 = 0.
Proof.
rewrite /curve25519_ladder.
apply opt_montgomery_0.
Qed.
\ No newline at end of file
Qed. *)
\ No newline at end of file
......@@ -129,16 +129,15 @@ From mathcomp Require Import ssrnat.
Theorem curve25519_ladder_really_ok (n : nat) x :
(n < 2^255)%nat ->
x != 0 ->
forall (p : mc curve25519_mcuType),
(curve25519_Fp_to_Fp2 p)#x0 = Zmodp2.Zmodp2 x 0 ->
curve25519_ladder n x = ((curve25519_Fp_to_Fp2 p) *+ n)#x0 /p.
Proof.
move => Hn Hx p Hp.
move => Hn p Hp.
have Hp' := cFp_to_Fp2_cancel p.
have Hp'' : p #x0 = x.
move: Hp'; rewrite Hp => //=.
rewrite (curve25519_ladder_ok n x Hn Hx p Hp'').
rewrite (curve25519_ladder_ok n x Hn p Hp'').
rewrite -nP_is_nP2.
rewrite cFp_to_Fp2_cancel //.
Qed.
......
......@@ -136,17 +136,12 @@ Lemma curve25519_ladder_maybe_ok (n : nat) (x:Zmodp.type) :
curve25519_ladder n x = (p *+ n)#x0 /p.
Proof.
move => Hn p Hp.
have /orP[Hx|Hx] := orNb (x == 0).
+ have [[c] Hc|[t] Ht] := Fp2_to_Fp x p Hp.
+ have Hcx0: curve25519_Fp_to_Fp2 c #x0 = Zmodp2.Zmodp2 x 0 by rewrite Hc.
rewrite (curve25519_ladder_really_ok n x Hn Hx c Hcx0) -Fp_to_Fp2_eq_C Hc //.
+ have Htx0: twist25519_Fp_to_Fp2 t #x0 = Zmodp2.Zmodp2 x 0 by rewrite Ht.
rewrite curve_twist_eq.
rewrite (twist25519_ladder_really_ok n x Hn Hx t Htx0) -Fp_to_Fp2_eq_T Ht //.
+ move/eqP: Hx Hp => ->.
rewrite curve25519_0.
have -> : Zmodp2.Zmodp2 0 0 = 0 => //=.
move/(p_x0_0_eq_0 n) => -> //.
have [[c] Hc|[t] Ht] := Fp2_to_Fp x p Hp.
+ have Hcx0: curve25519_Fp_to_Fp2 c #x0 = Zmodp2.Zmodp2 x 0 by rewrite Hc.
rewrite (curve25519_ladder_really_ok n x Hn c Hcx0) -Fp_to_Fp2_eq_C Hc //.
+ have Htx0: twist25519_Fp_to_Fp2 t #x0 = Zmodp2.Zmodp2 x 0 by rewrite Ht.
rewrite curve_twist_eq.
rewrite (twist25519_ladder_really_ok n x Hn t Htx0) -Fp_to_Fp2_eq_T Ht //.
Qed.
Close Scope ring_scope.
\ No newline at end of file
......@@ -29,7 +29,7 @@ Reserved Notation "\- x" (at level 50).
Record mcuType (K : ringType) := {
cA : K;
cB : K;
_ : cB != 0;
pB : cB != 0;
_ : cA^+2 != 4%:R;
}.
......@@ -82,6 +82,12 @@ Section MC.
Lemma oncurve_mc: forall p : mc, oncurve p.
Proof. exact: valP. Qed.
Lemma oncurve_0_0: oncurve (|0%:R ,0%:R|).
Proof. move => /= ; rewrite ?exprS ?expr0 ?mul0r ?mulr0 ?addr0 ; apply/eqP => //. Qed.
Lemma oncurve_inf: oncurve .
Proof. done. Qed.
Hint Resolve oncurve_mc.
End MC.
......
......@@ -137,7 +137,7 @@ Section OptimizedLadder.
- by apply/eqP; apply: montgomery_hom_eq; rewrite ?E //.
Qed.
Lemma opt_montgomery_ok (n m : nat) (x : K) :
Lemma opt_montgomery_x (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.
Proof.
......@@ -196,11 +196,53 @@ Proof.
all: ring_simplify_this.
Qed.
Theorem opt_montgomery_0 (n m: nat):
Lemma opt_montgomery_0 (n m: nat):
opt_montgomery n m 0 = 0.
Proof.
rewrite /opt_montgomery.
apply opt_montgomery_rec_0.
Qed.
Local Lemma p_x0_0_impl : forall (p: mc M),
p #x0 = 0%:R ->
p = MC (oncurve_0_0 M) \/ p = MC (oncurve_inf M).
Proof.
move => [] [Hp|xp yp Hp] => /= Hxp.
+ by right ; apply mc_eq.
+ left; apply mc_eq.
move: Hxp Hp -> => /=.
rewrite ?exprS ?expr0 ?mulr1 ?mulr0 ?addr0.
have/eqP := M.(pB) => Hb.
rewrite mulf_eq0.
move /orP => [].
by move/eqP.
by rewrite mulf_eq0; move /orP => []/eqP ->.
Qed.
Lemma p_x0_0_eq_0 : forall (n:nat) (p: mc M),
p #x0 = 0%:R ->
(p *+ n) #x0 = 0%R.
Proof.
elim => [| n IHn] => p.
move => _ ; rewrite mulr0n => //=.
rewrite mulrS => Hp.
have /IHn/p_x0_0_impl := Hp.
move => [] ->.
all: move/p_x0_0_impl:Hp.
all: move => [] ->.
all: rewrite /GRing.add //=.
rewrite eq_refl => //=.
Qed.
Lemma 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.
Proof.
have /orP[Hx|Hx] := orNb (x == 0) => Hn.
apply opt_montgomery_x => //.
move/eqP: Hx => -> => p.
move/(p_x0_0_eq_0 n) => ->.
apply opt_montgomery_0.
Qed.
End OptimizedLadder.
......@@ -45,10 +45,10 @@ Definition twist25519_ladder n x :=
Local Notation "p '#x0'" := (point_x0 p) (at level 30).
Theorem twist25519_ladder_ok (n : nat) x :
(n < 2^255)%nat -> x != 0 ->
(n < 2^255)%nat ->
forall (p : mc twist25519_mcuType), p#x0 = x -> twist25519_ladder n x = (p *+ n)#x0.
Proof.
move => Hn Hx p Hp.
move => Hn p Hp.
rewrite /twist25519_ladder.
apply opt_montgomery_ok => //=.
rewrite /a.
......
......@@ -127,16 +127,16 @@ Local Notation "p '/p'" := (tFp_to_Fp2 p) (at level 40).
From mathcomp Require Import ssrnat.
Theorem twist25519_ladder_really_ok (n : nat) x :
(n < 2^255)%nat -> x != 0 ->
(n < 2^255)%nat ->
forall (p : mc twist25519_mcuType),
twist25519_Fp_to_Fp2 p #x0 = Zmodp2.Zmodp2 x 0 ->
twist25519_ladder n x = ((twist25519_Fp_to_Fp2 p) *+ n)#x0 /p.
Proof.
move => Hn Hx p Hp.
move => Hn p Hp.
have Hp' := tFp_to_Fp2_cancel p.
have Hp'' : p #x0 = x.
rewrite Hp' Hp //.
rewrite (twist25519_ladder_ok n x Hn Hx p Hp'').
rewrite (twist25519_ladder_ok n x Hn p Hp'').
rewrite -nP_is_nP2.
rewrite tFp_to_Fp2_cancel //.
Qed.
......
\section{Mathematical Model}
In this section we extend the work of Bartzia and Strub \cite{DBLP:conf/itp/BartziaS14}
to support Montgomery curves. We also prove that the montgomery ladder computes
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
the x-coordinate of scalar multiplication over \F{p^2}
(Theorem 2.1 by Bernstein \cite{Ber06}) where $p$ is the prime \p.
\subsection{Formalization of Elliptic Curves}
In this section, we consider elliptic curves over a field \K. We assume that the
characteristic of \K is neither 2 or 3.
We consider elliptic curves over a field \K. We assume that the
characteristic of \K\ is neither 2 or 3.
\textbf{Definition 1.}
For a field \K, using an appropriate choice of coordinates, an elliptic curve \E\
is a plane cubic albreaic curve $\E(x,y)$ defined by an equation of the form:
$$\E : y^2 + a_1 xy + a_3 y = x^3 + a_2 x^2 + a_4 x + a_6$$
\begin{definition}
Let a field \K, using an appropriate choice of coordinates, an elliptic curve $E$
is a plane cubic albreaic curve $E(x,y)$ defined by an equation 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, 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\}$$
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\}$$
\end{definition}
\subsubsection{Weierstra{\ss} curves}
\label{Weierstrass}
This equation $E(x,y)$ can be reduced into its Weierstra{\ss} form.
In this case, this equation $\E(x,y)$ can be reduced into its Weierstrass form:
$$y^2 = x^3 + ax + b$$
Moreover, such curve does not present any singularity if
$\Delta(a,b) = 4a^3 + 27b^2$ is not equal to $0$.
\begin{definition}
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 the set of all points $(x,y) \in \K^2$ satisfying the equation:
$$y^2 = x^3 + ax + b,$$
along with an additional formal point \Oinf, ``at infinity''. Such curve does not present any singularity.
\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
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 prof that $\Delta(a,b) \neq 0$.
along with the proof that $\Delta(a,b) \neq 0$.
\begin{lstlisting}[language=Coq]
Record ecuType :=
{ A : K; B : K; _ : 4 * A^3 + 27 * B^2 != 0}.
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
......@@ -51,22 +60,329 @@ Points of an elliptic curve can be equiped with a structure of an abelian group.
\end{itemize}
This operaction can be defined in Coq as follow:
\begin{coq}
\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
| EC_Inf , _ => p2
| _ , EC_Inf => p1
| \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{coq}
\end{lstlisting}
And is proven internal to the curve (with coercion):
\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}
\label{montgomery}
Computation over elliptic curves are hard. Speedups can be obtained by using
homogeneous coordinates and other forms than the Weierstra{\ss} form. We consider
the Montgomery form \cite{MontgomerySpeeding}.
\begin{definition}
Let $a \in \K \backslash \{-2, 2\}$, and $b \in \K \backslash \{ 0\}$. The \textit{Montgomery curve} $M_{a,b}$ is the set of all points $(x,y) \in \K^2$ satisfying the equation:
$$by^2 = x^3 + ax^2 + x,$$
along with an additional formal point \Oinf, ``at infinity''.
\end{definition}
Using a similar representation, we defined the parametric type \texttt{mc} which
represent the points on a specific montgomery curve. It is parametrized by
a \texttt{K : ecuFieldType} -- the type of fields which characteristic is not 2 or 3 --
and \texttt{M : mcuType} -- a record that packs the curve paramaters $a$ and $b$
along with the proofs that $b \neq 0$ and $a^2 != 4$.
\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}
We define the addition on Montgomery curves the same way as it it is in the Weierstra{\ss} form,
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}$ be a Mongomery curve, Define $$a' = \frac{3-a^2}{3b^2} \text{\ \ \ \ and\ \ \ \ } b' = \frac{2a^3 - 9a}{27b^3}.$$
Then $E_{a',b'}$ is an elliptic curve, and the mapping $\varphi : M_{a,b} \mapsto E_{a',b'}$ 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}
\label{projective}
Points on a projective plane are represented with a triple $(X, Y, Z)$. Any points except $(0,0,0)$ defines a point on a projective plane. A scalar multiple of a point defines the same point, \ie
for all $\alpha \neq 0$, $(X,Y,Z)$ and $(\alpha X, \alpha Y, \alpha Z)$ defines the same point. The projective point $(X,Y,Z)$ corresponds to the point $(X/Z,Y/Z)$ on the Euclidian plane, likewise the point $(X,Y)$ on the Euclidian plane corresponds to $(X , Y, 1)$ on the projective plane.
We can write the equation for a Montgomery curve $M_{a,b}$ as such:
\begin{equation}
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)
\end{equation}
Multiplying both sides by $Z^3$ yields:
\begin{equation}
b Y^2Z = X^3 + a X^2Z + XZ^2
\end{equation}
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$.
By restristing the parameter $a$ of $M_{a,b}$ such that $a^2-4$ is not a square in \K, we ensure that $(0,0)$ is the only point with a $y$-coordinate of $0$.
With those coordinates we prove the following lemmas for the addition of two points.
\begin{lemma}
\label{lemma-add}
Define a function $\chi : M_{a,b} \to \K \cup \{\infty\}$ as $\chi(\Oinf) = \infty$ and $\chi((x,y)) = x$. Let $M_{a,b}$ 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$.
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}$ 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}
\label{lemma-double}
Define a function $\chi : M_{a,b} \to \K \cup \{\infty\}$ as $\chi(\Oinf) = \infty$ and $\chi((x,y)) = x$. Let $M_{a,b}$ 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
\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$ on $M_{a,b}$ such that $X_1/Z_1 = \chi(P_1)$, we have $X_3/Z_3 = \chi(2P_1)$.
\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}
With these two lemmas (\ref{lemma-add} and \ref{lemma-double}), we have the basic tools to compute efficiently additions and point doubling on projective coordinates.
\subsubsection{Scalar Multiplication Algorithms}
\label{ladder}
Suppose we have a scalar $n$ and a point $P$ on some curve. The most straightforward way to compute $nP$ 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.
\eg for $n=11$, we compute $2(2(2(2\Oinf + P)) + P)+ P$.
\begin{algorithm}[H]
\caption{Double-and-add for scalar mult.}
\label{double-add}
\begin{algorithmic}
\REQUIRE{Point $P$, scalars $n$ and $m$, $n < 2^m$}
\ENSURE{$Q = nP$}
\STATE $Q \leftarrow \Oinf$
\FOR{$k$ := $m$ downto $1$}
\STATE $Q \leftarrow 2Q$
\IF{$k^{\text{th}}$ bit of $n$ is $1$}
\STATE $Q \leftarrow Q + P$
\ENDIF
\ENDFOR
\end{algorithmic}
\end{algorithm}
\begin{lemma}
\label{lemma-double-add}
Algorithm \ref{double-add} is correct, \ie it respects its output conditions given the input conditions.
\end{lemma}
We prove Lemma \ref{lemma-double-add}. However with careful timing, an attacker could reconstruct $n$.
In the case of Curve25519, $n$ is the private key. With the Montgomery's ladder, while it provides slightly more computations and an extra variable, we can prevent the previous weakness.
See Algorithm \ref{montgomery-ladder}.
\begin{algorithm}[H]
\caption{Montgomery ladder for scalar mult.}
\label{montgomery-ladder}
\begin{algorithmic}
\REQUIRE{Point $P$, scalars $n$ and $m$, $n < 2^m$}
\ENSURE{$Q = nP$}
\STATE $Q \leftarrow \Oinf$
\STATE $R \leftarrow P$
\FOR{$k$ := $m$ downto $1$}
\IF{$k^{\text{th}}$ bit of $n$ is $0$}
\STATE $R \leftarrow Q + R$
\STATE $Q \leftarrow 2Q$
\ELSE
\STATE $Q \leftarrow Q + R$
\STATE $R \leftarrow 2R$
\ENDIF
\ENDFOR
\end{algorithmic}
\end{algorithm}
\begin{lemma}
\label{lemma-montgomery-ladder}
Algorithm \ref{montgomery-ladder} is correct, \ie it respects its output conditions given the input conditions.
\end{lemma}
In Curve25519 we are only interested in the $x$ coordinate of points, using Lemmas \ref{lemma-add} and \ref{lemma-double}, and replacing the if statements with conditional swapping we can define a ladder similar to the one used in TweetNaCl. See Algorithm \ref{montgomery-double-add}
\begin{algorithm}[H]
\caption{Montgomery ladder for scalar multiplication on $M_{a,b}$ with optimizations}
\label{montgomery-double-add}
\begin{algorithmic}
\REQUIRE{$x \in \K\backslash \{0\}$, scalars $n$ and $m$, $n < 2^m$}
\ENSURE{$a/c = \chi(nP)$ for any $P$ such that $\chi(P) = x$}
\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}
\label{lemma-montgomery-double-add}
Algorithm \ref{montgomery-double-add} is correct, \ie it respects its output conditions given the input conditions.
\end{lemma}
We formalized of this lemma (\ref{lemma-montgomery-double-add}):
\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}$, we have:
$$\forall P, P + \Oinf\ = P$$
thus we derive the following lemma and thus the theorem of the correctness of our ladder.
\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.
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{Curve and Twists}
......
......@@ -1117,3 +1117,15 @@ VeriSmall: Verified Smallfoot Shape Analysis, by Andrew W. Appel. In CPP 2011: F
pages = {77-92},
note = {\url{https://hal.inria.fr/hal-01102288}}
}
@article{MontgomerySpeeding,
author = {Peter L. Montgomery},
title = {Speeding the Pollard and Elliptic Curve Methods of Factorization. Math. Comp. 48, 243-264},