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

more of Joost feedback

parent 24c1c7db
......@@ -117,9 +117,9 @@ than the Weierstra{\ss} form. We consider the Montgomery form \cite{MontgomerySp
\begin{dfn}
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:
The \textit{elliptic curve} $M_{a,b}$ is defined by the equation:
$$by^2 = x^3 + ax^2 + x,$$
$M_{a,b}(\K)$ is the set of all points $(x,y) \in \K^2$ satisfying the $M_{a,b}$
along with an additional formal point $\Oinf$, ``at infinity''.
\end{dfn}
Similar to the definition of \texttt{ec}, we defined the parametric type \texttt{mc} which
......@@ -166,10 +166,10 @@ We then define a bijection between a Montgomery curve and its short Weierstra{\s
In this way we get associativity of addition on Montgomery curves from the
corresponding property for Weierstra{\ss} curves.
\begin{lemma}
Let $M_{a,b}(\K)$ be a Montgomery curve, define
Let $M_{a,b}$ 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:
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) ) &= \left( \frac{x}{b} + \frac{a}{3b} , \frac{y}{b} \right)
......@@ -204,7 +204,7 @@ For $Z\neq 0$, the projective point $(X:Y:Z)$ corresponds to the
point $(X/Z,Y/Z)$ on the affine plane. Likewise the point $(X,Y)$ on the
affine plane corresponds to $(X:Y:1)$ on the projective plane.
Using fractions as coordinates, the equation for a Montgomery curve $M_{a,b}(\K)$
Using fractions as coordinates, the equation for a Montgomery curve $M_{a,b}$
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)$$
Multiplying both sides by $Z^3$ yields:
......@@ -232,7 +232,7 @@ We define $\chi$ and $\chi_0$ to return the \xcoord of points on a curve.
Using projective coordinates we prove the formula for differential addition (\lref{lemma:xADD}).
\begin{lemma}
\label{lemma:xADD}
Let $M_{a,b}(\K)$ be a Montgomery curve such that $a^2-4$ is not a square, and
Let $M_{a,b}$ be a Montgomery curve such that $a^2-4$ is not a square in \K, and
let $X_1, Z_1, X_2, Z_2, X_4, Z_4 \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
......@@ -240,7 +240,7 @@ Define
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
then for any point $P_1$ and $P_2$ in $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:}
......@@ -251,14 +251,14 @@ If $x\ne 0$ then we define $x/0 = \infty$.
Similarly we also prove the formula for point doubling (\lref{lemma:xDBL}).
\begin{lemma}
\label{lemma:xDBL}
Let $M_{a,b}(\K)$ be a Montgomery curve such that $a^2-4$ is not a square, and
Let $M_{a,b}$ be a Montgomery curve such that $a^2-4$ is not a square in \K, and
let $X_1, Z_1 \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}(\K)$ such that $X_1/Z_1 = \chi(P_1)$,
then for any point $P_1$ in $M_{a,b}(\K)$ such that $X_1/Z_1 = \chi(P_1)$,
we have $X_3/Z_3 = \chi(2P_1)$.
\end{lemma}
......@@ -370,8 +370,8 @@ Theorem opt_montgomery_ok (n m: nat) (x : K) :
To be able to use the above theorem we need to satisfy 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.$$
If we consider the quadratic extension field $\F{p^2}$,
there exists $x$ such that $x^2 = a^2-4$, preventing use \tref{thm:montgomery-ladder-correct}
There always exists $x \in \F{p^2}$ such that $x^2 = a^2-4$,
preventing the use \tref{thm:montgomery-ladder-correct}
with $\K = \F{p^2}$.
We first study Curve25519 and one of its quadratic twists Twist25519, both defined
......@@ -399,10 +399,10 @@ Coercion repr (x : type) : Z :=
\end{lstlisting}
We define the basic operations ($+, -, \times$) with their respective neutral
elements ($0, 1$) and prove \lref{lemma:Zmodp_ring}.
elements ($0, 1$) and prove \lref{lemma:Zmodp_field}.
\begin{lemma}
\label{lemma:Zmodp_ring}
$\F{p}$ is a commutative ring.
\label{lemma:Zmodp_field}
$\F{p}$ is a commutative field.
\end{lemma}
For $a = 486662$, by using the Legendre symbol we prove that
$a^2 - 4$ and $2$ are not squares in $\F{p}$.
......@@ -510,10 +510,10 @@ $\F{p^2}\backslash\{0\}$, there exists a multiplicative inverse.
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}
Similarly as in $\F{p}$, we define $0^{-1} = 0$ and prove \lref{lemma:Zmodp2_ring}.
Similarly as in $\F{p}$, we define $0^{-1} = 0$ and prove \lref{lemma:Zmodp2_field}.
\begin{lemma}
\label{lemma:Zmodp2_ring}
$\F{p^2}$ is a commutative ring.
\label{lemma:Zmodp2_field}
$\F{p^2}$ is a commutative field.
\end{lemma}
%% TOO LONG
......@@ -584,7 +584,7 @@ Notice that:
\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}(\F{p})$ or $M_{486662,2}(\F{p})$, $Curve25519\_Fp$
in $M_{486662,1}(\F{p})$ or $M_{486662,2}(\F{p})$, $Curve25519\_Fp$
computes the $\chi_0(n \cdot P)$.
We 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}$.
......
Markdown is supported
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