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 (and complete) 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 and about prominent access control logics.
This work was supported by EU grant PIIF-GA-2008-219982 (THFTPTP).
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
The TPTP THF library, http://www.tptp.org .
Abadi, M.: Logic in access control. In: 18th IEEE Symposium on Logic in Computer Science, Ottawa, Canada, Proceedings, 22-25 June 2003. IEEE Computer Society, Los Alamitos (2003)
Andrews, P.B.: General models and extensionality. J. of Symbolic Logic 37, 395–397 (1972)
Andrews, P.B.: General models, descriptions, and choice in type theory. J. of Symbolic Logic 37, 385–394 (1972)
Andrews, P.B.: An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof, 2nd edn. Kluwer Academic Publishers, Dordrecht (2002)
Andrews, P.B.: Church’s type theory. In: Zalta, E.N. (ed.) The Stanford Encyclopedia of Philosophy (2008), http://plato.stanford.edu/archives/fall2008/entries/type-theory-church/
Andrews, P.B., Brown, C.E.: Tps: A hybrid automatic-interactive system for developing proofs. J. Applied Logic 4(4), 367–395 (2006)
Benzmüller, C.: Automating access control logics in simple type theory with LEO-II. SEKI Technical Report SR-2008-01, FB Informatik, U. des Saarlandes, Germany (2008)
Benzmüller, C., Brown, C.E., Kohlhase, M.: Higher order semantics and extensionality. J. of Symbolic Logic 69, 1027–1088 (2004)
Benzmüller, C., Paulson, L.: Festschrift in honour of Peter B. Andrews on his 70th birthday. In: Exploring Properties of Normal Multimodal Logics in Simple Type Theory with LEO-II. IFCoLog, Studies in Logic and the Foundations of Mathematics (2009)
Benzmüller, C., Rabe, F., Sutcliffe, G.: The core TPTP language for classical higher-order logic. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS, vol. 5195 (LNAI), pp. 491–506. Springer, Heidelberg (2008)
Benzmüller, C., Theiss, F., Paulson, L., Fietzke, A.: LEO-II - A cooperative automatic theorem prover for classical higher-order logic (System description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS ( LNAI), vol. 5195, pp. 162–170. Springer, Heidelberg (2008)
Brown, C.E.: Encoding hybrid logic in higher-order logic. Unpublished slides from an invited talk presented at Loria Nancy, France (April 2005), http://mathgate.info/cebrown/papers/hybrid-hol.pdf
Carpenter, B.: Type-logical semantics. MIT Press, Cambridge (1998)
Church, A.: A Formulation of the Simple Theory of Types. J. of Symbolic Logic 5, 56–68 (1940)
Gallin, D.: Intensional and Higher-Order Modal Logic. North-Holland Mathematics Studies, vol. 19. North-Holland, Amsterdam (1975)
Gamut, L.T.F.: Logic, Language, and Meaning. Intensional Logic and Logical Grammar, vol. II. The University of Chicago Press (1991)
Garg, D., Abadi, M.: A modal deconstruction of access control logics. In: Amadio, R. (ed.) FOSSACS 2008. LNCS, vol. 4962, pp. 216–230. Springer, Heidelberg (2008)
Gödel, K.: Eine interpretation des intuitionistischen aussagenkalküls. Ergebnisse eines Mathematischen Kolloquiums 8, 39–40 (1933)
Hardt, M., Smolka, G.: Higher-order syntax and saturation algorithms for hybrid logic. Electr. Notes Theor. Comput. Sci. 174(6), 15–27 (2007)
Harrison, J.: HOL Light Tutorial (for version 2.20). Intel JF1-13 (September 2006), http://www.cl.cam.ac.uk/~jrh13/hol-light/tutorial_220.pdf
Henkin, L.: Completeness in the theory of types. J. of Symbolic Logic 15, 81–91 (1950)
Kaminski, M., Smolka, G.: Terminating tableaux for hybrid logic with the difference modality and converse. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 210–225. Springer, Heidelberg (2008)
Merz, S.: Yet another encoding of TLA in isabelle (1999), http://www.loria.fr/~merz/projects/isabelle-tla/doc/design.ps.gz
Schulz, S.: E – A Brainiac Theorem Prover. Journal of AI Communications 15(2/3), 111–126 (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 IFIP International Federation for Information Processing
About this paper
Cite this paper
Benzmüller, C. (2009). Automating Access Control Logics in Simple Type Theory with LEO-II. In: Gritzalis, D., Lopez, J. (eds) Emerging Challenges for Security, Privacy and Trust. SEC 2009. IFIP Advances in Information and Communication Technology, vol 297. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-01244-0_34
Download citation
DOI: https://doi.org/10.1007/978-3-642-01244-0_34
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-01243-3
Online ISBN: 978-3-642-01244-0
eBook Packages: Computer ScienceComputer Science (R0)