--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/document/root.tex	Fri Apr 12 10:46:43 2013 +0100
@@ -0,0 +1,145 @@
+%\documentclass[10pt, conference, compsocconf]{IEEEtran}
+\documentclass[runningheads]{llncs}
+\usepackage{mathpartir}
+\usepackage{isabelle,isabellesym}
+\usepackage{amsmath}
+\usepackage{amssymb}
+\usepackage{times}
+\usepackage{tikz}
+\usepackage{pgf}
+\usepackage{color}
+\usepackage{graphicx} 
+
+% 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[greek,english]{babel}
+  %option greek for \<euro>
+  %option english (default language) for \<guillemotleft>, \<guillemotright>
+
+%\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}
+
+\def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,}
+\renewcommand{\isasymequiv}{$\dn$}
+\renewcommand{\isasymemptyset}{$\varnothing$}
+\renewcommand{\isacharunderscore}{\mbox{$\_$}}
+\renewcommand{\isasymiota}{}
+\renewcommand{\isasymtau}{s}
+
+\renewcommand{\dagger}{\bullet}
+
+\mprset{sep=0.9em}
+%%\mprset{center=false}
+\mprset{flushleft}
+\begin{document}
+\pagestyle{empty}
+
+\noindent
+The co-authors Xingyuan Zhang and Christian Urban attest that the student 
+Chunhan Wu did all the central
+work concerning the paper.\bigskip\bigskip
+
+\includegraphics[scale=0.9]{xingyuan.jpg}\\
+\noindent
+Xingyuan Zhang
+\bigskip\bigskip
+
+\mbox{}\hspace{-8mm}\includegraphics[scale=1.2]{christian.jpg}\\
+\noindent
+Christian Urban
+
+
+\newpage
+
+\title{A Formal Model and Correctness Proof for an Access Control Policy Framework}
+\author{Chunhan Wu\inst{1,2} \and Xingyuan Zhang\inst{1} \and Christian Urban\inst{2}}
+\institute{PLA University of Science and Technology, China \and King's College London, UK}
+
+%\author{\IEEEauthorblockN{Chunhan Wu\IEEEauthorrefmark{1}\IEEEauthorrefmark{2},
+%Xingyuan Zhang\IEEEauthorrefmark{1} and
+%Christian Urban\IEEEauthorrefmark{2}}
+%\IEEEauthorblockA{\IEEEauthorrefmark{1}PLA University of Science and Technology, Nanjing, China\\ 
+%Email: wuchunhan@gmail.com, xingyuanzhang@126.com}
+%\IEEEauthorblockA{\IEEEauthorrefmark{2}King's College London, London, UK\\
+%Email: christian.urban@kcl.ac.uk}
+%}
+
+\maketitle
+
+
+\begin{abstract}
+If an access control policy promises that a resource is protected in a
+system, how do we know it is really protected? To give an answer we
+formalise in this paper the Role-Compatibility Model---a framework,
+introduced by Ott, in which access control policies can be
+expressed. We also give a dynamic model determining which security
+related events can happen while a system is running. We prove that if
+a policy in this framework ensures a resource is protected, then there
+is really no sequence of events that would compromise the security of
+this resource. We also prove the opposite: if a policy does not
+prevent a security compromise of a resource, then there is a sequence
+of events that will compromise it.  Consequently, a static policy
+check is sufficient (sound and complete) in order to guarantee or
+expose the security of resources before running the system.  Our
+formal models and correctness proofs are mechanised in the
+Isabelle/HOL theorem prover using Paulson's inductive method for
+reasoning about valid sequences of events. Our results apply to the
+Role-Compatibility Model, but can be readily adapted to other
+role-based access control models.
+\end{abstract}
+
+%\begin{IEEEkeywords}
+%Security, Role-Based Access Control, Verification, Isabelle/HOL, Inductive Method
+%\end{IEEEkeywords}
+
+
+%\IEEEpeerreviewmaketitle
+
+
+%\tableofcontents
+
+% sane default for proof documents
+%\parindent 0pt\parskip 0.5ex
+
+
+
+
+
+
+% generated text of all theories
+\input{session}
+
+% optional bibliography
+\bibliographystyle{abbrv}
+\bibliography{root}
+
+\end{document}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: t
+%%% End: