Commit b1a35f42 authored by Benoit Viguier's avatar Benoit Viguier
Browse files

start writting with pdf

parent 1ea0554e
......@@ -44,6 +44,7 @@ Doc
*.bbl
*.bcf
*.blg
*.brf
*.dvi
*.fdb_latexmk
*.fls
......
FILES=$(wildcard *.md )
TEX=$(FILES:%.md=%.tex)
PDF=$(FILES:%.md=%.pdf)
curve25519.pdf: curve25519.tex collection.bib
latexmk -pdf curve25519.tex
all: $(TEX) $(PDF)
%.tex: %.md
pandoc --from=markdown --output=$*.tex $*.md --to=latex --standalone
%.pdf: %.tex
xelatex $*.tex
.PHONY: clean
clean:
@echo cleaning...
@rm *.pdf 2> /dev/null || true
@rm *.tex 2> /dev/null || true
@rm *.toc 2> /dev/null || true
@rm *.log 2> /dev/null || true
@rm *.aux 2> /dev/null || true
@rm *.bbl 2> /dev/null || true
@rm *.blg 2> /dev/null || true
@rm *.brf 2> /dev/null || true
@rm *.dvi 2> /dev/null || true
@rm *.fdb_latexmk 2> /dev/null || true
@rm *.fls 2> /dev/null || true
@rm *.log 2> /dev/null || true
@rm *.out 2> /dev/null || true
This diff is collapsed.
% TEMPLATE for Usenix papers, specifically to meet requirements of
% USENIX '05
% originally a template for producing IEEE-format articles using LaTeX.
% written by Matthew Ward, CS Department, Worcester Polytechnic Institute.
% adapted by David Beazley for his excellent SWIG paper in Proceedings,
% Tcl 96
% turned into a smartass generic template by De Clarke, with thanks to
% both the above pioneers
% use at your own risk. Complaints to /dev/null.
% make it two column with no page numbering, default is 10 point
% Munged by Fred Douglis <douglis@research.att.com> 10/97 to separate
% the .sty file from the LaTeX source template, so that people can
% more easily include the .sty file into an existing document. Also
% changed to more closely follow the style guidelines as represented
% by the Word sample file.
% Note that since 2010, USENIX does not require endnotes. If you want
% foot of page notes, don't include the endnotes package in the
% usepackage command, below.
% This version uses the latex2e styles, not the very ancient 2.09 stuff.
\documentclass[letterpaper,twocolumn,10pt]{article}
\usepackage{usenix,epsfig}
%\usepackage{etex}
\usepackage[utf8]{inputenc}
\usepackage[T1]{fontenc}
\usepackage[pdf]{pstricks}
\usepackage{multido}
\newif\ifpublic
\publictrue
\newif\iffull
\fulltrue
\usepackage{amsfonts,amsmath,amscd,amssymb,array}
\usepackage{type1cm}
\newcommand{\lstsize}{\fontsize{8.5pt}{8.5pt}\selectfont}
\usepackage{algorithm}
\usepackage{algorithmic}
\usepackage{xcolor}
\definecolor{linkcolor}{rgb}{0.65,0,0}
\definecolor{citecolor}{rgb}{0,0.65,0}
\definecolor{urlcolor}{rgb}{0,0,0.65}
\usepackage[colorlinks=true, backref=page, linkcolor=linkcolor, urlcolor=urlcolor, citecolor=citecolor]{hyperref}
%\usepackage{breakurl}
\usepackage{ctable}
\usepackage{cite}
\usepackage{dsfont}
\usepackage{xspace}
\usepackage{subfig}
\usepackage{float}
\floatstyle{ruled}
\newfloat{Listing}{htb}{lst}
\floatstyle{plain}
\newfloat{Protocol}{htb}{proto}
\newcounter{subListing}
\newcounter{subListing@save}
\renewcommand{\thesubListing}{\alph{subListing}}
\renewcommand{\tabcolsep}{4pt}
\def\subheading#1{\medskip\noindent{\boldmath\textbf{#1}}~\ignorespaces}
\newcommand{\todo}[1]{\marginpar{\baselineskip0ex\rule{2,5cm}{0.5pt}\\[0ex]{\tiny\textsf{#1}}}}
\input{macros}
\begin{document}
%don't want date printed
\date{}
%make title bold and 14 pt font (Latex default is non-bold, 16 pt)
\title{\Large \bf Proving the complete correctness of TweetNaCl's Curve25519 implementation.%
\thanks{
Date: somewhen in 2018.}
}
%for single author (just remove % characters)
\ifpublic
\author{
{\rm Peter Schwabe}\\
Digital Security Group, Radboud University, The Netherlands\\
%\~\\
\and
{\rm Beno\^it Viguier}\\
Digital Security Group, Radboud University, The Netherlands\\
}
\fi
\maketitle
%\thispagestyle{empty}
\subsection*{Abstract}
By using the Coq formal proof assistant with the VST library, we prove the
soundness and correctness of TweetNaCl's Curve25519 implementation.
%\input{intro}
\vspace*{1cm}
{\footnotesize \bibliographystyle{acm}
\bibliography{collection}}
\begin{appendix}
\end{appendix}
\end{document}
\newtheorem{theorem}{Theorem}[section]
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{corollary}[theorem]{Corollary}
\newcommand\invisiblesection[1]{%
\refstepcounter{section}
\sectionmark{#1}}
\newenvironment{proof}[1][Proof]{\begin{trivlist}
\item[\hskip \labelsep {\bfseries #1}]}{\end{trivlist}}
\newenvironment{definition}[1][Definition]{\begin{trivlist}
\item[\hskip \labelsep {\bfseries #1}]}{\end{trivlist}}
\newenvironment{example}[1][Example]{\begin{trivlist}
\item[\hskip \labelsep {\bfseries #1}]}{\end{trivlist}}
\newenvironment{remark}[1][Remark]{\begin{trivlist}
\item[\hskip \labelsep {\bfseries #1}]}{\end{trivlist}}
\newcommand{\qed}{\nobreak \ifvmode \relax \else
\ifdim\lastskip<1.5em \hskip-\lastskip
\hskip1.5em plus0em minus0.5em \fi \nobreak
\vrule height0.75em width0.5em depth0.25em\fi}
\DeclareMathOperator*{\argmin}{arg\,min}
\DeclareMathOperator*{\Vol}{Vol}
\DeclareMathOperator*{\Supp}{Supp}
\newcommand{\cR}{\ensuremath{\mathcal R}}
\newcommand{\cS}{\ensuremath{\mathcal S}}
\newcommand{\CVPDf}{\ensuremath{\algo{CVP}_{\tilde{D}_4}}}
\newcommand{\CVPDfZf}{\ensuremath{\algo{CVP}_{D_4/\ZZ^4}}}
\newcommand{\LDEncode}{\algo{Encode}}
\newcommand{\LDDecode}{\algo{Decode}}
\usepackage{soul}\let\strikethrough\st\let\st\undefined
\newcommand{\PeiktertROUND}[1]{\langle #1 \rangle_2}
\newcommand{\PeiktertRec}{\textsf{rec}\xspace}
\newcommand{\PeiktertDbl}{\textsf{dbl}\xspace}
\newcommand{\PeiktertALICE}{Alice}
\newcommand{\PeiktertBOB}{Bob}
\newcommand{\NewHope}{\textsc{NewHope}\xspace}
\newcommand{\JarJar}{\textsc{JarJar}\xspace}
\newcommand{\NewhopeALICE}{Alice}
\newcommand{\NewhopeBOB}{Bob}
\newcommand{\NewhopeSERVER}{server}
\newcommand{\NewhopeCLIENT}{client}
\newcommand{\NewhopeRAND}{\{0,1\}^{256}}
\newcommand{\NewhopeGENA}{\textsf{prg}\xspace}
\newcommand{\NewhopeSEED}{seed\xspace}
\newcommand{\NewhopeHASHXOF}{\textsf{SHAKE-128}\xspace}
\newcommand{\NewhopePARSE}{\textsf{Parse}\xspace}
\newcommand{\NewhopeHASH}{\textsf{SHA3-256}\xspace}
\newcommand{\NewhopeREC}{{\textsf{Rec}}\xspace}
\newcommand{\NewhopeHelpREC}{{\textsf{HelpRec}}\xspace}
\newcommand{\NewhopeSENDA}{{\textsf{encodeA}}\xspace}
\newcommand{\NewhopeSENDB}{{\textsf{encodeB}}\xspace}
\newcommand{\NewhopeRECVA}{{\textsf{decodeA}}\xspace}
\newcommand{\NewhopeRECVB}{{\textsf{decodeB}}\xspace}
\newcommand{\NewhopeLDDECODE}{\textsf{Decode}\xspace}
\newcommand{\NewhopeValuek}{16}
\newcommand{\NewhopeValuekhalf}{8}
\newcommand{\NewhopeErrorDist}{\psi^n_{\NewhopeValuek}}
\newcommand{\NewhopeErrorDistOne}{\psi_{\NewhopeValuek}}
\newcommand{\NewhopeK}{\nu}
\newcommand{\NewhopeKey}{\mu}
\newcommand{\NTT}{\mbox{\textsf{NTT}}\xspace}
\newcommand{\INVNTT}{\ensuremath{\mbox{\textsf{NTT}}^{-1}}\xspace}
\newcommand{\pw}{\circ}
\newcommand{\NewhopeRing}{\ensuremath{\mathcal{R}_q}}
\newcommand{\T}{L}
%\newcommand{\F}{\mathbb{Z}}
\newcommand{\Z}{\mathbb{Z}}
\newcommand{\ZZ}{\mathbb{Z}}
\newcommand{\corr}{\,\hat{=}\,}
\newcommand{\RR}{\ensuremath{\mathbb{R}}}
\newcommand{\N}{\ensuremath{\mathbb{N}}}
\newcommand{\mbf}{\ensuremath{\mathbf}}
\newcommand{\rando}{\ensuremath{\xleftarrow{\$}}}
\newcommand{\la}{\ensuremath{\leftarrow}}
\newcommand{\MD}{\ensuremath{\mathcal{D}}\xspace}
\newcommand{\MS}{\ensuremath{\mathcal{D}}\xspace}
\newcommand{\MA}{\ensuremath{\mathcal{A}}\xspace}
\newcommand{\MB}{\ensuremath{\mathcal{B}}\xspace}
\newcommand{\MP}{\ensuremath{\mathcal{P}}\xspace}
\newcommand{\tA}{\ensuremath{t_{\mathcal{A}}}}
\newcommand{\eA}{\ensuremath{\varepsilon_{\mathcal{A}}}}
\newcommand{\tS}{\ensuremath{t_{\mathcal{D}}}}
\newcommand{\eS}{\ensuremath{\varepsilon_{\mathcal{D}}}}
\newcommand{\vX}{\mathcal X}
\newcommand{\vY}{\mathcal Y}
\newcommand{\MR}{\ensuremath{\mathcal{R}}\xspace}
\newcommand{\tR}{\ensuremath{t_{\mathcal{R}}}}
\newcommand{\eR}{\ensuremath{\varepsilon_{\mathcal{R}}}}
\newcommand{\tD}{\ensuremath{t_{\mathcal{D}}}}
\newcommand{\eD}{\ensuremath{\varepsilon_{\mathcal{D}}}}
\newcommand{\sis}{\textsf{SIS}\xspace}
\newcommand{\isis}{\textsf{ISIS}\xspace}
\newcommand{\lwe}{\textsf{LWE}\xspace}
\newcommand{\dlwe}{\textsf{LWE}\xspace}
\newcommand{\rdlwe}{\textsf{R-LWE}\xspace}
\newcommand{\ee}{\ensuremath{\varepsilon}}
\newcommand{\sS}{\ensuremath{\sigma}}
\newcommand{\sE}{\ensuremath{\sigma}}
\newcommand{\DS}{\ensuremath{D_{\sS}}}
\newcommand{\DE}{\ensuremath{D_{\sE}}}
%\newcommand{\Dy}{\ensuremath{D_y}}
\newcommand{\Dy}{\ensuremath{[-B, B]}}
\newcommand{\Dysc}{\ensuremath{D_{y,\mat{Sc}}}}
\newcommand{\Dz}{\ensuremath{D_z}}
\newcommand{\bit}{\ensuremath{\{0,1\}}}
\newcommand{\eqdef}{\stackrel{\mathrm{def}}=}
\newcommand{\rand}{\getsr}
\newcommand{\rounddq}[1]{\ensuremath{\lfloor #1 \rceil_{d,q}}}
\newcommand{\roundd}[1]{\ensuremath{\lfloor #1 \rceil_d}}
\newcommand{\norm}[1]{\ensuremath{||#1||}}
%\newcommand{\KeyGen}{\ensuremath{\mathsf{KeyGen_{BG}}}}
%\newcommand{\Sign}{\ensuremath{\mathsf{Sign_{BG}}}}
%\newcommand{\Verify}{\ensuremath{\mathsf{Verify_{BG}}}}
\newcommand{\KeyGen}{\keygen}
\newcommand{\Sign}{\sign}
\newcommand{\Verify}{\verify}
\newcommand{\keygen}{\ensuremath{\mathsf{KeyGen}}}
\newcommand{\sign}{\ensuremath{\mathsf{Sign}}}
\newcommand{\verify}{\ensuremath{\mathsf{Verify}}}
\newcommand{\start}{\underline{\ensuremath{\mathsf{Start}}}\xspace}
\newcommand{\randO}{\ensuremath{\underline{\mathsf{Rand}}^{O_c}}\xspace}
\newcommand{\signO}{\ensuremath{\underline{\mathsf{Sign}}^{O_c}}\xspace}
\newcommand{\finishO}{\ensuremath{\underline{\mathsf{Finish}}^{O_c}}}
\newcommand{\instance}{\underline{\ensuremath{\mathsf{Instance}}}}
\newcommand{\Sample}{\ensuremath{\mathsf{Sample}}}
\newcommand{\keygenQ}{\ensuremath{\mathsf{KeyGen}}}
\newcommand{\signQ}{\ensuremath{\mathsf{Sign}}}
\newcommand{\verifyQ}{\ensuremath{\mathsf{Verify}}}
\newcommand{\CHgen}{\ensuremath{\mathsf{ChGen}}}
\newcommand{\inputtext}{\textsf{INPUT:}\;}
\newcommand{\outputtext}{\textsf{OUTPUT:}\;}
\newcommand{\iftext}{\mathbf{if\;}}
\newcommand{\elsetext}{\mathbf{else\;}}
\newcommand{\then}{\mathbf{then\;}}
\newcommand{\return}{\mathbf{return\;}}
\newcommand{\mat}[1]{\mathbf{#1}}
\renewcommand{\vec}[1]{\mathbf{#1}}
\newcommand{\modq}{\ensuremath{\; (\bmod \; q)}}
%\newcommand{\modq}{\ensuremath{\; (q)}}
\newcommand{\ip}[2]{\ensuremath{\langle {#1},{#2}\rangle}}
\newcommand{\adv}{\ensuremath{\mathcal{A}}}
\newcommand{\secpar}{\ensuremath{\lambda}}
\newcommand{\sk}{\ensuremath{\mathsf{sk}}\xspace}
\newcommand{\pk}{\ensuremath{\mathsf{vk}}\xspace}
\newcommand{\sst}{\ensuremath{\mathsf{st}}\xspace}
\newcommand{\CH}{\ensuremath{\mathcal{CH}}}
\newcommand{\ch}{\ensuremath{\mathsf{CH}}}
\newcommand{\Mek}{\ensuremath{\mathsf{M_{ek}}}}
\newcommand{\Yek}{\ensuremath{\mathsf{Y_{ek}}}}
\newcommand{\Rek}{\ensuremath{\mathsf{R_{ek}}}}
\newcommand{\ek}{\ensuremath{\mathsf{ek}}}
\newcommand{\td}{\ensuremath{\mathsf{td}}}
\newcommand{\Gen}{\ensuremath{\mathsf{Gen}}}
\newcommand{\negl}{\ensuremath{\mathsf{negl}}}
\newcommand{\R}{\mathcal{R}}
\newcommand{\Rp}{\mathcal{R}_p}
\newcommand{\Rq}{\mathcal{R}_q}
\newcommand{\Rqk}[1]{\mathcal{R}_{q,#1}}
\def\getsr{\stackrel{{\scriptscriptstyle \$}}{\leftarrow}}
\def\gets{{\leftarrow}}
\newcommand{\Uniform}{\mathcal{U}}
\newcommand{\UniRk}[1]{\Rqk{#1}}
\newcommand{\UniRq}{\Rq}
\newcommand{\zeropo}{{\bf 0}}
\newcommand{\Apo}{{\bf A\xspace}}
\newcommand{\Bpo}{{\bf B\xspace}}
\newcommand{\Ipo}{{\bf I\xspace}}
\newcommand{\apo}{{\bf a\xspace}}
\newcommand{\bpo}{{\bf b\xspace}}
\newcommand{\cpo}{{\bf c\xspace}}
\newcommand{\Cpo}{{\bf C\xspace}}
\newcommand{\dpo}{{\bf d\xspace}}
\newcommand{\epo}{{\bf e\xspace}}
\newcommand{\ppo}{{\bf p\xspace}}
\newcommand{\fpo}{{\bf f\xspace}}
\newcommand{\gpo}{{\bf g\xspace}}
\newcommand{\Gpo}{{\bf G\xspace}}
\newcommand{\hpo}{{\bf h\xspace}}
\newcommand{\kpo}{{\bf k\xspace}}
\newcommand{\Kpo}{{\bf K\xspace}}
\newcommand{\lpo}{{\bf l\xspace}}
\newcommand{\Lpo}{{\bf L\xspace}}
\newcommand{\mpo}{{\bf m\xspace}}
\newcommand{\rpo}{{\bf r\xspace}}
\newcommand{\spo}{{\bf s\xspace}}
\newcommand{\tpo}{{\bf t\xspace}}
\newcommand{\upo}{{\bf u\xspace}}
\newcommand{\Upo}{{\bf U\xspace}}
\newcommand{\vpo}{{\bf v\xspace}}
\newcommand{\wpo}{{\bf w\xspace}}
\newcommand{\xpo}{{\bf x\xspace}}
\newcommand{\ypo}{{\bf y\xspace}}
\newcommand{\zpo}{{\bf z\xspace}}
\newcommand{\Zpo}{{\bf Z\xspace}}
\newcommand{\Spo}{{\bf S}}
\newcommand{\Ypo}{{\bf Y}}
\newcommand{\NTTPSI}{{\gamma}}
\newcommand{\algo}[1]{\textsf{#1}}
\newcommand{\PeikertDBL}{\algo{dbl}}
\newcommand{\PeikertREC}{\algo{rec}}
\newcommand{\PowMul}{{\text{\sf PowMul}}}
\newcommand{\PowMulPsi}{{\text{\sf PowMul}_{\psi}}}
% usenix.sty - to be used with latex2e for USENIX.
% To use this style file, look at the template usenix_template.tex
%
% $Id: usenix.sty,v 1.2 2005/02/16 22:30:47 maniatis Exp $
%
% The following definitions are modifications of standard article.sty
% definitions, arranged to do a better job of matching the USENIX
% guidelines.
% It will automatically select two-column mode and the Times-Roman
% font.
%
% USENIX papers are two-column.
% Times-Roman font is nice if you can get it (requires NFSS,
% which is in latex2e.
\if@twocolumn\else\input twocolumn.sty\fi
\usepackage{mathptmx} % times roman, including math (where possible)
%
% USENIX wants margins of: 1" sides, 1" bottom, and 1" top.
% 0.25" gutter between columns.
% Gives active areas of 6.5" x 9"
%
\setlength{\textheight}{9.0in}
\setlength{\columnsep}{0.25in}
\setlength{\textwidth}{6.50in}
\setlength{\topmargin}{0.0in}
\setlength{\headheight}{0.0in}
\setlength{\headsep}{0.0in}
% Usenix wants no page numbers for camera-ready papers, so that they can
% number them themselves. But submitted papers should have page numbers
% for the reviewers' convenience.
%
%
% \pagestyle{empty}
%
% Usenix titles are in 14-point bold type, with no date, and with no
% change in the empty page headers. The whole author section is 12 point
% italic--- you must use {\rm } around the actual author names to get
% them in roman.
%
\def\maketitle{\par
\begingroup
\renewcommand\thefootnote{\fnsymbol{footnote}}%
\def\@makefnmark{\hbox to\z@{$\m@th^{\@thefnmark}$\hss}}%
\long\def\@makefntext##1{\parindent 1em\noindent
\hbox to1.8em{\hss$\m@th^{\@thefnmark}$}##1}%
\if@twocolumn
\twocolumn[\@maketitle]%
\else \newpage
\global\@topnum\z@
\@maketitle \fi\@thanks
\endgroup
\setcounter{footnote}{0}%
\let\maketitle\relax
\let\@maketitle\relax
\gdef\@thanks{}\gdef\@author{}\gdef\@title{}\let\thanks\relax}
\def\@maketitle{\newpage
\vbox to 2.5in{
\vspace*{\fill}
\vskip 2em
\begin{center}%
{\Large\bf \@title \par}%
\vskip 0.375in minus 0.300in
{\large\it
\lineskip .5em
\begin{tabular}[t]{c}\@author
\end{tabular}\par}%
\end{center}%
\par
\vspace*{\fill}
% \vskip 1.5em
}
}
%
% The abstract is preceded by a 12-pt bold centered heading
\def\abstract{\begin{center}%
{\large\bf \abstractname\vspace{-.5em}\vspace{\z@}}%
\end{center}}
\def\endabstract{}
%
% Main section titles are 12-pt bold. Others can be same or smaller.
%
\def\section{\@startsection {section}{1}{\z@}{-3.5ex plus-1ex minus
-.2ex}{2.3ex plus.2ex}{\reset@font\large\bf}}
Supports Markdown
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