tweetverif.tex 1.65 KB
Newer Older
1
2
% \documentclass[letterpaper,twocolumn,9pt]{article}
\documentclass[conference]{IEEEtran}
3

Peter Schwabe's avatar
Peter Schwabe committed
4
\IEEEoverridecommandlockouts % this enables the \thanks command
5

6
7
8
9
\usepackage{epsfig}
\usepackage{setup}

\newif\ifpublic
Peter Schwabe's avatar
Peter Schwabe committed
10
\publicfalse
11
12
13
14
15
16
17
18
19
20
21
22

\newif\iffull
\fulltrue

\input{macros}

\begin{document}

%don't want date printed
\date{}

%make title bold and 14 pt font (Latex default is non-bold, 16 pt)
Benoit Viguier's avatar
Benoit Viguier committed
23
\title{\Large \bf A Coq proof of TweetNaCl's X25519 correctness}
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43

%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{XXX: Affiliation,\\
The Netherlands}
\and
\IEEEauthorblockN{Freek Wiedijk}
\IEEEauthorblockA{Radboud University,\\
The Netherlands}
}
Benoit Viguier's avatar
Benoit Viguier committed
44
45
46
\else
% just to remove complains from compilation
\author{}
47
48
49
50
\fi

\maketitle

Peter Schwabe's avatar
Peter Schwabe committed
51
52
53
54
55
56
57
%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.
%}
58

59
60
61
62
63
64
65
66
67
68
%\thispagestyle{empty}

\input{abstract.tex}
\input{intro.tex}
\input{preliminaries.tex}
\input{lowlevel.tex}
\input{highlevel.tex}
\input{conclusion.tex}

\vspace*{1cm}
Benoit Viguier's avatar
Benoit Viguier committed
69
{\footnotesize \bibliographystyle{IEEEtran}
70
71
72
\bibliography{collection}}

\begin{appendix}
73
  \input{code-tweetnacl.tex}
Benoit Viguier's avatar
Benoit Viguier committed
74
  \input{coq.tex}
75
  \input{proofs.tex}
76
  \input{files.tex}
77
78
79
\end{appendix}

\end{document}