Commit 0c99e7b1 authored by Benoit Viguier's avatar Benoit Viguier
Browse files

add graphics for the proofs in the maths parts

parent 91b9ca96
......@@ -26,15 +26,6 @@ used elsewhere in the paper. I.e., elsewhere in the paper, there is
usually a lot of code details."\\
+ I don't know what to do on that one.
- "the discussion of the computation of n’ was completely unclear to me."\\
+ describe the process of clamping better.
- "Maybe use a backward reference to p.3 where
CSWAP was defined, since in between, there was a lot of content,
and relying on the reader’s memory does not really work here (or
at least, it did not work for me)"\\
+ @PETER ?
- "I was wondering whether you consider the approach in [13] as synthesis or
verification, because to me, it seemed a mix/neither."\\
+ [13] is "Verified Low-Level Programming Embedded in F*",\\
......
......@@ -27,10 +27,21 @@ We first review the work of Bartzia and Strub \cite{BartziaS14} (\ref{subsec:ECC
We extend it to support Montgomery curves (\ref{subsec:ECC-Montgomery})
with homogeneous coordinates (\ref{subsec:ECC-projective}) and prove the
correctness of the ladder (\ref{subsec:ECC-ladder}).
We discuss the plot twist (\ref{subsec:Zmodp}) of Curve25519 and solve it (\ref{subsec:curvep2}).
\subsection{Formalization of elliptic Curves}
\label{subsec:ECC}
\todo{Beter here of after the final theorem of the subsection?}
\begin{figure}[h]
\centering
\include{tikz/highlevel1}
\caption{Overview of the proof of Montgomery ladder's correctness}
\label{tikz:ProofHighLevel1}
\end{figure}
We consider elliptic curves over a field $\K$. We assume that the
characteristic of $\K$ is neither 2 or 3.
......@@ -311,6 +322,16 @@ Theorem opt_montgomery_ok (n m: nat) (x : K) :
\subsection{Curves, twists and extension fields}
\todo{Beter here of after the final theorem of the subsection?}
\begin{figure}[h]
\centering
\include{tikz/highlevel2}
\caption{Instanciations and proof dependencies for the correctness of X25519}
\label{tikz:ProofHighLevel2}
\end{figure}
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.$$
......@@ -368,7 +389,6 @@ We instantiate \coqe{opt_montgomery} in two specific ways:\\
-- $Twist25519\_Fp(n,x)$ for $M_{486662,2}(\F{p})$.
\end{dfn}
\todoln{use \$...\$ or \$\$...\$\$ ?}
With \tref{thm: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}$,\\
......@@ -411,6 +431,7 @@ Theorem x_is_on_curve_or_twist:
\end{lstlisting}
\subsubsection{Curve25519 over \F{p^2}}
\label{subsec:curvep2}
The quadratic extension $\F{p^2}$ is defined as $\F{p}[\sqrt{2}]$ by~\cite{Ber06}.
The theory of finite fields already has been formalized in the Mathematical Components
......
......@@ -54,11 +54,6 @@ o[i] = aux1 + aux2;
\todo{NEW}
\subheading{Limitations of our proof}
Our proof focuses on the correctness, we do not verify the constant-timeness of
the TweetNaCl code nor do we prove
\subheading{Corrections in TweetNaCl.}
As a result of this verification, we removed superfluous code.
Indeed indexes 17 to 79 of the \TNaCle{i64 x[80]} intermediate variable of
......@@ -78,11 +73,14 @@ and thus solved this problem.
o[i]&=0xffff;
\end{lstlisting}
We believe that type changes of loop indexes (\TNaCle{int} instead of \TNaCle{i64})
do not impact the trust of our proof.
\todo{NEW}
\todoln{NEW}
We contacted the authors of TweetNaCl and believe that the changes above
Aside from the modications above mentionned, all subsequent alteration
---such as the type change of loop indexes (\TNaCle{int} instead of \TNaCle{i64})---
were required for VST to parse properly the code. We believe those
adjustments do not impact the trust of our proof.
We contacted the authors of TweetNaCl and expect that the changes above
mentionned will soon be integrated in a new version of the library.
\subheading{Extending our work.}
......@@ -92,9 +90,14 @@ assuming the same forumlas are used.
In addition to the curve equation, the field \F{p} would need to be redefined
as $p=2^{255}-19$ is hard-coded in order to speed up some proofs.
With respect to the C code verification (\sref{sec:C-Coq}),
\eg X448~\cite{cryptoeprint:2015:625,rfc7748} would require the adaptation most of the
low level arithmetic (mainly the multiplication, carry propagations and reductions).
With respect to the C code verification (\sref{sec:C-Coq}), the extension of
the verification effort to Ed25519 would makes directly use of the low level
arithmetic. The ladder steps formula being different this would require a high
level verification similar to \tref{thm:montgomery-ladder-correct}.
The verification \eg X448~\cite{cryptoeprint:2015:625,rfc7748} in C would
require the adaptation of most of the low level arithmetic (mainly the
multiplication, carry propagations and reductions).
Once the correctness and bounds of the basic operations are established,
reproving the full ladder would make use of our generic definition and lower
the workload.
......
......@@ -3,6 +3,9 @@
This paper has been submitted to IEEE Symposium on Security and Privacy 2020.
We thank and really appreciate the reviewers who took time to provide us with
such detailed feedback.
\subsection{S\&P 2020 Review \#582A}
Overall merit: 3. Weak reject - The paper has flaws, but I will not argue against it.
......@@ -81,10 +84,17 @@ On page 9: "each functions" => no s
\subheading{Our answer}
\todoln{New stuff}
We corrected the typos. There are no new proof techniques in the case of this
verification. We used reflections techniques to generically solve some of our
goals such as the proof of inversion.
We corrected the typos.
The novelty of this work is not in the proof techniques.
It lies in the assurance gained by the formalization of the X25519 from RFC~7748,
and its correctness with respect to the theory of elliptic curves.
It is the first time, we have a link from the C code up to the mathematical
definitions of Curve25519.
We removed the description of how verification of for loops are handled and the
details of the proof by reflections.
We described in the Conclusion (\sref{sec:Conclusion}) how our results can be
extended or reused in future works.
\subsection{S\&P 2020 Review \#582B}
......@@ -184,10 +194,15 @@ whether this is careful quantification or not.
\subheading{Our answer}
\todoln{New stuff}
Clarification in intro: VST has already been used to verify symmetric Cryptographic
primities, as mentioned later by \cite{Beringer2015VerifiedCA} and \cite{2015-Appel}.
We have not found errors in the implementation but we removed an
undefined behavior by the C standard.
\todo{Can I say that?}
Compilers were smart enough to prevent problems in that instance.
\subsection{S\&P 2020 Review \#582C}
......@@ -277,5 +292,3 @@ Do you already prove such a property? More generally, what about the proof of
Section V is specific to X25519 and what is generic?
\subheading{Our answer}
\todoln{New stuff}
\begin{tikzpicture}[textstyle/.style={black, anchor= south west, align=center, minimum height=0.45cm, text centered, font=\scriptsize}]
% Bartzia & Strub
\draw[dashed, fill=doc@lstbackground] (2.75,0.5) -- (2.75,2) -- (6,2) -- (6, 0.5) -- cycle;
\draw (6,2) node[textstyle, anchor=north east] {Library from Bartzia \& Strub};
% Mab
\begin{scope}[yshift=0 cm,xshift=0 cm]
\draw (0,0) -- (1.5,0) -- (1.5,-0.75) -- (0, -0.75) -- cycle;
\draw (0.75,-0.375) node[textstyle, anchor=center] {$M_{a,b}(\K)$};
\end{scope}
% Eab
\begin{scope}[yshift=1.5 cm,xshift=3 cm]
\draw[fill=white] (0,0) -- (1.5,0) -- (1.5,-0.75) -- (0, -0.75) -- cycle;
\draw (0.75,-0.375) node[textstyle, anchor=center] {$E_{a',b'}(\K)$};
\end{scope}
% 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};
\end{scope}
% Hypothesis x square is not 2
\begin{scope}[yshift=-1.5 cm,xshift=0 cm]
\draw [fill=orange!20] (0,0) -- (1.5,0) -- (1.5,-1.25) -- (0, -1.25) -- cycle;
\draw (0,0) node[textstyle, anchor=north west] {\textbf{Hyp:}};
\draw (0.75,-0.375) node[textstyle, anchor=north] {$\forall x \in \K,$\\$x^2 \neq 2$};
\end{scope}
% Final theorem
\begin{scope}[yshift=-1.5 cm,xshift=3 cm]
\draw [fill=green!20] (0,0) -- (3.25,0) -- (3.25,-1.375) -- (0, -1.375) -- cycle;
\draw (0,0) node[textstyle, anchor=north west] {\textbf{Thm:}};
\draw (1.675,-0.375) node[textstyle, anchor=north] {$\forall x \in \K, n \in \N, P \in M_{a,b}(\K),$\\$x = \chi(P) \implies$\\ladder $n$ $x$ = $\chi(n \cdot P)$};
\end{scope}
\path [thick, double, ->] (1.5,-0.375) edge [out=0, in=-180] (3,-0.375);
\path [thick, double, ->] (3.75,0.75) edge [out=-90, in=90] (3.75,0);
\path [thick, double, ->] (3.75,-0.75) edge [out=-90, in=90] (3.75,-1.5);
\path [thick, double, ->] (1.5,-2.125) edge [out=0, in=-180] (3,-2.125);
\end{tikzpicture}
\begin{tikzpicture}[textstyle/.style={black, anchor= south west, align=center, minimum height=0.45cm, text centered, font=\scriptsize}]
\draw (6.75,1.5) node[textstyle, anchor=north east] {$p = \p$\\$C = M_{486662,1}$\\$T = M_{486662,2}$\\};
\begin{scope}[yshift=1.5 cm,xshift=-0.5 cm]
\draw [fill=green!20] (0,0) -- (1.5,0) -- (1.5,-0.75) -- (0, -0.75) -- cycle;
\draw (0.75,-0.375) node[textstyle, anchor=center] {$p$ is prime};
\end{scope}
\begin{scope}[yshift=0 cm,xshift=-0.5 cm]
\draw[fill=white] (0,0) -- (1.5,0) -- (1.5,-0.75) -- (0, -0.75) -- cycle;
\draw (0.75,-0.375) node[textstyle, anchor=center] {$\F{p}$};
\end{scope}
\begin{scope}[yshift=-1 cm,xshift=1.5 cm]
\draw[fill=green!20] (0,0) -- (1.5,0) -- (1.5,-0.75) -- (0, -0.75) -- cycle;
\draw (0.75,-0.375) node[textstyle, anchor=center] {$\forall x \in \F{p},$\\$x^2 \neq 2$};
\end{scope}
\begin{scope}[yshift=-1 cm,xshift=4 cm]
\draw[fill=white] (0,0) -- (1.5,0) -- (1.5,-0.75) -- (0, -0.75) -- cycle;
\draw (0.75,-0.375) node[textstyle, anchor=center] {$C(\F{p})$};
\end{scope}
\begin{scope}[yshift=-1 cm,xshift=6 cm]
\draw[fill=white] (0,0) -- (1.5,0) -- (1.5,-0.75) -- (0, -0.75) -- cycle;
\draw (0.75,-0.375) node[textstyle, anchor=center] {$T(\F{p})$};
\end{scope}
\path [thick, double, ->] (0.25,0.75) edge [out=-90, in=90] (0.25,0);
\path [thick, double] (1,-0.375) edge [out=0, in=180] (6.75,-0.375);
\path [thick, double, ->] (2.25,-0.375) edge [out=-90, in=90] (2.25,-1);
\path [thick, double, ->] (4.75,-0.375) edge [out=-90, in=90] (4.75,-1);
\path [thick, double, ->] (6.75,-0.375) edge [out=-90, in=90] (6.75,-1);
\begin{scope}[yshift=-2.5 cm,xshift=1.5 cm]
\draw[fill=green!20] (-0.35,0) -- (1.85,0) -- (1.85,-1.25) -- (-0.35, -1.25) -- cycle;
\draw (0.75,0) node[textstyle, anchor=north] {$\forall x \in \F{p},$\\$\exists P \in C(\F{p}),$\\$\exists Q \in T(\F{p})$,\\$x = \chi(P)\vee x = \chi(Q)$};
\end{scope}
\begin{scope}[yshift=-2.5 cm,xshift=4 cm]
\draw[fill=green!20] (-0.20,0) -- (1.70,0) -- (1.70,-1.25) -- (-0.20, -1.25) -- cycle;
\draw (0.75,0) node[textstyle, anchor=north] {$\forall x \in \F{p},$\\$\forall P \in C(\F{p}),$\\$x = \chi(P)\implies$\\lad. $n$ $x = \chi(n \cdot P)$};
\end{scope}
\begin{scope}[yshift=-2.5 cm,xshift=6 cm]
\draw[fill=green!20] (-0.20,0) -- (1.70,0) -- (1.70,-1.25) -- (-0.20, -1.25) -- cycle;
\draw (0.75,0) node[textstyle, anchor=north] {$\forall x \in \F{p},$\\$\forall Q \in T(\F{p}),$\\$x = \chi(Q)\implies$\\lad. $n$ $x = \chi(n \cdot Q)$};
\end{scope}
\path [thick, double] (2.25,-2.125) edge [out=0, in=180] (6.75,-2.125);
\path [thick, double, ->] (2.25,-1.75) edge [out=-90, in=90] (2.25,-2.5);
\path [thick, double, ->] (4.75,-1.75) edge [out=-90, in=90] (4.75,-2.5);
\path [thick, double, ->] (6.75,-1.75) edge [out=-90, in=90] (6.75,-2.5);
% F(p^2)
\path [thick, double, ->] (0.25,-0.75) edge [out=-90, in=90] (0.25,-2.5);
\begin{scope}[yshift=-2.5 cm,xshift=-0.5 cm]
\draw[fill=white] (0,0) -- (1.5,0) -- (1.5,-0.75) -- (0, -0.75) -- cycle;
\draw (0.75,-0.375) node[textstyle, anchor=center] {$\F{p^2}$};
\end{scope}
\path [thick, double, ->] (0.25,-3.25) edge [out=-90, in=90] (0.25,-5);
% C(F(p^2))
\begin{scope}[yshift=-5 cm,xshift=-0.5 cm]
\draw[fill=white] (0,0) -- (1.5,0) -- (1.5,-0.75) -- (0, -0.75) -- cycle;
\draw (0.75,-0.375) node[textstyle, anchor=center] {$C(\F{p^2})$};
\end{scope}
\begin{scope}[yshift=-5 cm,xshift=1.5 cm]
\draw[fill=green!20] (0,0) -- (2,0) -- (2,-0.75) -- (0, -0.75) -- cycle;
\draw (1,-0.375) node[textstyle, anchor=center] {$C(\F{p}) \subset C(\F{p^2})$};
\end{scope}
\begin{scope}[yshift=-6 cm,xshift=1.5 cm]
\draw[fill=green!20] (0,0) -- (2,0) -- (2,-0.75) -- (0, -0.75) -- cycle;
\draw (1,-0.375) node[textstyle, anchor=center] {$T(\F{p}) \subset C(\F{p^2})$};
\end{scope}
\path [thick, double, ->] (1,-5.375) edge [out=0, in=-180] (1.5,-5.375);
\path [thick, double] (1.25,-5.375) edge [out=-90, in=90] (1.25,-6.375);
\path [thick, double, ->] (1.25,-6.375) edge [out=0, in=-180] (1.5,-6.375);
\begin{scope}[yshift=-5 cm,xshift=4.5 cm]
\draw [fill=green!20] (0,0) -- (3.25,0) -- (3.25,-1.75) -- (0, -1.75) -- cycle;
\draw (0,0) node[textstyle, anchor=north west] {\textbf{Thm:}};
\draw (1.675,-0.375) node[textstyle, anchor=north] {$\forall x \in \F{p},$\\$\forall P \in C(\F{p^2}),$\\$x = \chi(P)\implies$\\ladder $n$ $x = \chi(n \cdot P)$};
\end{scope}
\path [thick, double] (2.25,-4.375) edge [out=0, in=180] (6.75,-4.375);
\path [thick, double] (2.25,-3.75) edge [out=-90, in=90] (2.25,-4.375);
\path [thick, double] (4.75,-3.75) edge [out=-90, in=90] (4.75,-4.375);
\path [thick, double] (6.75,-3.75) edge [out=-90, in=90] (6.75,-4.375);
\path [thick, double] (3.5,-5.375) edge [out=0, in=180] (3.75,-5.375);
\path [thick, double] (3.5,-6.375) edge [out=0, in=180] (3.75,-6.375);
\path [thick, double] (3.75,-6.375) edge [out=90, in=-90] (3.75,-4.375);
\path [thick, double, ->] (6.125,-4.375) edge [out=-90, in=90] (6.125,-5);
\end{tikzpicture}
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