Commit dda26b57 authored by Timmy Weerwag's avatar Timmy Weerwag
Browse files

Some improvements to section V

parent cae3b1c7
......@@ -30,18 +30,18 @@ correctness of the ladder (\ref{subsec:ECC-ladder}).
We discuss the twist of Curve25519 (\ref{subsec:Zmodp}) and explain how we deal
with it in the proofs (\ref{subsec:curvep2}).
\subsection{Formalization of elliptic Curves}
\subsection{Formalization of elliptic curves}
\label{subsec:ECC}
\fref{tikz:ProofHighLevel1} presents the structure of the proof of the ladder's
correctness. The white tiles are definitions, the orange ones are hypothesis and
the green tiles represent major lemmas and theorems.
We consider elliptic curves over a field $\K$. We assume that the
characteristic of $\K$ is neither 2 or 3.
We formalize the Montgomery curves ($M_{a,b}(\K)$), then by using the equivalent
Weierstra{\ss} form ($E_{a',b'}(\K)$) from the library of Bartzia and Strub, we prove
that $M_{a,b}(\K)$ forms an associative finite group. Under the hypothesis that
The plan is as follows.
We consider the field $\K$ and formalize the Montgomery curves ($M_{a,b}(\K)$).
Then, by using the equivalent Weierstra{\ss} form ($E_{a',b'}(\K)$) from the library of Bartzia and Strub,
we prove that $M_{a,b}(\K)$ forms an abelian group.
Under the hypothesis that
$a^2 - 4$ is not a square in $\K$, we prove the correctness of the ladder (\tref{thm:montgomery-ladder-correct}).
\begin{figure}[h]
......@@ -51,8 +51,6 @@ $a^2 - 4$ is not a square in $\K$, we prove the correctness of the ladder (\tref
\label{tikz:ProofHighLevel1}
\end{figure}
We now turn our attention to the details of the proof of the ladder's correctness.
\begin{dfn}
Given a field $\K$,
using an appropriate choice of coordinates,
......@@ -68,20 +66,21 @@ We now turn our attention to the details of the proof of the ladder's correctnes
\subsubsection{Short Weierstra{\ss} curves}
\label{subsec:ECC-Weierstrass}
This equation $E(x,y)$ can be reduced into its short Weierstra{\ss} form.
For the remainder of this text, we assume that the characteristic of $\K$ is neither 2 nor 3.
Then, this equation $E(x,y)$ can be reduced into its short Weierstra{\ss} form.
\begin{dfn}
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 defined by the equation:
The \textit{elliptic curve} $E_{a,b}$ is defined by the equation
$$y^2 = x^3 + ax + b.$$
$E_{a,b}(\K)$ is the set of all points $(x,y) \in \K^2$ satisfying the $E_{a,b}$
along with an additional formal point $\Oinf$, ``at infinity''. Such a curve does not have any singularity.
\end{dfn}
In this setting, Bartzia and Strub defined the parametric type \texttt{ec} which
represent the points on a specific curve. It is parameterized by
a \texttt{K : ecuFieldType} --- the type of fields whose characteristic is not 2 or 3 ---
and \texttt{E : ecuType} --- a record that packs the curve parameters $a$ and $b$
represents the points on a specific curve. It is parameterized by
a \texttt{K : ecuFieldType}, the type of fields whose characteristic is neither 2 nor 3,
and \texttt{E : ecuType}, a record that packs the curve parameters $a$ and $b$
along with the proof that $\Delta(a,b) \neq 0$.
\begin{lstlisting}[language=Coq]
Inductive point := EC_Inf | EC_In of K * K.
......@@ -97,12 +96,16 @@ Definition oncurve (p : point) :=
Inductive ec : Type := EC p of oncurve p.
\end{lstlisting}
Points on an elliptic curve are equipped with the structure of an abelian group.
Points on an elliptic curve form an abelian group when equipped with the following structure.
\begin{itemize}
\item The negation of a point $P = (x,y)$ is defined by reflection over the $x$ axis $-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 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, Q \in E_{a,b}(\K) \setminus \{\Oinf\}$ with $P \neq Q$ and $P \neq -Q$
is defined as the negation of the third intersection point of the line through $P$ and $Q$.
In case $P = Q$, we either use the line tangent to $P$ if $P$ is not an inflection point,
and define $P + Q = -P = -Q$ otherwise.
In case $P = -Q$, we define $P + Q = \Oinf$.
\item The point $\Oinf$ acts as the neutral element. Hence, we define $-\Oinf = \Oinf$,
$P + \Oinf = P$ and $\Oinf + P = P$.
\end{itemize}
These operations are defined in Coq as follows (where we omit the code for the tangent case):
\begin{lstlisting}[language=Coq]
......@@ -141,11 +144,11 @@ than the Weierstra{\ss} form. We consider the Montgomery form \cite{MontgomerySp
$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
Similar to the definition of \texttt{ec}, we define the parametric type \texttt{mc} which
represents the points on a specific Montgomery curve.
It is parameterized by
a \texttt{K : ecuFieldType} --- the type of fields whose characteristic is not
2 or 3 --- and \texttt{M : mcuType} --- a record that packs the curve
a \texttt{K : ecuFieldType}, the type of fields whose characteristic is neither
2 nor 3, and \texttt{M : mcuType}, a record that packs the curve
parameters $a$ and $b$ along with the proofs that $b \neq 0$ and $a^2 \neq 4$.
\begin{lstlisting}[language=Coq,belowskip=-0.1 \baselineskip]
Record mcuType :=
......@@ -182,21 +185,26 @@ Definition addmc (p1 p2 : mc) : mc :=
MC p1 p2 (addO p1 p2)
\end{lstlisting}
We then define a bijection between a Montgomery curve and its short Weierstra{\ss} form
(\lref{lemma:bij-ecc}).
In this way we get associativity of addition on Montgomery curves from the
corresponding property for Weierstra{\ss} curves.
Remarkably, of all the group properties, associativity is the hardest one to prove for elliptic curves.
Instead of reproving this property for Montgomery curves, we transfer it from the Weierstra{\ss} curves
with a trick.
We define a bijection between a Montgomery curve and its short Weierstra{\ss} form
(as in \lref{lemma:bij-ecc})
and prove that it respects the addition as defined on the respective curves.
It is then easy to verify all the group laws for Montgomery curves from the Weierstra{\ss} ones.
After we have verified the group properties, it follows that the bijection is a group isomorphism.
\begin{lemma}
\label{lemma:bij-ecc}
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'}$ is an elliptic curve, and the mapping
$\varphi : M_{a,b} \mapsto E_{a',b'}$ defined as:
then $E_{a',b'}$ is a Weierstra{\ss} curve, and the mapping
$\varphi : M_{a,b} \to 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)
\end{align*}
is an isomorphism between elliptic curves.
is a group isomorphism between elliptic curves.
\end{lemma}
% \begin{lstlisting}[language=Coq,belowskip=-0.25 \baselineskip]
% Definition ec_of_mc_point p :=
......@@ -214,32 +222,32 @@ corresponding property for Weierstra{\ss} curves.
% Lemma ec_of_mc_bij : bijective ec_of_mc.
% \end{lstlisting}
\subsubsection{Projective coordinates}
\subsubsection{Homogeneous coordinates}
\label{subsec:ECC-projective}
In a projective plane, points are represented with triples $(X:Y:Z)$,
with the exception of $(0:0:0)$.
Scalar multiples are representing the same point, \ie
In a projective plane, points are represented by the triples $(X:Y:Z)$ excluding $(0:0:0)$.
Scalar multiples of triples are identified with eachother, \ie
for all $\lambda \neq 0$, the triples $(X:Y:Z)$ and $(\lambda X:\lambda Y:\lambda Z)$ represent
the same point.
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.
the same point in the projective plane.
For $Z\neq 0$, the point $(X:Y:Z)$ corresponds to the
point $(X/Z,Y/Z)$ in the affine plane.
Likewise, the point $(X,Y)$ in the affine plane corresponds to $(X:Y:1)$ in the projective plane.
The points $(X : Y : 0)$ can be considered as points at infinity.
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:
$$b Y^2Z = X^3 + a X^2Z + XZ^2$$
With this equation we can additionally represent the ``point at infinity''. By
setting $Z=0$, we derive $X=0$, giving us the ``infinite point'' $(0:1:0)$.
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
$$b Y^2Z = X^3 + a X^2Z + XZ^2.$$
Setting $Z = 0$ in this equation, we derive $X = 0$.
Hence, $(0 : 1 : 0)$ is the unique point on the curve at infinity.
By restricting the parameter $a$ of $M_{a,b}(\K)$ such that $a^2-4$ is not a
square in \K (Hypothesis \ref{hyp:a_minus_4_not_square}),
we ensure that $(0,0)$ is the only point with a $y$-coordinate of $0$.
\begin{hypothesis}
\label{hyp:a_minus_4_not_square}
$a^2-4$ is not a square in \K.
The number $a^2-4$ is not a square in \K.
\end{hypothesis}
\begin{lstlisting}[language=Coq]
Hypothesis mcu_no_square :
......@@ -247,16 +255,15 @@ Hypothesis mcu_no_square :
\end{lstlisting}
We define $\chi$ and $\chi_0$ to return the \xcoord of points on a curve.
\begin{dfn}Let $\chi$ and $\chi_0$:\\
\vspace{-1em}
\begin{itemize}
\item[--] $\chi : M_{a,b}(\K) \to \K \cup \{\infty\}$\\
such that $\chi(\Oinf) = \infty$ and $\chi((x,y)) = x$.
\item[--] $\chi_0 : M_{a,b}(\K) \to \K$\\
such that $\chi_0(\Oinf) = 0$ and $\chi_0((x,y)) = x$.
\end{itemize}
\begin{dfn}
Let $\chi : M_{a,b}(\K) \to \K \cup \{\infty\}$ and $\chi_0 : M_{a,b}(\K) \to \K$ such that
\begin{align*}
\chi((x,y)) &= x, & \chi(\Oinf) &= \infty, &&\text{and} \\
\chi_0((x,y)) &= x, & \chi_0(\Oinf) &= 0.
\end{align*}
\end{dfn}
Using projective coordinates we prove the formula for differential addition.% (\lref{lemma:xADD}).
Using homogeneous coordinates we prove the formula for differential addition.% (\lref{lemma:xADD}).
\begin{lemma}
\label{lemma:xADD}
Let $M_{a,b}$ be a Montgomery curve such that $a^2-4$ is not a square in \K, and
......@@ -274,7 +281,7 @@ Using projective coordinates we prove the formula for differential addition.% (\
These definitions should be understood in $\K \cup \{\infty\}$.
If $x\ne 0$ then we define $x/0 = \infty$.
\end{lemma}
Similarly we also prove the formula for point doubling.% (\lref{lemma:xDBL}).
Similarly, we also prove the formula for point doubling.% (\lref{lemma:xDBL}).
\begin{lemma}
\label{lemma:xDBL}
Let $M_{a,b}$ be a Montgomery curve such that $a^2-4$ is not a square in \K, and
......@@ -289,7 +296,7 @@ Similarly we also prove the formula for point doubling.% (\lref{lemma:xDBL}).
\end{lemma}
With \lref{lemma:xADD} and \lref{lemma:xDBL}, we are able to compute efficiently
differential additions and point doublings using projective coordinates.
differential additions and point doublings using homogeneous coordinates.
\subsubsection{Scalar multiplication algorithms}
\label{subsec:ECC-ladder}
......@@ -352,10 +359,10 @@ The white tiles are definitions while green tiles are important lemmas and theor
\label{tikz:ProofHighLevel2}
\end{figure}
A brief overview of the complete proof of is described bellow.
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}$.
Subsquently we show that neither $2$ nor $a^2 - 2$ are square in $\F{p}$.
Subsequently, we show that neither $2$ nor $a^2 - 2$ are 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 exist 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})$.
......@@ -518,7 +525,7 @@ of formulas by using rewrite rules:
\end{equation*}
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.
$0, 1, +, -, \times$. Thus $(a,0)$ can be abbreviated as $a$ without confusion.
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
......@@ -551,25 +558,25 @@ We now study the case of the scalar multiplication and show similar proofs.
\begin{lemma}
\label{lemma:proj}
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:
$M_{486662,1}(\F{p})$ (respectively on the quadratic twist $M_{486662,2}(\F{p})$), we have
\begin{align*}
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)
P &\in M_{486662,1}(\F{p}) & \implies \varphi_c(n \cdot P) &= n \cdot \varphi_c(P), &&\text{and} \\
P &\in M_{486662,2}(\F{p}) & \implies \varphi_t(n \cdot P) &= n \cdot \varphi_t(P).
\end{align*}
\end{lemma}
Notice that:
Notice that
\begin{align*}
\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)
\forall P \in M_{486662,1}(\F{p}), &&\psi(\chi_0(\varphi_c(P))) &= \chi_0(P), &&\text{and} \\
\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}$
In summary, for all $n \in \N$, $n < 2^{255}$, for any point $P\in\F{p}\times\F{p}$
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}$
computes $\chi_0(n \cdot P)$.
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 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
Moreover, we have proved that for any point on the curve or the twist, we can compute the
scalar multiplication by $n$ and obtain 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}:
% No: missing uniqueness !
......@@ -589,7 +596,7 @@ computation in $\F{p^2}$.
% curve25519_Fp_ladder n x = (p *+ n)#x0 /p.
% \end{lstlisting}
We then prove the equivalence between of operations in $\Ffield$ and $\Zfield$,
We then prove the equivalence of operations between $\Ffield$ and $\Zfield$,
in other words between \coqe{Zmodp} and \coqe{:GF}.
This allows us to show that given a clamped value $n$ and normalized \xcoord of $P$,
\coqe{RFC} gives the same results as $Curve25519\_Fp$.
......
......@@ -20,7 +20,7 @@
% M is a finite assoc group
\begin{scope}[yshift=0 cm,xshift=3 cm]
\draw [fill=green!20] (0,0) -- (3.25,0) -- (3.25,-0.75) -- (0, -0.75) -- cycle;
\draw (1.675,-0.375) node[textstyle, anchor=center] {$M_{a,b}(\K)$ is an Assoc. Fin. Grp.};
\draw (1.675,-0.375) node[textstyle, anchor=center] {$M_{a,b}(\K)$ is an abelian group};
\end{scope}
% Hypothesis x square is not 2
......
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