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.
2014
24
4
705
762
http://logcom.oxfordjournals.org/cgi/reprint/exs040? ijkey=mEzfmA0eg4m63C2&keytype=ref
access control; conditional logics; intuitionistic logic; sequent calculi; labelled deductive systems
Valerio Genovese; Laura Giordano; Valentina Gliozzi; Gian Luca Pozzato
File in questo prodotto:
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.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/2318/106000
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 7
  • ???jsp.display-item.citation.isi??? 4
social impact