A Modal Deconstruction ofAccess Control LogicsDeepak Garg1and Mart´ın Abadi2,31Carnegie Mellon University2University of California, Santa Cruz3Microsoft Research, Silicon ValleyAbstract. We present a translation from a logic of access control witha “says” operator to th e classical modal logic S4. We prove that thetranslation is sound and complete. We also show that it extends to logicswith boolean combinations of principals and with a “speaks for” relation.While a straightforward definition of this relation requires second-orderquantifiers, we use our translation for obtaining alternative, quantifier-free presentations. We also derive decidability and complexity results forthe logics of access control.1 IntroductionIn computer systems, access control checks restrict the operations that users, ma-chines, and other principals can execute on objects such as files [27]. These checksare governed by access co ntrol policies—often by the combination of several poli-cies at different laye rs and from different entities. In practice, the principals, theobjects, the formulations of policies, and their implementations can be quitevaried. The resulting gaps, inconsistencies, and obscurity endanger security.In response to these concerns, specialized logics have been proposed a s fra me-works for describing, analyzing, and enfor c ing acces s control policies (e.g., [2, 3,6, 10, 19, 20, 29, 30]). A number of research projects have applied these logics fordesigning or e xplaining var ious languages and systems (e.g., [4, 6–10,13, 14, 16,18, 26, 29, 35]). On the other hand, there have been only few, limited efforts tostudy the logics themselves (e.g., [2, 3, 19, 20]). Accordingly, the decidability, ex-pressiveness, and semantics of these logics are largely unexplored.Our objective in the present paper is to fill this gap. Specifically, we study aclass of access control logics via sound and complete tra nslations to the classicalmodal logic S4.– Relying on the theory of S4 (e.g., [24, 25]), we obtain Kripke semantics forthe logics. In the quantifier-free case, we also establish the decidability ofthe logics and their P SPACE complexity. The trans lations also open thepossibility of re-using existing decision procedures for S4.– Translating several logics to S4 enables us to compare their expressiveness. Inparticular, while a straightforward definition of the “speaks for” re lation [26,28] requires second-order quantifiers, we use our translations for obtainingalternative, quantifier-free presentations. We prove tha t these quantifier-freepresentations yield the same consequences as the second-order definition.– The translations also suggest a logic with a boolean structure on principals.Although propositional, this new logic is rich and quite expressive. Previouslogics with similar constructs allowed conjunctions and disjunctions of prin-cipals (but not negations); the present logic goes beyond them in ways thatwe consider both elegant and useful.Access control logics (those studied here and most of those in the literature)include formulas of the form A says s, where A is a principal and s is a formula.Intuitively, A says s means that A asserts (or s upports) s. For example, theadministrator admin of a domain might certify that Alice is an authorized user;this assertion may be represented as a d min says authuser(Alice). In addition,many logics support the use of the “speaks for” relation: A ⇒ B means that Asp e aks for B, that is, A says s implies B says s for every s. For example, whenKeyAlicerepresents the public key of Alice , one may write KeyAlice⇒ Alice. Whena server S acts on Alice’s behalf impersonating her, one may also write S ⇒ Alice.Despite these similarities, logics differ in their axioms. A 2003 survey discussessome of the options [1]. Recently, several works [2, 19, 20, 29] have basically reliedupon the rules of lax logic and the computational lambda calculus [11, 17, 33] forthe o perator says. This approach has several benefits, for example validatingthe “handoff axiom” [2, 26]; a detailed discussion of its fea tures is beyond thescope of this paper. We follow this approach in the logics that we consider.The first of these logics, called ICL, extends prop ositional intuitionistic logicwith the operator sa ys which behaves as a principal-indexed lax modality (Sec-tion 2). IC L can be viewed as an indexed version of CL [11], hence its name,and also as the common propositional fragment of CDD [2, Section 8] and othersystems [20, 29]. An extension of ICL, called IC L⇒, allows formulas of the formA ⇒ B (Section 3). Another extension, called ICLB, allows compound principalsformed with boolean connectives (Section 4). Our translations and the resultingtheorems apply to each of these logics. In addition, we show that A ⇒ B can beencoded using either compound principals or a se c ond-order universal quantifier(Sections 5 and 6). We conclude with a discussion of directions for further work(Section 7).Related Work. Our translations are partly based on a translation from intuition-istic logic to S4 that goes back to G¨odel [22]. Moreover, ICL can be seen as arather dir e c t generalization o f lax logic. Nevertheless, our tra nslation from ICL(and, as a special c ase, from lax logic) to S4 appears to be new.Partly fo llowing Curry [15], Fairtlough and Mendler suggested interpretinglax logic in intuitionistic logic by mapping  s to C ∨ s or to C ⊃ s, where is a la x modality and C is a fixed proposition [17]. These interpretations aresound but not c omplete. Composing them with a translation from intuitionisticlogic to S4, one can map  s to (( C) ∨ s) or to (( C) ⊃ s). A s imila rtranslation from lax logic to S4 follows fro m our definitions, as a special case;however, our translation does not put a on C, and it is sound and complete.Other interpretations of lax logic have targeted multimodal logics or intu-itionistic S4 [5, 11, 17, 34]. Our translations seem simpler; in par ticula r, they tar-get classical S4. Semantically, those interpretations lead to Kripke models withat least two accessibility relations, while we need only one.Fairtlough and Mendler also deduced the decidability of lax logic from a sub-formula property [17]. Further, Howe developed a PSPACE decision procedurefor lax logic [23]. It seems possible to extend Howe’s approach to obtain an al-ternative proof of decidability for ICL. We do not know