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 ombinations of access control axioms, we define four access control logics, namely, Cond^ACLUC, Cond ^ACLU4, Cond^ACLIC and Cond ^ACLI4. 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 Cond^ACLUC, 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 Cond ^ACLUC is in PSPACE.