In this paper we study the applicability of constructive conditional logics as a general framework to define decision procedures in access control logics. To this purpose, we formalize the assertion A says \phi, whose intended meaning is that principal A says that \phi, as a conditional implication. We introduce four conditional logics by combining some well known access control axioms. We identify the conditional axioms needed to capture the basic properties of the “says” operator and to provide a proper definition of boolean principals. We provide a Kripke model semantics for the logics and we prove that their axiomatization is sound and complete with respect to the semantics. Moreover, we show that in the proposed conditional access control logics we can deal with the well known “speaks for” operator introduced in the logic ABLP without the need of adding any extra machinery. Finally, we define sound, complete, cut-free sequent calculi for them. For one of the proposed logic, called CondUC ACL , 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.
A conditional constructive logic for access control and its sequent calculus
GLIOZZI, Valentina;POZZATO, GIAN LUCA
2011-01-01
Abstract
In this paper we study the applicability of constructive conditional logics as a general framework to define decision procedures in access control logics. To this purpose, we formalize the assertion A says \phi, whose intended meaning is that principal A says that \phi, as a conditional implication. We introduce four conditional logics by combining some well known access control axioms. We identify the conditional axioms needed to capture the basic properties of the “says” operator and to provide a proper definition of boolean principals. We provide a Kripke model semantics for the logics and we prove that their axiomatization is sound and complete with respect to the semantics. Moreover, we show that in the proposed conditional access control logics we can deal with the well known “speaks for” operator introduced in the logic ABLP without the need of adding any extra machinery. Finally, we define sound, complete, cut-free sequent calculi for them. For one of the proposed logic, called CondUC ACL , 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.File | Dimensione | Formato | |
---|---|---|---|
TABLEAUX 2011 - access control.pdf
Accesso riservato
Tipo di file:
POSTPRINT (VERSIONE FINALE DELL’AUTORE)
Dimensione
340.71 kB
Formato
Adobe PDF
|
340.71 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.