Commit 71c3179c authored by Benoit Viguier's avatar Benoit Viguier
Browse files

fixes

parent 2ac582eb
......@@ -80,7 +80,7 @@ matches the specification.
The X25519 implementation from the Evercrypt project~\cite{EverCrypt}
uses a low-level language called Vale that translates
directly to assembly and proves equivalence to a high-level specification in F$^*$.
In~\cite{Zinzindohoue2016AVE}, Zinzindohou{\'{e}}, Bartzia, and Bhargavan
In~\cite{Zinzindohoue2016AVE}, Zinzindohou{\'{e}}, Bartzia, and Bhargavan
describe a verified extensible library of elliptic curves~ in F*~\cite{DBLP:journals/corr/BhargavanDFHPRR17}.
This served as ground work for the cryptographic library HACL*~\cite{zinzindohoue2017hacl}
used in the NSS suite from Mozilla. The approach they use is a combination
......@@ -113,11 +113,9 @@ As those are all symmetric primitives without the rich mathematical
structure of finite field and elliptic curves the actual proofs are quite different.
\subheading{Reproducing the proofs.}
%To maximize reusability of our results
We place the code of our formal proof
%presented in this paper
into the public domain.
It is available at \url{https://cdn-15.anonfile.com/B9x43aZ6n4/6aa03e98-1581782249/coq-verif-tweetnacl.tar.gz}
To maximize reusability of our results we place the code of our formal proof
presented in this paper into the public domain.
It is available at \url{https://anonfile.com/B9x43aZ6n4/coq-verif-tweetnacl.tar.gz}
with instructions of how to compile and verify our proof.
A description of the content of the code archive is provided in
Appendix~\ref{appendix:proof-folders}.
......
......@@ -103,7 +103,9 @@ in GF(p), i.e., they are performed modulo p.''}~\cite{rfc7748}
Operations used in the Montgomery ladder of \coqe{RFC} are performed on
integers (See Appendix~\ref{subsubsec:RFC-Coq}).
The reduction modulo $\p$ is deferred to the very end as part of the
\coqe{ZPack25519} operation. We now turn our attention to the decoding and encoding of the byte arrays.
\coqe{ZPack25519} operation.
We now turn our attention to the decoding and encoding of the byte arrays.
We define the little-endian projection to integers as follows.
\begin{dfn}
Let \Coqe{ZofList} : $\Z \rightarrow \texttt{list}~\Z \rightarrow \Z$,
......@@ -116,7 +118,6 @@ Fixpoint ZofList {n:Z} (a:list Z) : Z :=
| h :: q => h + 2^n * ZofList q
end.
\end{lstlisting}
The encoding from integers to bytes is defined in a similar way:
\begin{dfn}
Let \Coqe{ListofZ32} : $\Z \rightarrow \Z \rightarrow \texttt{list}~\Z$, given
......
......@@ -27,7 +27,8 @@ 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}).
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}
\label{subsec:ECC}
......
......@@ -2,7 +2,7 @@
\newif\ifpublic
\usenixtrue
\publictrue
\publicfalse
\ifusenix
\input{_usenix}
......
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