@book{SR--2008--01,
author={Christoph Benzm{\"u}ller},       
title={Automating Access Control Logics in Simple Type Theory with LEO-II},
publisher ={{SEKI Publications}},
series    ={{SEKI-Report SR--2008--01 (ISSN 1437-4447)}},
address   ={Saarland Univ.},
year      ={2008},
note      ={{\url{www.ags.uni-sb.de/~cp/SEKI/welcome.html}}},
abstract  ={Garg and Abadi recently proved that prominent access
  control logics can be translated in a sound and complete way into
  modal logic S4. We have previously outlined how normal multimodal
  logics, including monomodal logics K and S4, can be embedded in
  simple type theory and we have demonstrated that the higher-order
  theorem prover LEO-II can automate reasoning in and about them. In
  this paper we combine these results and describe a sound embedding
  of different access control logics in simple type theory. Employing
  this framework we show that the off the shelf theorem prover LEO-II
  can be applied to automate reasoning in prominent access control
  logics.},
}