\documentclass[11pt,a4paper]{article}
\usepackage[T1]{fontenc}
\usepackage{isabelle,isabellesym} 
\usepackage{latexsym}
\usepackage{amssymb}
\usepackage{textcomp}
\usepackage[english]{babel}
\usepackage{wasysym}
\usepackage{graphicx}

% this should be the last package used
\usepackage{pdfsetup}

% proper setup for best-style documents
\urlstyle{rm}   
\isabellestyle{it}

\hyphenation{Isabelle}

\begin{document}

\title{An Isabelle Correctness Proof for the Volpano/Smith Security Typing System}

\author{Gregor Snelting and Daniel Wasserrab\\
  IPD Snelting\\Universität Karlsruhe (TH)}

\date{\today}

\maketitle

\begin{abstract}
The Volpano/Smith/Irvine security type systems \cite{VolpanoSmith96} requires
that variables are annotated as high (secret) or low (public), and
provides typing rules which guarantee that secret values cannot leak
to public output ports. This property of a program is called
confidentiality. 

For a simple while-language without threads, our proof shows that
typeability in the Volpano/Smith system guarantees
noninterference. Noninterference means that if two initial states for
program execution are low-equivalent, then the final states are
low-equivalent as well. This indeed implies that secret values cannot
leak to public ports. For more details on noninterference and security
typing systems, see \cite{SabelfeldMyers03}.

The proof defines an abstract syntax and operational semantics for
programs, formalizes noninterference, and then proceeds by rule
induction on the operational semantics. The mathematically most
intricate part is the treatment of implicit flows. Note that the
Volpano/Smith system is not flow-sensitive and thus quite unprecise,
resulting in false alarms. However, due to the correctness property,
all potential breaks of confidentiality are discovered.
\end{abstract}

\clearpage

\tableofcontents

\clearpage

\input{session}

\bibliographystyle{plain}
\bibliography{root}

\end{document}