Commit cdab911c authored by Freek Wiedijk's avatar Freek Wiedijk
Browse files

More changes to chapter 5.

parent 8332bb44
......@@ -197,8 +197,8 @@ Lemma ec_of_mc_bij : bijective ec_of_mc.
\subsubsection{Projective coordinates}
\label{subsec:ECC-projective}
On a projective plane, points are represented with a triple $(X:Y:Z)$.
With the exception of $(0:0:0)$, any point can be projected.
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
for all $\lambda \neq 0$, the triples $(X:Y:Z)$ and $(\lambda X:\lambda Y:\lambda Z)$ represent
the same point.
......@@ -235,7 +235,7 @@ Using projective coordinates we prove the formula for differential addition (\lr
\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 $X_1, Z_1, X_2, Z_2, X_3, Z_3 \in \K$, such that $(X_1,Z_1) \neq (0,0)$,
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
\begin{align*}
......@@ -245,13 +245,16 @@ Z_3 &= X_4((X_1 - Z_1)(X_2+Z_2) - (X_1+Z_1)(X_2-Z_2))^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$.
\textbf{Remark:}
%For any $x \in \K \backslash\{0\}, x/0$ should be understood as $\infty$.
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 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}(\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
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\\
......@@ -262,15 +265,21 @@ we have $X_3/Z_3 = \chi(2P_1)$.
\end{lemma}
With \lref{lemma:xADD} and \lref{lemma:xDBL}, we are able to compute efficiently
differential additions and point doubling on projective coordinates.
differential additions and point doublings using projective coordinates.
\subsubsection{Scalar multiplication algorithms}
\label{subsec:ECC-ladder}
By taking \aref{alg:montgomery-ladder} and replacing \texttt{xDBL} and \texttt{xADD}
with their respective formula (\lref{lemma:xADD} and \lref{lemma:xDBL}),
we define a generic ladder \coqe{opt_montgomery} similar to the one used in
TweetNaCl. We prove its correctness for any points which \xcoord is not 0.
we define a ladder \coqe{opt_montgomery} (in which $\K$ has not been fixed yet),
similar to the one used in
TweetNaCl.
(This definition is closely related to \coqe{montgomery_rec} that was used
in the definition of \coqe{RFC}, and is easily proved the same.)
%\ref to the def of montgomery_rec? relevant lemma(s) that show(s) these are "the same"?
We prove its correctness for any points which \xcoord is not 0.
% By taking \aref{alg:montgomery-ladder} and replacing \texttt{xDBL} and \texttt{xADD}
......@@ -336,14 +345,14 @@ 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}(\K)$, we have:
$$\forall P, P + \Oinf\ = P$$
thus we derive the following lemma.
Also \Oinf\ is the neutral element of $M_{a,b}(\K)$.
%$$\forall P, P + \Oinf\ = P$$
%thus we derive the following lemma.
\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.
\end{lstlisting}
And thus the theorem of the correctness of the Montgomery ladder.
This gives us the theorem of the correctness of the Montgomery ladder.
\begin{theorem}
\label{thm:montgomery-ladder-correct}
For all $n, m \in \N$, $x \in \K$, $P \in M_{a,b}(\K)$,
......@@ -362,11 +371,11 @@ 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$$
As we consider the quadratic extension field $\F{p^2}$,
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}
with $\K = \F{p^2}$.
We first study Curve25519 and one of the quadratic twist Twist25519, both defined
We first study Curve25519 and one of its quadratic twists Twist25519, both defined
over \F{p}.
\subsubsection{Curves and twists}
......@@ -396,7 +405,7 @@ elements ($0, 1$) and prove \lref{lemma:Zmodp_ring}.
\label{lemma:Zmodp_ring}
$\F{p}$ is a commutative ring.
\end{lemma}
And finally for $a = 486662$, by using the Legendre symbol we prove that
For $a = 486662$, by using the Legendre symbol we prove that
$a^2 - 4$ and $2$ are not squares in $\F{p}$.
\begin{lstlisting}[language=Coq]
Fact a_not_square : forall x: Zmodp.type,
......@@ -406,9 +415,11 @@ Fact a_not_square : forall x: Zmodp.type,
Fact two_not_square : forall x: Zmodp.type,
x^+2 != 2%:R.
\end{lstlisting}
We consider $M_{486662,1}(\F{p})$ and $M_{486662,2}(\F{p})$, one of its quadratic twist.
We now consider $M_{486662,1}(\F{p})$ and $M_{486662,2}(\F{p})$, one of its quadratic twists.
% \begin{dfn}Let the following instantiations of \aref{alg:montgomery-double-add}:\\
\begin{dfn}Let the following instantiations of \aref{alg:montgomery-ladder}:\\
\begin{dfn}
%Let the following instantiations of \aref{alg:montgomery-ladder}:\\
We instantiate \coqe{opt_montgomery} in two specific ways:\\
-- $Curve25519\_Fp(n,x)$ for $M_{486662,1}(\F{p})$.\\
-- $Twist25519\_Fp(n,x)$ for $M_{486662,2}(\F{p})$.
\end{dfn}
......@@ -455,9 +466,19 @@ Theorem x_is_on_curve_or_twist:
\subsubsection{Curve25519 over \F{p^2}}
The quadratic extension $\F{p^2}$ is defined as $\F{p}[\sqrt{2}]$ by~\cite{Ber06}.
We can represent it as the set $\F{p} \times \F{p}$ with $\delta = 2$, in other words,
The theory of finite fields already had been formalized in the Mathematical Components
library,
%ref?
but this formalization is rather abstract, and we need concrete representations of field
elements here.
For this reason we decided to formalize a definition of $\F{p^2}$ ourselves.
We can represent $\F{p^2}$ as the set $\F{p} \times \F{p}$,
%with $\delta = 2$,
%we haven't introduced this delta?
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.
as for $\F{p}$ we use a module in Coq.
\begin{lstlisting}[language=Coq]
Module Zmodp2.
Inductive type :=
......@@ -498,7 +519,7 @@ Similarly as in $\F{p}$, we define $0^{-1} = 0$ and prove \lref{lemma:Zmodp2_rin
%% TOO LONG
%% If need remove this paragraph
We can then specialize the basic operations in order to speed up the verification
We then specialize the basic operations in order to speed up the verification
of formulas by using rewrite rules:
\begin{equation*}
\begin{split}
......@@ -525,10 +546,14 @@ $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})$. Similarly, any point on the quadratic twist
$M_{486662,2}(\F{p})$ is also on the curve $M_{486662,1}(\F{p^2})$.
$M_{486662,2}(\F{p})$ also corresponds to a point on the curve $M_{486662,1}(\F{p^2})$.
As direct consequence, using \lref{lemma: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,1}(\F{p^2})$ such that $\chi_0(P) = (x,0) = x$.
%for that you don't need that lemma, because in \F{p^2} you have square roots
%what you mean is that those points always are either from the curve or from th e twist in \F{p}
%do you have that as a lemma too?
%if so that lemma is what should be here
\begin{lstlisting}[language=Coq]
Lemma x_is_on_curve_or_twist_implies_x_in_Fp2:
......@@ -593,4 +618,6 @@ We then prove the equivalence between of operations in $\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$.
This proves the correctness of TweetNaCl's X25519 and RFC~7748.
All put together, this finishes the proof of the mathematical correctness of X25519: the fact that the code in X25519, both in the RFC~7748 and
in TweetNaCl versions, correctly computes multiplication in the elliptic curve.
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