Sciweavers

CSFW
2012
IEEE

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

12 years 17 days ago
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.
Valerio Genovese, Deepak Garg, Daniele Rispoli
Added 28 Sep 2012
Updated 28 Sep 2012
Type Journal
Year 2012
Where CSFW
Authors Valerio Genovese, Deepak Garg, Daniele Rispoli
Comments (0)