cpsa4manual.tex

\documentclass[11pt]{report}
\usepackage{amssymb}
\usepackage{amsmath}
\usepackage{amsthm}
\usepackage{url}
\usepackage{graphicx,geometry,color}
\usepackage{makeidx}
\usepackage{alltt}
\usepackage[hyperfootnotes=false]{hyperref}
\usepackage[all]{xy}
\usepackage{fancyhdr}
\usepackage{pdfpages}
\input{macros}

\newif\ifpubrel
%\pubreltrue
\pubrelfalse

\fancypagestyle{title}{%
  \fancyhf{}%
  \renewcommand\headrulewidth{0pt}%
  \fancyhead[L]{Approved for Public Release; Distribution Unlimited. Case Number 15-3120.}%
  \fancyfoot[C]{This technical data was produced for the
    U.S. Government\\ under Contract. No. W15P7T-13-C-A802, and is\\
    subject to the Rights in Technical Data-Noncommercial Items clause\\
    at DFARS 252.227-7013 (FEB 2012)\\
\copyright 2016 The MITRE Corporation. ALL RIGHTS RESERVED.}%
}

\pagestyle{plain}

\makeindex

\title{The Cryptographic Protocol Shapes Analyzer:\\ A Manual for CPSA
  4\thanks{\ {\copyright} 2016--2022 The
    MITRE Corporation.  Permission to copy without fee all or part of
    this material is granted provided that the copies are not made or
    distributed for direct commercial advantage, this copyright notice
    and the title of the publication and its date appear, and notice
    in given that copying is by permission of The MITRE
    Corporation.}}
\author{Moses D.~Liskov\qquad John D.~Ramsdell\\Joshua D.~Guttman\qquad Paul D.~Rowe\\ \\
  {\Large The MITRE Corporation}\\ \\ CPSA Version \version}

\makeindex
\begin{document}

\ifpubrel
\thispagestyle{title}
\fi
\maketitle
\vfill
%{\footnotesize}
%\cpsacopying
\ifpubrel
\thispagestyle{title}
\fi
\pagenumbering{roman}

\tableofcontents

\listoffigures

\listoftables

\newpage
\pagenumbering{arabic}
\setcounter{page}{1}
\input{intro}

\part{Basic use of CPSA}
\label{part:basic}
\input{setup}
\input{basic}
\input{algebra}
\part{Understanding and Guiding CPSA}
\label{part:intermediate}
\input{algorithm}
\input{declarations}
\part{Advanced features of CPSA}
\label{part:advanced}
\input{goals}
\input{channels_state}
%\input{trace_constraints}

\part{Reference material}
\label{part:reference}
\input{troubleshooting}
\input{input}
\input{tools}

\bibliography{secureprotocols}
\bibliographystyle{plain}

\printindex

% The cribsheet needs to be updated to show CPSA4 syntax.
% \newpage
% \includepdf[angle=90]{CPSA_cribsheet}

\end{document}

%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End: