%\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: