Commit 83f8b86b authored by Benoit Viguier's avatar Benoit Viguier
Browse files

Writting in progress

parent 1ec52f01
\subsection*{Abstract}
By using the Coq formal proof assistant with the VST library, we first extend
the work of Bartzia and Strub \cite{DBLP:conf/itp/BartziaS14} to support
By using the Coq formal proof assistant, we first extend
the formalization of elliptic curves of Bartzia and Strub \cite{DBLP:conf/itp/BartziaS14} to support
Montgomery curves. Then with the Verified Software Toolchain \cite{2012-Appel}
we then prove the soundness and correctness of TweetNaCl's Curve25519 implementation
up to the formal definitions of elliptic curves.
we prove the soundness and correctness of TweetNaCl's Curve25519 implementation.
\section{Introduction}
Implementing cryptographic primitives without any bugs is hard.
While tests provides a some code coverage and are used in the limits,
While tests provides a code coverage and are used in the limits,
they still don't cover 100\% of the possible input values.
Using Coq, we prove the correctness of the scalar multiplication in Tweetnacl.
Our method is can be seen as a static analysis over the input values coupled
with the formal proof that the code of the algorithm matches its specification.
TweetNaCl\cite{BGJ+15} is a compact reimplementation of the
NaCl\cite{BLS12} library. It does not aim for high speed
application and has been optimized for source code compactness.
It maintains some degree of readability in order to be
easily auditable.
It maintains some degree of readability in order to be easily auditable.
This library makes use of Curve25519\cite{Ber06}, a function over a \F{p}-restricted
x-coordinate scalar multiplication on $E(\F{p^2})$, where $p$ is the prime number \p
and E is the elliptic curve $y^2 = x^3 + 486662 x^2 + x$.
% It defines the function \texttt{crypto\_scalarmult} which
% takes as input a scalar $n$ and the $x$ coordinate of a
% point $P$ and returns the $x$ coordinate of the
% point $[n]P$.
$x$-coordinate computing a scalar multiplication on $E(\F{p^2})$, where $p$ is the prime number \p
and $E$ is the elliptic curve $y^2 = x^3 + 486662 x^2 + x$.
Coq is a formal system that allows us to machine-check our proofs. The Compcert\cite{Leroy-backend}
compiler and the Verifiable Software Toolchain (VST)\cite{2012-Appel} are build
Coq is a formal system that allows to machine-check our proofs.
A famous example of its use is the proof of the Four Color Theorem.
The Compcert\cite{Leroy-backend} compiler and the Verifiable Software Toolchain (VST)\cite{2012-Appel} are build
on top of it.
Our approach is as follow, we use the \textit{clightgen} tool from Compcert to
generate the \textit{semantic version} (Clight\cite{Blazy-Leroy-Clight-09}) of
the TweetNaCl C code. Using the Separation logic\cite{1969-Hoare,Reynolds02separationlogic}
with (VST) we show that the semantics of the program satisfies a functionnal
specification in Coq. We then prove that this specification represent the scalar
multiplication on Curve25519.
the TweetNaCl C code.
Using the Separation logic\cite{1969-Hoare,Reynolds02separationlogic}
with with the Verifiable Software Toolchain we show that the semantics of the
program satisfies a functionnal specification in Coq.
We extend the work of Bartzia and Strub \cite{DBLP:conf/itp/BartziaS14} to support Montgomery curves.
With this formalization, we prove the correctness of a generic Montgomery ladder
and show that our specification can be seen as an instance of it.
\section{Curve25519 implementation}
\todo[inline]{This part does not really make sens here. Needs to be rewritten.}
To prove the correctness of \texttt{crypto\_scalarmult},
we also need to do the same with all the functions subsequently called:
\texttt{unpack25519}; \texttt{A}; \texttt{Z}; \texttt{M}; \texttt{S};
\texttt{car25519}; \texttt{inv25519}; \texttt{set25519}; \texttt{sel25519};
\texttt{pack25519}.
In this section we present in detail the algorithm computing the crypto scalar multiplication.
We then discuss what will be the required proofs.
\subsection{Implementation} \label{sec:impl}
Curve25519 is defined over \Zfield. Number in that field can
be represented by a 256-bits number. Each of them represented in base $2^{16}$.
they are cut into 16 limbs of at least 16 bits placed into 64-bits signed
container.
Given a natural number $n$ and a value $x \in \F{p}$, Curve25519 is a function over a $\F{p}$-restricted
$x$-coordinate computing a scalar multiplication on $E(\F{p^2})$.
Due to this restriction, all computations are done over $\F{p}$.
Number in that field can be represented by a 256-bits number.
We can represent them in either 8-bit limbs (respectively 16-bit limbs),
making use of a base $2^8$ (respectively $2^{16}$).
As a result, input of the Curve25519 function are seen as arrays of bytes.
Computations inside this function makes use of the 16-bit limbs representation.
Those are placed into 64-bits signed container in order to mitigate overflows or underflows.
\begin{lstlisting}[language=Ctweetnacl]
typedef long long i64;
typedef i64 gf[16];
\end{lstlisting}
This does not guaranty a unique representation of each number. i.e.\\
We notice this does not guaranty a unique representation of each number. i.e.\\
$\exists x,y \in$ \TNaCle{gf} such that
\vspace{-0.25cm}
$$x \neq y\ \ \land\ \ x \equiv y \pmod{2^{255}-19}$$
......@@ -49,19 +50,32 @@ sv M(gf o,const gf a,const gf b) {
To avoid overflows, carries are propagated by the \texttt{car25519} function.
\begin{lstlisting}[language=Ctweetnacl]
sv car25519(gf o) {
sv car25519(gf o)
{
int i;
i64 c;
FOR(i,15) {
o[i]+=(1LL<<16);
c=o[i]>>16;
o[(i+1)*(i<15)]+=c-1+37*(c-1)*(i==15);
o[i]-=c<<16;
FOR(i,16) {
o[(i+1)%16]+=(i<15?1:38)*(o[i]>>16);
o[i]&=0xffff;
}
}
\end{lstlisting}
% In order to simplify the verification of this function,
% we extract the last step of the loop $i = 15$.
% \begin{lstlisting}[language=Ctweetnacl]
% sv car25519(gf o)
% {
% int i;
% i64 c;
% FOR(i,15) {
% o[(i+1)]+=o[i]>>16;
% o[i]&=0xffff;
% }
% o[0]+=38*(o[15]>>16);
% o[15]&=0xffff;
% }
% \end{lstlisting}
At the end of the Mongomery ladder, we have to compute an inverse.
At the end of the Montgomery ladder, we have to compute an inverse.
This is done using the Fermat's little theorem by the exponentiation to
$2^{255}-21$ with the Square-and-multiply algorithm and taking
advantage of the shape of the number.
......@@ -73,15 +87,21 @@ sv inv25519(gf o,const gf a)
set25519(c,a);
for(i=253;i>=0;i--) {
S(c,c);
if(i!=2&&i!=4) M(c,c,a);
if(i!=2 && i!=4) M(c,c,a);
}
FOR(i,16) o[i]=c[i];
}
\end{lstlisting}
The last step of the crypto\_scalarmult is the packing of the limbs, it returns
an array of bytes and guarantees a unique representation in $\mathbb{Z}_{2^{255}-19}$.
The last step of crypto\_scalarmult is the packing of the limbs, it returns
an array of bytes. It first performs 3 carry propagations in order to guarantee
that each 16-bit limbs values are between $0$ and $2^{16}$.
Then it computes a modulo reduction by \p by iterative substraction and
conditional swap until it reaches a negative number.
This guarantees a unique representation in $\mathbb{Z}_{2^{255}-19}$.
After which each 16-bit limbs are splitted into 8-bit limbs.
\begin{lstlisting}[language=Ctweetnacl]
sv pack25519(u8 *o,const gf n)
{
int i,j;
......@@ -109,7 +129,9 @@ sv pack25519(u8 *o,const gf n)
}
\end{lstlisting}
The full Montgomery ladder is defined as follow:
The full Montgomery ladder is defined as follow.
First extract and clamb the value of $n$. Then unpack the value of $p$.
Compute the Montgomery ladder over the clamped $n$ and $p$, pack the result into $q$.
\begin{lstlisting}[language=Ctweetnacl]
int crypto_scalarmult(u8 *q,
const u8 *n,
......@@ -162,10 +184,15 @@ int crypto_scalarmult(u8 *q,
\subsection{What need to be proven?}
Verifying \texttt{crypto\_scalarmult} also implies to verify all the functions
subsequently called: \texttt{unpack25519}; \texttt{A}; \texttt{Z}; \texttt{M};
\texttt{S}; \texttt{car25519}; \texttt{inv25519}; \texttt{set25519}; \texttt{sel25519};
\texttt{pack25519}.
We prove that the implementation of Curve25519 is \textbf{sound} \ie
\begin{itemize}
\item absence of access out-of-bounds of arrays.
\item absence of access out-of-bounds of arrays (memory safety).
\item absence of overflows/underflow on the arithmetic.
\end{itemize}
......@@ -176,11 +203,14 @@ We also prove that TweetNaCl's code is \textbf{correct}:
\item Curve25519 is correctly implemented (we get what we expect).
\item Operations on \texttt{gf} (\texttt{A}, \texttt{Z}, \texttt{M}, \texttt{S})
are equivalent to operations ($+,-,\times,x^2$) in \Zfield.
\item The Montgomery ladder does compute a scalar multiplication between a natural number and a point.
\end{itemize}
In order to prove the soundness and correctness of \texttt{crypto\_scalarmult},
we defined multiples levels of specifications.
A high level specification (over a generic field $\mathbb{F}$) looking only at
we define multiples levels of specifications.
A high level specification (over a generic field $\K$) looking only at
the structure of the Montgomery ladder provided us with the correcntess.
A low level specification close to the \texttt{C} code (over lists of $\mathbb{Z}$)
gave us the soundness assurance.
......
......@@ -27,7 +27,7 @@ $$E(\K) = \{(x,y) \in \K \times \K | E(x,y)\} \cup \{\Oinf\}$$
This equation $E(x,y)$ can be reduced into its Weierstra{\ss} form.
\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:
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:
$$y^2 = x^3 + ax + b,$$
along with an additional formal point \Oinf, ``at infinity''. Such curve does not present any singularity.
\end{definition}
......@@ -91,7 +91,7 @@ homogeneous coordinates and other forms than the Weierstra{\ss} form. We conside
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:
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:
$$by^2 = x^3 + ax^2 + x,$$
along with an additional formal point \Oinf, ``at infinity''.
\end{definition}
......@@ -141,8 +141,8 @@ Definition addmc (p1 p2 : mc) : mc :=
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:
Let $M_{a,b}(\K)$ 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'}(\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} )
......@@ -172,7 +172,7 @@ Lemma ec_of_mc_bij : bijective ec_of_mc.
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. For $Z\neq 0$, 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:
We can write the equation for a Montgomery curve $M_{a,b}(\K)$ 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}
......@@ -182,27 +182,27 @@ 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$.
By restristing the parameter $a$ of $M_{a,b}(\K)$ 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$.
\begin{lstlisting}[language=Coq]
Hypothesis mcu_no_square : forall x : K, x^+2 != (M#a)^+2 - 4%:R.
\end{lstlisting}
With those coordinates we prove the following lemmas for the addition of two points.
\begin{definition}We define the functions $\chi$ and $\chi_0$:\\
-- $\chi : M_{a,b} \to \K \cup \{\infty\}$\\
-- $\chi : M_{a,b}(\K) \to \K \cup \{\infty\}$\\
such that $\chi(\Oinf) = \infty$ and $\chi((x,y)) = x$.\\
-- $\chi_0 : M_{a,b} \to \K$\\
-- $\chi_0 : M_{a,b}(\K) \to \K$\\
such that $\chi_0(\Oinf) = 0$ and $\chi_0((x,y)) = x$.
\end{definition}
\begin{lemma}
\label{lemma-add}
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$.
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$.
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)$.\\
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:
......@@ -240,13 +240,13 @@ then for any point $P_1$ and $P_2$ on $M_{a,b}$ such that $X_1/Z_1 = \chi(P_1),
With those coordinates we also prove a similar lemma for point doubling.
\begin{lemma}
\label{lemma-double}
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
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
\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)$.
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)$.
\end{lemma}
% Which is formalized as follow:
% \begin{lstlisting}[language=Coq]
......@@ -323,7 +323,7 @@ Algorithm \ref{montgomery-ladder} is correct, \ie it respects its output conditi
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}
\caption{Montgomery ladder for scalar multiplication on $M_{a,b}$ with optimizations}
\caption{Montgomery ladder for scalar multiplication on $M_{a,b}(\K)$ with optimizations}
\label{montgomery-double-add}
\begin{algorithmic}
\REQUIRE{$x \in \K\backslash \{0\}$, scalars $n$ and $m$, $n < 2^m$}
......@@ -381,7 +381,7 @@ We can remark that for an input $x = 0$, the ladder returns $0$.
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:
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}
......@@ -395,7 +395,7 @@ Lemma p_x0_0_eq_0 : forall (n : nat) (p : mc M),
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}$,
For all $n, m \in \N$, $x \in \K$, $P \in M_{a,b}(\K)$,
if $\chi_0(P) = x$ then Algorithm \ref{montgomery-double-add} returns $\chi_0(nP)$
\end{theorem}
\begin{lstlisting}[language=Coq]
......@@ -463,18 +463,20 @@ Lemma a_not_square : forall x: Zmodp.type,
Lemma two_not_square : forall x : Zmodp.type,
x^+2 != 2%:R.
\end{lstlisting}
We consider $M_{486662,1}$ and $M_{486662,2}$ over \F{p}. $M_{486662,1}$ has the same equation as Curve25519 while $M_{486662,2}$ is ome of its quadratic twist.
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.
By instanciating theorem \ref{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}$ and $\chi_0(P) = x$.
such that $P \in M_{486662,1}(\F{p})$ and $\chi_0(P) = x$.
Given $n$ and $x$, $Curve25519\_Fp(n,x) = \chi_0(nP)$.
\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}$ and $\chi_0(P) = x$.
such that $P \in M_{486662,2}(\F{p})$ and $\chi_0(P) = x$.
Given $n$ and $x$, $Twist25519\_Fp(n,x) = \chi_0(nP)$.
\end{lemma}
As the Montgomery ladder defined above does not depends on $b$, it is trivial to see that the computations done for points of $M_{486662,1}$ and of $M_{486662,2}$ are the same.
As the Montgomery ladder defined above does not depends 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.
\begin{lstlisting}[language=Coq]
Theorem curve_twist_eq: forall n x,
curve25519_Fp_ladder n x = twist25519_Fp_ladder n x.
......@@ -489,7 +491,7 @@ $$y^2 = x\ \ \ \lor\ \ 2y^2 = x$$
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}$ or over $M_{486662,2}$ such that the $x$-coordinate of $P$ is $x$.
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{coq}
Theorem x_is_on_curve_or_twist: forall x : Zmodp.type,
......@@ -499,9 +501,8 @@ Theorem x_is_on_curve_or_twist: forall x : Zmodp.type,
\subsubsection{Curve25519 over \F{p^2}}
We use the same definitions as in \cite{Ber06} and we consider the extension field \F{p^2} as the set $\F{p} \times \F{p}$. We prove that two is not a square and...
In a similar way as for \F{p} we use Module in Coq.
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]
Module Zmodp.
Inductive type :=
......@@ -552,8 +553,8 @@ 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}$ over $\F{p^2}$. With the rewrite rule above, it is straightforward to prove that any point on the curve $M_{486662,1}$ over $\F{p}$ is also on the curve $M_{486662,1}$ over $\F{p^2}$. Similarily, any point on the quadratic twist $M_{486662,2}$ over $\F{p}$ is also on the curve $M_{486662,1}$.
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}$ such that $\chi_0(P)$ is $(x,0)$
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})$.
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:
......@@ -574,24 +575,24 @@ Define the functions $\varphi_c$, $\varphi_t$ and $\psi$\\
\end{definition}
\begin{lemma}
For all $n \in \N$, for all point $P\in\F{p}\times\F{p}$ on the curve $M_{486662,1}$ (respectively on the quadratic twist $M_{486662,2}$), we have:
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} &\implies \varphi_c(n \cdot P) = n \cdot \varphi_c(P)\\
P \in M_{486662,2} &\implies \varphi_t(n \cdot P) = n \cdot \varphi_t(P)
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}, \psi(\chi_0(\varphi_c(P))) = \chi_0(P)\\
\forall P \in M_{486662,2}, \psi(\chi_0(\varphi_t(P))) = \chi_0(P)\\
\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*}
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}$ or $M_{486662,2}$ \texttt{curve25519\_Fp\_ladder} computes the $\chi_0(nP)$.
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(nP)$.
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}
For all $n \in \N$, $x \in \F{P}$, $P \in M_{486662,1}$, such that $n < 2^{255}$ and $\chi_0(P) = \varphi(x)$, \texttt{curve25519\_Fp\_ladder}$(n, x)$ computes $\psi(\chi_0(nP))$.
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(nP))$.
\end{theorem}
which can be formalized in Coq as:
\begin{lstlisting}[language=Coq]
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment