Commit d6ba523e authored by benoit's avatar benoit
Browse files

move to ieee format

parent d16cfd19
......@@ -7,7 +7,7 @@ It uses specialized code for different platforms, which makes it rather complex
TweetNaCl~\cite{BGJ+15} is a compact re-implementation in C
of the core functionalities of NaCl and is claimed to be
\emph{``the first cryptographic library that allows correct functionality
to be verified by auditors with reasonable effort''}~\cite{BGJ+15}.
to be verified by auditors with reasonable effort''}~\cite{BGJ+15}.
The original paper presenting TweetNaCl describes some effort to support
this claim, for example, formal verification of memory safety, but does not actually
prove correctness of any of the primitives implemented by the library.
......@@ -115,7 +115,7 @@ structure of finite field and elliptic curves the actual proofs are quite differ
\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://anonfile.com/B9x43aZ6n4/coq-verif-tweetnacl.tar.gz}
It is available at \url{https://github.com/coq-verif-tweetnacl/coq-verif-tweetnacl/}
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}.
......@@ -135,7 +135,7 @@ effort required to extend our work to other elliptic-curve software.
\fref{tikz:ProofOverview} shows a graph of dependencies of the proofs.
C source files are represented by {\color{doc@lstfunctions}.C} while
{\color{doc@lstfunctions}.V} corresponds to Coq files.
{\color{doc@lstfunctions}.V} corresponds to Coq files.
\begin{figure}[h]
\centering
......
% \documentclass[letterpaper,twocolumn,9pt]{article}
\documentclass[conference]{IEEEtran}
\IEEEoverridecommandlockouts % this enables the \thanks command
\usepackage{epsfig}
\usepackage{setup}
\newif\ifpublic
\publicfalse
\newif\iffull
\fulltrue
\input{_macros}
\begin{document}
\input{_todo}
%don't want date printed
\date{}
%make title bold and 14 pt font (Latex default is non-bold, 16 pt)
\title{\Large \bf A Coq proof of the correctness of X25519 in TweetNaCl}
%for single author (just remove % characters)
\ifpublic
\author{
\IEEEauthorblockN{Peter Schwabe}
\IEEEauthorblockA{Radboud University,\\
The Netherlands}
\and
\IEEEauthorblockN{Beno\^it Viguier}
\IEEEauthorblockA{Radboud University,\\
The Netherlands}
\and
\IEEEauthorblockN{Timmy Weerwag}
\IEEEauthorblockA{Radboud University,\\
The Netherlands}
\and
\IEEEauthorblockN{Freek Wiedijk}
\IEEEauthorblockA{Radboud University,\\
The Netherlands}
}
\else
% just to remove complains from compilation
\author{}
\fi
\maketitle
%XXX: Figure out how to put this somewhere nice
%\thanks{
%XXX:
%This work would not have been possible without the assistance of multiple people.
%Andrew Appel and Lennart Beringer for having us in Princeton and teaching us the use of VST.
%John Wiegley for introducing us to proofs by reflection at the DeepSpec Summer School 2017.
%}
%\thispagestyle{empty}
\newif\ifusenix
\newif\ifacm
\newif\ifieee
\newif\ifpublic
\usenixtrue
\usenixfalse
\acmfalse
\ieeetrue
\publicfalse
\ifusenix
\input{_usenix}
\else
\input{_acmccs}
\input{_usenix}
\fi
\ifacm
\input{_acmccs}
\fi
\ifieee
\input{_ieee}
\fi
% \begin{acks}
......@@ -21,14 +29,20 @@
\ifusenix
\bibliographystyle{plain}
\bibliography{collection}
\else
\fi
\ifacm
\vspace*{1cm}
{\bibliographystyle{ACM-Reference-Format}
\bibliography{collection}}
\bibliography{collection}}
\fi
\ifieee
\vspace*{1cm}
{\footnotesize \bibliographystyle{IEEEtran}
\bibliography{collection}}
\fi
\begin{appendix}
\intput{appendix}
\intput{appendix}
\end{appendix}
\end{document}
......@@ -28,10 +28,10 @@
\renewcommand{\linenumberfont}{\normalfont\footnotesize\color{red}}
\else
\fi
% \definecolor{linkcolor}{rgb}{0.65,0,0}
% \definecolor{citecolor}{rgb}{0,0.45,0}
% \definecolor{urlcolor}{rgb}{0,0,0.65}
% \usepackage[colorlinks=true, backref=page, linkcolor=linkcolor, urlcolor=urlcolor, citecolor=citecolor]{hyperref}
\definecolor{linkcolor}{rgb}{0.65,0,0}
\definecolor{citecolor}{rgb}{0,0.45,0}
\definecolor{urlcolor}{rgb}{0,0,0.65}
\usepackage[colorlinks=true, backref=page, linkcolor=linkcolor, urlcolor=urlcolor, citecolor=citecolor]{hyperref}
\renewcommand{\algorithmicrequire}{\textbf{Input:\ }}
\renewcommand{\algorithmicensure}{\textbf{Output:\ }}
......
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