Labeled Sequent Calculi for Access Control Logics: Countermodels, Saturation and Abduction

—We show that Kripke semantics of modal logic, manifest in the syntactic proof formalism of labeled sequent calculi, can be used to solve three central problems in access control: Generating evidence for denial of access (countermodel generation), finding all consequences of a policy (saturation) and determining which additional credentials will allow an access (abduction). At the core of our work is a single, non-trivial, countermodel producing decision procedure for a specific access control logic. The procedure is based on backwards search in a labeled sequent calculus for the logic. Modifications of the calculus yield a procedure for abduction and, surprisingly, for saturation.

• Type: Journal
• Year: 2012
• Where: CSFW
• Authors: Valerio Genovese, Deepak Garg, Daniele Rispoli
• Keywords: CSFW 2012, Kripke Semantics, Security Privacy, Sequent Calculi, Sequent Calculus