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 (counter model 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, counter model 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.
展开▼
