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.
Logics in Access Control: A Conditional Approach
GLIOZZI, Valentina;POZZATO, GIAN LUCA
2014-01-01
Abstract
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.File | Dimensione | Formato | |
---|---|---|---|
JLC_access control.pdf
Accesso aperto
Descrizione: versione inviata all'editore
Tipo di file:
POSTPRINT (VERSIONE FINALE DELL’AUTORE)
Dimensione
819.33 kB
Formato
Adobe PDF
|
819.33 kB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.