Commit 9bed7b4f authored by Benoit Viguier's avatar Benoit Viguier
Browse files

removing alg 2

parent bc40eda7
......@@ -26,7 +26,7 @@ Details of the formalization can be found in \sref{subsec:ECC-Montgomery}.
For $M_{a,b}$ over a finite field $\F{p}$, the parameter $b$ is known as the ``twisting factor''.
For $b'\in \F{p}\backslash\{0\}$ and $b' \neq b$, the curves $M_{a,b}$ and $M_{a,b'}$
are isomorphic via $(x,y) \mapsto (x, \sqrt{b'/b} \cdot y)$.
are isomorphic via $(x,y) \mapsto (x, \sqrt{b/b'} \cdot y)$.
\begin{dfn}
When $b'/b$ is not a square in \F{p}, $M_{a,b'}$ is a \emph{quadratic twist} of $M_{a,b}$, i.e.,
......
......@@ -141,19 +141,19 @@ The correctness of this specification is formally proven in Coq with
% For the sake of completeness we proved all intermediate functions.
\subheading{Memory aliasing.}
In the VST, a simple specification of \texttt{M(o,a,b)} will assume that the pointer arguments
point to non-overlapping space in memory, also named memory share.
% XXX-Peter: "memory share" is unclear; please fix in the next sentence.
When called with three memory shares (\texttt{o, a, b}),
point to non-overlapping space in memory.
When called with three memory fragments (\texttt{o, a, b}),
the three of them will be consumed. However assuming this naive specification
when \texttt{M(o,a,a)} is called (squaring), the first two memory shares (\texttt{o, a})
are consumed and VST will expect a third memory share (\texttt{a}) which does not \emph{exist} anymore.
when \texttt{M(o,a,a)} is called (squaring), the first two memory areas (\texttt{o, a})
are consumed and VST will expect a third memory section (\texttt{a}) which does not \emph{exist} anymore.
Examples of such cases are illustrated in \fref{tikz:MemSame}.
\begin{figure}[h]
\centering
\include{tikz/memory_same_sh}
\caption{Aliasing and Separation Logic}
\label{tikz:MemSame}
\begin{figure}[h]%
\centering%
\include{tikz/memory_same_sh}%
\caption{Aliasing and Separation Logic}%
\label{tikz:MemSame}%
\end{figure}
As a result, a function must either have multiple specifications or specify which
......@@ -171,6 +171,9 @@ In the proof of our specification, we do a case analysis over $k$ when needed.
This solution does not cover all cases (e.g. all arguments are aliased) but it
is enough for our needs.
%XXX-Peter: shouldn't verifying fixed-length for loops be rather standard?
%XXX Benoit: it is simple if the argument is increasing or if the "recursive call"
% is made before the computations.
......@@ -276,7 +279,7 @@ Lemma M_bound_Zlength :
\subsection{Inversions, reflections and packing}
\subsection{Reflections, inversions and packing}
\label{subsec:inversions-reflections}
We now turn our attention to the multiplicative inverse in $\Zfield$ and techniques
......
......@@ -264,53 +264,61 @@ differential additions and point doubling on projective coordinates.
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 can define a ladder similar to the one used in TweetNaCl (See \aref{alg:montgomery-double-add}).
\begin{algorithm}
\caption{Montgomery ladder for scalar multiplication on $M_{a,b}(\K)$ with optimizations}
\label{alg:montgomery-double-add}
\begin{algorithmic}
\REQUIRE{$x \in \K\backslash \{0\}$, scalars $n$ and $m$, $n < 2^m$}
\ENSURE{$a/c = \chi_0(n \cdot P)$ for any $P$ such that $\chi_0(P) = x$}
\STATE $(a,c) \leftarrow (1,0)$ ~~~~~~~~~~~~~~~{\color{gray}\textit{$\chi_0(\Oinf) = (1:0)$}}
\STATE $(b,d) \leftarrow (x,1)$ ~~~~~~~~~~~~~~~{\color{gray}\textit{$\chi_0(P) = (x:1)$}}
\FOR{$k$ := $m$ \textbf{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}
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.
% 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 can define a ladder similar to the one used in TweetNaCl (See \aref{alg:montgomery-double-add}).
%
% \begin{algorithm}
% \caption{Montgomery ladder for scalar multiplication on $M_{a,b}(\K)$ with optimizations}
% \label{alg:montgomery-double-add}
% \begin{algorithmic}
% \REQUIRE{$x \in \K\backslash \{0\}$, scalars $n$ and $m$, $n < 2^m$}
% \ENSURE{$a/c = \chi_0(n \cdot P)$ for any $P$ such that $\chi_0(P) = x$}
% \STATE $(a,c) \leftarrow (1,0)$ ~~~~~~~~~~~~~~~{\color{gray}\textit{$\chi_0(\Oinf) = (1:0)$}}
% \STATE $(b,d) \leftarrow (x,1)$ ~~~~~~~~~~~~~~~{\color{gray}\textit{$\chi_0(P) = (x:1)$}}
% \FOR{$k$ := $m$ \textbf{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}
% \aref{alg:montgomery-double-add} is correct, \ie it respects its output
% conditions given the input conditions.
% \end{lemma}
% We formalized \lref{lemma:montgomery-double-add} as follows:
\begin{lemma}
\label{lemma:montgomery-double-add}
\aref{alg:montgomery-double-add} is correct, \ie it respects its output
conditions given the input conditions.
\end{lemma}
We formalized \lref{lemma:montgomery-double-add} as follows:
\begin{lstlisting}[language=Coq]
Lemma opt_montgomery_x :
forall (n m : nat) (x : K),
......@@ -334,7 +342,8 @@ And thus 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)$,
if $\chi_0(P) = x$ then \aref{alg:montgomery-double-add} returns $\chi_0(n \cdot P)$
% if $\chi_0(P) = x$ then \aref{alg:montgomery-double-add} returns $\chi_0(n \cdot P)$
if $\chi_0(P) = x$ then \coqe{opt_montgomery} returns $\chi_0(n \cdot P)$
\end{theorem}
\begin{lstlisting}[language=Coq]
Theorem opt_montgomery_ok (n m: nat) (x : K) :
......@@ -393,7 +402,8 @@ 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.
\begin{dfn}Let the following instantiations of \aref{alg:montgomery-double-add}:\\
% \begin{dfn}Let the following instantiations of \aref{alg:montgomery-double-add}:\\
\begin{dfn}Let the following instantiations of \aref{alg:montgomery-ladder}:\\
-- $Curve25519\_Fp(n,x)$ for $M_{486662,1}(\F{p})$.\\
-- $Twist25519\_Fp(n,x)$ for $M_{486662,2}(\F{p})$.
\end{dfn}
......
......@@ -32,6 +32,8 @@
\renewcommand{\algorithmicrequire}{\textbf{Input:\ }}
\renewcommand{\algorithmicensure}{\textbf{Output:\ }}
\setlength{\abovecaptionskip}{-10pt}
\newcommand{\todo}[1]{
{\color{red} \bf TODO: #1}
}
......@@ -110,6 +112,7 @@
}
\def\VSTe{\lstinline[language=CoqVST, basicstyle=\ttfamily\normalsize]}
\def\VSTes{\lstinline[language=CoqVST, basicstyle=\scriptsize]}
\def\VSTess{\lstinline[language=CoqVST, basicstyle=\ttfamily\footnotesize]}
\lstnewenvironment{CoqVST}{
% \mdframed[backgroundcolor=doc@lstbackground]%
......
\begin{tikzpicture}
\draw (0,0) rectangle (3,0.3);
\draw[thick] (1,0) -- (1,0.3);
\draw[thick] (2,0) -- (2,0.3);
......@@ -10,9 +9,9 @@
\draw[thick, -> ] (1.95, -0.6) -- (1.95, -0.5) -- (2.5,-0.1);
\node [anchor=north west, text width=6cm, align=left] (Sepoab) at (-0.5,-1.8)
{\footnotesize{$\mathtt{sh [\!\!\{ v\_o \}\!\!]\ \textrm{<\!--(}lg16\textrm{)--}\ o}$;\\
$\mathtt{sh [\!\!\{ v\_a \}\!\!]\ \textrm{<\!--(}lg16\textrm{)--}\ a}$;\\
$\mathtt{sh [\!\!\{ v\_b \}\!\!]\ \textrm{<\!--(}lg16\textrm{)--}\ b}$}};
{\VSTess{sh [{ v_o $\!\!\}\!\!]\!\!\!$ <<(lg16)-- o}\\[-0.2em]
\VSTess{sh [{ v_a $\!\!\}\!\!]\!\!\!$ <<(lg16)-- a}\\[-0.2em]
\VSTess{sh [{ v_b $\!\!\}\!\!]\!\!\!$ <<(lg16)-- b}};
\begin{scope}[yshift=0 cm,xshift=4.5 cm]
......@@ -26,15 +25,14 @@
\draw[thick, -> ] (1.45, -0.6) -- (1.45, -0.5) -- (1.5,-0.1);
\node [anchor=north west, text width=6cm, align=left] (Sepoab) at (-0.5,-1.8)
{\footnotesize{$\mathtt{sh [\!\!\{ v\_c \}\!\!]\ \textrm{<\!--(}lg16\textrm{)--}\ c}$;\\
$\mathtt{sh [\!\!\{ v\_a \}\!\!]\ \textrm{<\!--(}lg16\textrm{)--}\ a}$}};
{\VSTess{sh [{ v_c $\!\!\}\!\!]\!\!\!$ <<(lg16)-- c}\\[-0.2em]
\VSTess{sh [{ v_a $\!\!\}\!\!]\!\!\!$ <<(lg16)-- a}};
\end{scope}
\draw[dashed] (-0.5,-1.2) -- +(7.5,0);
\draw[dashed] (-0.5,-1.2) -- +(8,0);
\node [anchor=north west] (sep) at (-0.5,-1.2) {In Separation Logic:};
\begin{scope}[yshift=-4.5 cm,xshift=2 cm]
\begin{scope}[yshift=-4.25 cm,xshift=2 cm]
\draw (0,0) rectangle (2,0.3);
\draw[thick] (1,0) -- (1,0.3);
\node [anchor=east] (shm) at (0,0.15) {sh\;};
......@@ -49,12 +47,11 @@
\draw[thick, -> ] (2.0, -0.6) -- (2.45, -0.2) -- (2.45, 0.3) -- (2.2, 0.65) -- (1.5,0.65);
\node [anchor=north west, text width=6cm, align=left] (Sepoab) at (-0.5,-1.8)
{\footnotesize{$\mathtt{sh [\!\!\{ v\_a \}\!\!]\ \textrm{<\!--(}lg16\textrm{)--}\ a}$;\\
$\mathtt{sh [\!\!\{ v\_c \}\!\!]\ \textrm{<\!--(}lg16\textrm{)--}\ c}$;\\
$\mathtt{Ews} \mathtt{[\!\!\{ \_\_121665 \}\!\!]\ \textrm{<\!--(}lg16\textrm{)--}\ \_121665}$}};
{\VSTess{sh [{ v_a $\!\!\}\!\!]\!\!\!$ <<(lg16)-- a}\\[-0.2em]
\VSTess{sh [{ v_c $\!\!\}\!\!]\!\!\!$ <<(lg16)-- c}\\[-0.2em]
\VSTess{Ews [{ __121665 $\!\!\}\!\!]\!\!\!$ <<(lg16)-- _121665}
};
\end{scope}
\draw[dashed] (0.5,-5.7) -- +(6,0);
\node [anchor=north west] (sep) at (0.5,-5.7) {In Separation Logic:};
\end{tikzpicture}
\draw[dashed] (0.5,-5.45) -- +(6,0);
\node [anchor=north west] (sep) at (0.5,-5.45) {In Separation Logic:};
\end{tikzpicture}%
......@@ -50,12 +50,12 @@
\draw (0.3,-0.05) node[textstyle] {Specification};
\draw (1.375,-1) node[textstyle, anchor=center, align=left] {
{\color{doc@lstnumbers}\textbf{Pre}}:\\
~~\texttt{s}$[\!\!\{$\texttt{n}$\}\!\!]= n \in \N$,\\
~~\texttt{s}$[\!\!\{$\texttt{n}$\}\!\!]\leftarrow n \in \N$,\\
% ~~$n \in$ \TNaCles{u8[32]},\\
~~\texttt{s}$[\!\!\{$\texttt{p}$\}\!\!]= P \in E(\F{p^2})$\\
~~\texttt{s}$[\!\!\{$\texttt{p}$\}\!\!]\leftarrow P \in E(\F{p^2})$\\
% ~~$P \in$ \TNaCles{u8[32]}\\
{\color{doc@lstdirective}\textbf{Post}}:\\
~~\texttt{s}$[\!\!\{$\texttt{q}$\}\!\!]=$~\texttt{RFC}$(n,P)$};
~~\texttt{s}$[\!\!\{$\texttt{q}$\}\!\!]\leftarrow$~\texttt{RFC}$(n,P)$};
\end{scope}
% VST Theorem
......
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