Automating Access Control Logics in Simple Type Theory with LEO-II

TL;DR

This paper demonstrates how to embed access control logics into simple type theory and use the LEO-II theorem prover to automate reasoning tasks in these logics.

Contribution

It provides a sound and complete embedding of access control logics into simple type theory, enabling automated reasoning with LEO-II.

Findings

LEO-II can automate reasoning in access control logics

Embedding is sound and complete

Framework facilitates reasoning in prominent access control logics

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 (which is also known as higher-order logic) 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 prominent access control logics.