% !TeX root = Fenrir.tex


\xkcdchapter[0.6]{Proverif}{citation}{Nah, it's just details...}
\label{Appendix}

\section{Full Security Handshake}\label{Code:Proof}\index{Handshake!Proof}\index{Proof!Handshake}

\lstset{ %
  basicstyle=\tiny,			% the size of the fonts that are used for the code
  breakatwhitespace=false,	% sets if automatic breaks should only happen at whitespace
  breaklines=true,			% sets automatic line breaking
  captionpos=b,			% sets the caption-position to bottom
  %deletekeywords={...},		% if you want to delete keywords from the given language
  %escapeinside={\%*}{*)},		% if you want to add LaTeX within your code
  extendedchars=true,		% lets you use non-ASCII characters; for 8-bits encodings only, does not work with UTF-8
  frame=single,			% adds a frame around the code
  columns=flexible,
  keepspaces=true,			% keeps spaces in text, useful for keeping indentation of code (possibly needs columns=flexible)
  %morekeywords={let},		% if you want to add more keywords to the set
  numbers=none,			% where to put the line-numbers; possible values are (none, left, right)
 %stepnumber=5,			% the step between two line-numbers. If it's 1, each line will be numbered
 %numbersep=5pt,			% how far the line-numbers are from the code
  showspaces=false,		% show spaces everywhere adding particular underscores; it overrides 'showstringspaces'
  showstringspaces=false,		% underline spaces within strings only
  showtabs=false,			% show tabs within strings adding particular underscores
  tabsize=4,				% sets default tabsize to 2 spaces
  title=\lstname			% show the filename of files included with \lstinputlisting; also try caption instead of title
}

\makeatletter
\def\lst@outputspace{{\ifx\lst@bkgcolor\empty\color{white}\else\lst@bkgcolor\fi\lst@visiblespace}}
\makeatother

%\lstinputlisting{Validazione/Fenrir.pv}

\label{Fenrir proof}
\LinkInclude[style=Proverif]{Validation/Fenrir.pv}

\section{Rogue Authentication Server}\label{Rogue proof}\index{Proof!Rogue Authentication Server}

\LinkInclude[style=Proverif]{Validation/RogueAS.pv}