TY - GEN
T1 - A conditional constructive logic for access control and its sequent calculus
AU - Genovese, Valerio
AU - Giordano, Laura
AU - Gliozzi, Valentina
AU - Pozzato, Gian Luca
PY - 2011
Y1 - 2011
N2 - 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 φ, whose intended meaning is that principal A says that φ, as a conditional implication. We introduce , which is a conservative extension of the logic ICL recently introduced by Garg and Abadi. 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 logic and we prove that the axiomatization is sound and complete with respect to the semantics. Moreover, we define a sound, complete, cut-free and terminating sequent calculus for CondACL, which allows us to prove that the logic is decidable. We argue for the generality of our approach by presenting canonical properties of some further well known access control axioms. The identification of canonical properties provides the possibility to craft access control logics that adopt any combination of axioms for which canonical properties exist.
AB - 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 φ, whose intended meaning is that principal A says that φ, as a conditional implication. We introduce , which is a conservative extension of the logic ICL recently introduced by Garg and Abadi. 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 logic and we prove that the axiomatization is sound and complete with respect to the semantics. Moreover, we define a sound, complete, cut-free and terminating sequent calculus for CondACL, which allows us to prove that the logic is decidable. We argue for the generality of our approach by presenting canonical properties of some further well known access control axioms. The identification of canonical properties provides the possibility to craft access control logics that adopt any combination of axioms for which canonical properties exist.
UR - http://www.scopus.com/inward/record.url?scp=79959710786&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-22119-4_14
DO - 10.1007/978-3-642-22119-4_14
M3 - Conference contribution
AN - SCOPUS:79959710786
SN - 9783642221187
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 164
EP - 179
BT - Automated Reasoning with Analytic Tableaux and Related Methods - 20th International Conference, TABLEAUX 2011, Proceedings
T2 - 20th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2011
Y2 - 4 July 2011 through 8 July 2011
ER -