%\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 asystem, how do we know it is really protected? To give an answer weformalise in this paper the Role-Compatibility Model---a framework,introduced by Ott, in which access control policies can beexpressed. We also give a dynamic model determining which securityrelated events can happen while a system is running. We prove that ifa policy in this framework ensures a resource is protected, then thereis really no sequence of events that would compromise the security ofthis resource. We also prove the opposite: if a policy does notprevent a security compromise of a resource, then there is a sequenceof events that will compromise it. Consequently, a static policycheck is sufficient (sound and complete) in order to guarantee orexpose the security of resources before running the system. Ourformal model and correctness proof are mechanised in theIsabelle/HOL theorem prover using Paulson's inductive method forreasoning about valid sequences of events. Our results apply to theRole-Compatibility Model, but can be readily adapted to otherrole-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: