Automating Access Control Logics in Simple Type Theory with LEO-II (bibtex)
by Christoph Benzmüller
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.
Reference:
Automating Access Control Logics in Simple Type Theory with LEO-II (Christoph Benzmüller), SEKI Publications (ISSN 1437-4447), number SR-2008-01, 2008. (arXiv:0901.3574)
Bibtex Entry:
@techreport{R42,
  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.  },
  Author =	 {Christoph Benzm{\"u}ller},
  Institution =	 {Universit{\"a}t des Saarlandes},
  Address =	 {Saarbr{\"u}cken, Germany},
  Keywords =	 {own, LEO Prover, Higher Order Logic, Automated
                  Reasoning, Henkin Semantics, Security Logics},
  Note =	 {arXiv:0901.3574},
  Number =	 {SR-2008-01},
  Publisher =	 {SEKI Publications (ISSN 1437-4447)},
  Title =	 {Automating Access Control Logics in Simple Type
                  Theory with {LEO-II}},
  Type =	 {SEKI Report},
  Url =		 {http://arxiv.org/abs/0901.3574},
  Year =	 2008,
}
Powered by bibtexbrowser