Reasoning about policy behavior in logic-based trust management systems: Some complexity results and an operational framework





Publicado en

Actas de las XV Jornadas de Programación y Lenguajes (PROLE 2015)


All rights reserved to their respective owners


In this paper we show that the logical framework proposed by Becker et al. [1] to reason about security policy behavior in a trust management context can be captured by an operational framework that is based on the language proposed by Miller in 1989 to deal with scoping and/or modules in logic programming. The framework of Becker et al. uses propositional Horn clauses to represent both policies and credentials, implications in clauses are interpreted in counterfactual logic, a Hilbertstyle proof system is defined and a system based on SAT is used to prove whether properties about credentials, permissions and policies are valid, i.e. true under all possible policies. Our contributions in this paper are three. First, we show that this kind of validation can rely on an operational semantics (derivability relation) of a language very similar to Miller’s language, which is very close to derivability in logic programs. Second, we are able to establish that, as in propositional logic, validity of formulas is a co-NP-complete problem. And third, we present a provably correct implementation of a goal-oriented algorithm for validity.


Acerca de Pasarella, Edelmira

Palabras clave


Página completa del ítem
Notificar un error en este resumen
Mostrar cita
Mostrar cita en BibTeX
Descargar cita en BibTeX