%\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 model and correctness proof 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: