Logics in Access Control: A Conditional Approach

The paper introduces a framework based on constructive conditional logics to define axiomatization, semantics and proof methods for access control logics. We formalize the well known says operator as a conditional normal modality and, by considering some specific combinations of access control axioms, we define four access control logics, namely, CondUCACL , CondU4ACL , CondICACL and CondI4ACL . Such logics integrate access control logics with intuitionistic conditional logics and provide a natural formulation of boolean principals. The well known “speaks for” operator introduced in the logic ABLP is defined on the top of the says modality. We provide a Kripke model semantics for the logics and we prove that their axiomatization is sound and complete with respect to the semantics. Also, we develop sound, complete, cut-free sequent calculi for them. For the logic CondUCACL , which (as concerns atomic principals) is slightly stronger than the logic ICL recently introduced by Garg and Abadi, we also provide a terminating sequent calculus, thus proving that the logic is decidable and that validity in CondUCACL is in PSPACE.