\documentclass[10pt,DIV16,a4paper,abstract=true,twoside=semi,openright]
{scrreprt}
\usepackage[USenglish]{babel}
\usepackage[numbers, sort&compress]{natbib}
\usepackage{isabelle,isabellesym}
\usepackage{booktabs}
\usepackage{paralist}
\usepackage{graphicx}
\usepackage{amssymb}
\usepackage{xspace}
\usepackage{xcolor}
\usepackage{hyperref}

\definecolor{lhWhite}        {RGB}{248,248,248}
\definecolor{lhBlack}        {RGB}{  8,  8,  8}
%
\definecolor{lhOrange}       {RGB}{243,107, 33}
\definecolor{lhGreen}        {RGB}{ 65,242, 34}
\definecolor{lhCyan}         {RGB}{ 34,169,242}
\definecolor{lhMagenta}      {RGB}{211, 34,242}
\definecolor{lhGold}         {RGB}{242,211, 34}
%
\definecolor{lhOrangeMedium} {RGB}{156, 69, 22}
\definecolor{lhGreenMedium}  {RGB}{ 42,156, 22}
\definecolor{lhCyanMedium}   {RGB}{ 22,109,156}
\definecolor{lhMagentaMedium}{RGB}{135, 22,156}
\definecolor{lhGoldMedium}   {RGB}{156,135, 22}
%
\definecolor{lhOrangeDark}   {RGB}{ 71, 31, 10}
\definecolor{lhGreenDark}    {RGB}{ 19, 71, 10}
\definecolor{lhCyanDark}     {RGB}{ 10, 50, 71}
\definecolor{lhMagentaDark}  {RGB}{ 62, 10, 71}
\definecolor{lhGoldDark}     {RGB}{ 51, 86, 28}
%
\definecolor{lhLightGray}    {RGB}{204,204,204}
\definecolor{lhDarkGray}     {RGB}{ 68, 68, 68}

\usepackage{dirtree}
\renewcommand*\DTstylecomment{\ttfamily\itshape}

\usepackage{ifthen}
\usepackage{lh-listings}
\usepackage{railsetup}

\sloppy

\pagestyle{headings}
\isabellestyle{default}
\setcounter{tocdepth}{1}
\newcommand{\ie}{i.\,e.\xspace}
\newcommand{\eg}{e.\,g.\xspace}
%\newcommand{\thy}{\isabellecontext}
%\renewcommand{\isamarkupsection}[1]{%
%  \begingroup% 
%  \def\isacharunderscore{\textunderscore}%
%  \section{#1 (\thy)}%
%  \def\isacharunderscore{-}%
%  \expandafter\label{sec:\isabellecontext}%
%  \endgroup% 
%}

\title{Automated Stateful Protocol Verification}
\author{%
\begin{minipage}{.8\textwidth}
  \centering
      \href{https://www.dtu.dk/english/service/phonebook/person?id=64207}{Andreas~V.~Hess}\footnotemark[1]
      \qquad\qquad
      \href{https://people.compute.dtu.dk/samo/}{Sebastian~M{\"o}dersheim}\footnotemark[1]
      \\
      \href{http://www.brucker.ch/}{Achim~D.~Brucker}\footnotemark[2]
      \qquad\qquad
      \href{https://people.cs.aau.dk/~andsch/}{Anders~Schlichtkrull}\footnotemark[3]
     \end{minipage}
}

\publishers{%
  \footnotemark[1]~DTU Compute, Technical University of Denmark, Lyngby, Denmark\texorpdfstring{\\}{, }
   \texttt{\{avhe, samo\}@dtu.dk}\\[2em]
  %
  \footnotemark[2]~
  Department of Computer Science, University of Exeter, Exeter, UK\texorpdfstring{\\}{, }
  \texttt{a.brucker@exeter.ac.uk}\\[2em]
  %
  \footnotemark[3]~
  Department of Computer Science, Aalborg University, Copenhagen, Denmark\texorpdfstring{\\}{, }
  \texttt{andsch@cs.aau.dk}
  %
}

\begin{document}
  \maketitle
  \begin{abstract}
    \begin{quote}
      In protocol verification we observe a wide spectrum from fully
      automated methods to interactive theorem proving with proof
      assistants like Isabelle/HOL.
      In this AFP entry, we present a fully-automated approach for
      verifying stateful security protocols, i.e., protocols with mutable
      state that may span several sessions.
      The approach supports reachability goals like secrecy and
      authentication.
      We also include a simple user-friendly transaction-based
      protocol specification language that is embedded into Isabelle.
      
    \bigskip
    \noindent{\textbf{Keywords:}} 
      Fully automated verification, stateful security protocols
    \end{quote}
  \end{abstract}


\tableofcontents
\cleardoublepage

\chapter{Introduction}
  In protocol verification we observe a wide spectrum from fully
  automated methods to interactive theorem proving with proof
  assistants like Isabelle/HOL. The latter provide overwhelmingly high
  assurance of the correctness, which automated methods often cannot:
  due to their complexity, bugs in such automated verification tools
  are likely and thus the risk of erroneously verifying a flawed
  protocol is non-negligible. There are a few works that try to
  combine advantages from both ends of the spectrum: a high degree of
  automation and assurance.

  Inspired by~\cite{brucker.ea:integrating:2009}, we present here a
  first step towards achieving this for a more challenging class of
  protocols, namely those that work with a mutable long-term state. To
  our knowledge this is the first approach that achieves fully
  automated verification of stateful protocols in an LCF-style theorem
  prover.  The approach also includes a simple user-friendly
  transaction-based protocol specification language embedded into
  Isabelle, and can also leverage a number of existing results such as
  soundness of a typed model (see,
  e.g.,~\cite{hess:typing:2018,hess.ea:formalizing:2017,hess.ea:typing:2018})
  and compositionality (see,
  e.g.,~\cite{hess:typing:2018,hess.ea:stateful:2018}). The Isabelle 
  formalization extends the AFP entry on stateful protocol composition and 
  typing~\cite{hess.ea:stateful:2020}.

  \begin{figure}
    \centering
    \includegraphics[height=\textheight]{session_graph}
    \caption{The Dependency Graph of the Isabelle Theories.\label{fig:session-graph}}
  \end{figure}
  The rest of this document is automatically generated from the
  formalization in Isabelle/HOL, i.e., all content is checked by
  Isabelle. \autoref{cha:manual} provides a manual of our automated protocol verification tool, called PSPSP, that is provided as part of this AFP entry. 
Thereafter, the structure of this document follows the
  theory dependencies (see \autoref{fig:session-graph}): After
  introducing the formal framework for verifying stateful security protocols
  (\autoref{cha:verification}), we continue with the setup for
  supporting the high-level protocol specifications language for
  security protocols (the Trac format) and the implementation of the
  fully automated proof tactics (\autoref{cha:trac}). Finally, we
  present examples (\autoref{cha:examples}).

\paragraph{Acknowledgments}
This work was supported by the Sapere-Aude project ``Composec: Secure Composition of Distributed Systems'', grant 4184-00334B of the Danish Council for Independent Research, by the EU H2020 project no. 700321 ``LIGHTest: Lightweight Infrastructure for Global Heterogeneous Trust management in support of an open Ecosystem of Trust schemes'' (lightest.eu) and by the ``CyberSec4Europe'' European Union's Horizon 2020 research and innovation programme under grant agreement No 830929.

\clearpage

\chapter{The PSPSP Manual}
\label{cha:manual}
\input{introduction}
\input{KeyserverEx}
\input{manual}

\chapter{Stateful Protocol Verification}
\label{cha:verification}
\input{Transactions.tex}
\input{Term_Abstraction.tex}
\input{Stateful_Protocol_Model.tex}
\input{Term_Variants.tex}
\input{Term_Implication.tex}
\input{Stateful_Protocol_Verification.tex}

\chapter{Trac Support and Automation}
\label{cha:trac}
\input{Eisbach_Protocol_Verification.tex}
\input{ml_yacc_lib.tex}
\input{trac_term.tex}
\input{trac_fp_parser.tex}
\input{trac_protocol_parser.tex}
\input{trac.tex}

\chapter{Examples}
\label{cha:examples}
\input{Keyserver.tex}
\input{Keyserver2.tex}
\input{Keyserver_Composition.tex}
\input{PKCS_Model03.tex}
\input{PKCS_Model07.tex}
\input{PKCS_Model09.tex}

% \input{session}


{\small
  \bibliographystyle{abbrvnat}
  \bibliography{root}
}
\end{document}
\endinput 
%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End:

