1 %\documentclass[10pt, conference, compsocconf]{IEEEtran}

     2 \documentclass[runningheads]{llncs}

     3 \usepackage{mathpartir}

     4 \usepackage{isabelle,isabellesym}

     5 \usepackage{amsmath}

     6 \usepackage{amssymb}

     7 \usepackage{times}

     8 \usepackage{tikz}

     9 \usepackage{pgf}

    10 \usepackage{color}

    11 \usepackage{graphicx} 

    12 

    13 % further packages required for unusual symbols (see also

    14 % isabellesym.sty), use only when needed

    15 

    16 %\usepackage{amssymb}

    17   %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,

    18   %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,

    19   %\<triangleq>, \<yen>, \<lozenge>

    20 

    21 %\usepackage[greek,english]{babel}

    22   %option greek for \<euro>

    23   %option english (default language) for \<guillemotleft>, \<guillemotright>

    24 

    25 %\usepackage[only,bigsqcap]{stmaryrd}

    26   %for \<Sqinter>

    27 

    28 %\usepackage{eufrak}

    29   %for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)

    30 

    31 %\usepackage{textcomp}

    32   %for \<onequarter>, \<onehalf>, \<threequarters>, \<degree>, \<cent>,

    33   %\<currency>

    34 

    35 % this should be the last package used

    36 

    37 \usepackage{pdfsetup}

    38 

    39 % urls in roman style, theory text in math-similar italics

    40 \urlstyle{rm}

    41 \isabellestyle{it}

    42 

    43 % for uniform font size

    44 \renewcommand{\isastyle}{\isastyleminor}

    45 

    46 \def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,}

    47 \renewcommand{\isasymequiv}{$\dn$}

    48 \renewcommand{\isasymemptyset}{$\varnothing$}

    49 \renewcommand{\isacharunderscore}{\mbox{$\_$}}

    50 \renewcommand{\isasymiota}{}

    51 \renewcommand{\isasymtau}{s}

    52 

    53 \renewcommand{\dagger}{\bullet}

    54 

    55 \mprset{sep=0.9em}

    56 %%\mprset{center=false}

    57 \mprset{flushleft}

    58 \begin{document}

    59 \pagestyle{empty}

    60 

    61 \noindent

    62 The co-authors Xingyuan Zhang and Christian Urban attest that the student 

    63 Chunhan Wu did all the central

    64 work concerning the paper.\bigskip\bigskip

    65 

    66 \includegraphics[scale=0.9]{xingyuan.jpg}\\

    67 \noindent

    68 Xingyuan Zhang

    69 \bigskip\bigskip

    70 

    71 \mbox{}\hspace{-8mm}\includegraphics[scale=1.2]{christian.jpg}\\

    72 \noindent

    73 Christian Urban

    74 

    75 

    76 \newpage

    77 

    78 \title{A Formal Model and Correctness Proof for an Access Control Policy Framework}

    79 \author{Chunhan Wu\inst{1,2} \and Xingyuan Zhang\inst{1} \and Christian Urban\inst{2}}

    80 \institute{PLA University of Science and Technology, China \and King's College London, UK}

    81 

    82 %\author{\IEEEauthorblockN{Chunhan Wu\IEEEauthorrefmark{1}\IEEEauthorrefmark{2},

    83 %Xingyuan Zhang\IEEEauthorrefmark{1} and

    84 %Christian Urban\IEEEauthorrefmark{2}}

    85 %\IEEEauthorblockA{\IEEEauthorrefmark{1}PLA University of Science and Technology, Nanjing, China\\ 

    86 %Email: wuchunhan@gmail.com, xingyuanzhang@126.com}

    87 %\IEEEauthorblockA{\IEEEauthorrefmark{2}King's College London, London, UK\\

    88 %Email: christian.urban@kcl.ac.uk}

    89 %}

    90 

    91 \maketitle

    92 

    93 

    94 \begin{abstract}

    95 If an access control policy promises that a resource is protected in a

    96 system, how do we know it is really protected? To give an answer we

    97 formalise in this paper the Role-Compatibility Model---a framework,

    98 introduced by Ott, in which access control policies can be

    99 expressed. We also give a dynamic model determining which security

   100 related events can happen while a system is running. We prove that if

   101 a policy in this framework ensures a resource is protected, then there

   102 is really no sequence of events that would compromise the security of

   103 this resource. We also prove the opposite: if a policy does not

   104 prevent a security compromise of a resource, then there is a sequence

   105 of events that will compromise it.  Consequently, a static policy

   106 check is sufficient (sound and complete) in order to guarantee or

   107 expose the security of resources before running the system.  Our

   108 formal models and correctness proofs are mechanised in the

   109 Isabelle/HOL theorem prover using Paulson's inductive method for

   110 reasoning about valid sequences of events. Our results apply to the

   111 Role-Compatibility Model, but can be readily adapted to other

   112 role-based access control models.

   113 \end{abstract}

   114 

   115 %\begin{IEEEkeywords}

   116 %Security, Role-Based Access Control, Verification, Isabelle/HOL, Inductive Method

   117 %\end{IEEEkeywords}

   118 

   119 

   120 %\IEEEpeerreviewmaketitle

   121 

   122 

   123 %\tableofcontents

   124 

   125 % sane default for proof documents

   126 %\parindent 0pt\parskip 0.5ex

   127 

   128 

   129 

   130 

   131 

   132 

   133 % generated text of all theories

   134 \input{session}

   135 

   136 % optional bibliography

   137 \bibliographystyle{abbrv}

   138 \bibliography{root}

   139 

   140 \end{document}

   141 

   142 %%% Local Variables:

   143 %%% mode: latex

   144 %%% TeX-master: t

   145 %%% End: