A logical framework for reasoning on data access control policies

In this paper we propose a logic formalism that naturally supports rite encoding of complex security specifications. This formalism relies on a hierarchically structured domain made of subjects, objects and privileges. Authorizations are expressed by logic rules. The formalism supports both negation by failure (possibly unstratified) and mle negation. The latter is used to express negative authorizations. It turns out that conflicts may result from a set of authorization rules. Dealing with such conflicts requires the knowledge of the domain structure, such as grantor priorities and object/subject hierarchies, which is used in the deductive process to determine which authorization prevails, if any, on the others. Often, however; conflicts are unsolvable, as they express intrinsic ambiguities. We have devised two semantics as an extension of the well-founded and the stable model semantics of logic programming. We have also defined a number of access policies, each based on two orthogonal choices: one is related to the way how we cope with multiplicity of authorization sets in case of stable model semantics; the other is concerned with the open/closed assumption. A comparative analysis of the proposed authorization policies, based oil their degree of permissivity, shows that they form a complete lattice.