\documentclass[11pt,a4paper]{article}
\usepackage[T1]{fontenc}
\usepackage{isabelle,isabellesym}
\renewcommand{\isastyletxt}{\isastyletext}

% further packages required for unusual symbols (see also
% isabellesym.sty), use only when needed

%\usepackage{amssymb}
  %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
  %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
  %\<triangleq>, \<yen>, \<lozenge>

%\usepackage{eurosym}
  %for \<euro>

%\usepackage[only,bigsqcap]{stmaryrd}
  %for \<Sqinter>

%\usepackage{eufrak}
  %for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)

%\usepackage{textcomp}
  %for \<onequarter>, \<onehalf>, \<threequarters>, \<degree>, \<cent>,
  %\<currency>

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

% urls in roman style, theory text in math-similar italics
\urlstyle{rm}
\isabellestyle{it}

% for uniform font size
%\renewcommand{\isastyle}{\isastyleminor}


\begin{document}

\title{Conservation of CSP Noninterference Security\\under Concurrent Composition}
\author{Pasquale Noce\\Security Certification Specialist at Arjo Systems, Italy\\pasquale dot noce dot lavoro at gmail dot com\\pasquale dot noce at arjosystems dot com}
\maketitle

\begin{abstract}
In his outstanding work on Communicating Sequential Processes, Hoare has defined
two fundamental binary operations allowing to compose the input processes into
another, typically more complex, process: sequential composition and concurrent
composition. Particularly, the output of the latter operation is a process in
which any event not shared by both operands can occur whenever the operand that
admits the event can engage in it, whereas any event shared by both operands can
occur just in case both can engage in it.

This paper formalizes Hoare's definition of concurrent composition and proves,
in the general case of a possibly intransitive policy, that CSP noninterference
security is conserved under this operation. This result, along with the previous
analogous one concerning sequential composition, enables the construction of
more and more complex processes enforcing noninterference security by composing,
sequentially or concurrently, simpler secure processes, whose security can in
turn be proven using either the definition of security, or unwinding theorems.
\end{abstract}

\tableofcontents

% sane default for proof documents
\parindent 0pt\parskip 0.5ex

% generated text of all theories
\input{session}

% bibliography
\bibliographystyle{abbrv}
\bibliography{root}

\end{document}
