A Constructive Conditional Logic for Access Control:a completeness result and a sequent calculus

We define an Intuitionistic Conditional Logic for Access Control called CICL . The logic CICL is based on a conditional language allowing principals to be defined as arbitrary formulas and it includes few uncontroversial axioms of access control logics. We provide an axiomatization and a Kripke model semantics for the logic CICL , prove that the axiomatization is sound and complete with respect to the semantics, and define a sound, complete and cut-free labelled sequent calculus for it.