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

   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

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

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

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

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

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

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

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

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

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

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

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

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

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

   112 role-based access control models.

   112 role-based access control models.

   113 \end{abstract}

   113 \end{abstract}