The Knowledge Base Paradigm Applied to Delegation Revocation

Abstract

In ownership-based access control frameworks with the possibility of delegating permissions and administrative rights, delegation chains will form. There are di erent ways to treat delegation chains when revoking rights, which give rise to di erent revocation schemes. In this paper, we investigate the problem of delegation revocation from the perspective of the knowledge base paradigm. A knowledge base is a formal speci cation of domain knowledge in a rich formal language. Multiple forms of inference can be applied to this formal speci cation in order to solve various problems and tasks that arise in the domain. In other words, the paradigm proposes a strict separation of concerns between information and problem solving. The knowledge base that we use in this paper speci es the e ects of the various revocation schemes. By applying di erent inferences to this knowledge base, we can solve the following tasks: to determine the state of the system after a certain delegation or revocation; to interactively simulate the progression of the system state through time; to determine whether a user has a certain permission or administrative right given a certain state of the system; to verify invariants of the system; and to determine which revocation schemes give rise to a certain speci ed set of desired outcomes.

Introduction

In ownership-based frameworks for access control, it is common to allow principals (users or processes) to grant both permissions and administrative rights to other principals in the system. Often it is desirable to grant a principal the right to further grant permissions and administrative rights to other principals. This may lead to delegation chains starting at a source of authority (the owner of a resource) and passing on certain permissions to other principals in the chain [ 20, 23, 7, 27 ].

Furthermore, such frameworks commonly allow a principal to revoke a permission that she granted to another principal [ 17, 28, 7, 3 ]. Depending on the reasons for the revocation, di erent ways to treat the chain of principals whose permissions depended on the second principal's delegation rights can be desirable [ 17, 8 ]. For example, if one is revoking a permission given to an employee because he is moving to another position in the company, it makes sense to keep the permissions of principals who received them from this employee; but if one is revoking a permission from a user who has abused his rights and is hence distrusted by the user who granted the permission, it makes sense to delete the permissions of principals who received them from this user. Any algorithm that determines which permissions to keep intact and which permissions to delete when revoking a permission is called a revocation scheme.

Hagstrom et al. [ 17 ] have presented a framework for classifying possible revocation schemes along three dimensions: the extent of the revocation to other grantees (propagation), the e ect on other grants to the same grantee (dominance), and the permanence of the negation of rights (resilience). Since there are two options along each dimension, there are in total eight di erent revocation schemes in Hagstrom et al.'s framework. This classi cation was based on revocation schemes that had been implemented in database management systems [ 16, 15, 5, 4 ].

In this paper, we investigate the problem of delegation revocation from the perspective of the knowledge base paradigm, a declarative programming paradigm based on the idea of strictly separating information and problem solving. A knowledge base is a formal speci cation of domain knowledge in a rich formal language. Multiple forms of inference can be applied to this formal speci cation in order to solve various problems and tasks that arise in the domain. The IDP system is an implementation of the knowledge base paradigm with associated formal language FO( ), an extension of rst-order logic [ 12 ].

In this paper we present an application of the knowledge base paradigm to delegation revocation, realized in the IDP system. We have written a formal speci cation of the eight revocation schemes in Hagstrom et al.'s framework, which formally described their e ects. By applying di erent inferences to this speci cation, we can solve various tasks that can be useful both for implementing a system which allows for these revocation schemes and for supporting a user of such a system: Given a certain state of the system and a certain action (delegation or revocation), one inference determines the state of the system after this action. Another inference can interactively simulate the progression of the system state through time. A third determines whether a user has a certain permission or administrative right given a certain state of the system. A fourth inference allows to verify that the system satis es certain invariants. Finally, there is an inference that allows a user to specify a set of desired outcomes (e.g. that a certain user should no longer have a certain right while another user is una ected) and determine which actions give rise to this outcome.

The paper is structured as follows: We introduce Hagstrom et al.'s delegation revocation framework in Section 2. In Section 3 we motivate and describe the knowledge base paradigm, the IDP system and its speci cation language FO( ). Section 4 presents the application of the knowledge base paradigm to Hagstrom et al.'s framework. Section 5 discusses related work and section 6 concludes. 2

The delegation revocation framework

In this section we present Hagstrom et al.'s [ 17 ] delegation revocation framework in a slightly simpli ed way.

Let P be the set of principals (users or processes) in the system, let O be the set of objects for which authorizations can be stated, and let A be the set of access types, i.e. of actions that principals may perform on objects. For every object o 2 O, there is a source of authority (SOA), for example the owner of le o, which is a principal that has full power over object o and is the ultimate authority with respect to accesses to object o. For any a 2 A and o 2 O, the SOA of o can grant the right to access a on object o to other principals in the system, and can also delegate the right to grant access and to grant this delegation right. Therefore two kinds of permissions are distinguished: Permission means that only access right is granted, while permission means that both access and delegation rights are granted. Additionally, Hagstrom et al.'s framework allows for negative authorizations, which can be used to block a principal's access or delegation rights without deleting any authorization. Due to space limitations, we restrict ourselves to the fragment of Hagstrom et al.'s framework consisting of positive authorizations only. In a technical report to this paper, negative authorizations are taken into account [ 9 ].

We assume that all authorizations in the system are stored in an authorization speci cation, and that every authorization is of the form (i; j; a; o; ), where i; j 2 P , a 2 A, o 2 O, and 2 f ; g is a permission. The meaning of this authorization is that principal i is granting some permission concerning access type a on object o to principal j. If b is T , the permission contains the right to delegate the permission further.

Note that there is no interaction between the rights of principals concerning di erent access-object pairs (a; o), so we can consider a and o to be xed for the rest of the paper. Therefore we simplify an authorization (i; j; a; o; ) to (i; j; ). 2.1

Delegation chains and connectivity property Hagstrom et al. use the notion of a principal p having a permission without formally de ning it. The intended meaning of this can be formalized using the notion of a rooted delegation chain:1 1The idea to formalize Hagstrom et al.'s notion of having a permission in this way was rst proposed by Aucher et al. [ 1 ].

is a sequence p1; : : : ; pn of i there is a rooted delegation chain for principal p De nition 1 A rooted delegation chain for principal i with respect to permssion principals satisfying the following properties: 1. p1 is the source of authority. 2. pn is i. 3. For every integer k with 1 4. For every integer k with 1 5. n = .

k < n, an authorization (pk; pk+1; k) is in place.

k < n 1, k = .

De nition 2 We say that a principal p has permission with respect to permission .

Hagstrom et al.'s framework allows an authorization (i; j; ) to be in the authorization speci cation only if i has delegation right. This is called the connectivity property, and it can be viewed as an invariant that any system based on Hagstrom et al.'s framework needs to satisfy: Connectivity property: For every authorization (i; j; ) in the authorization speci cation, i has permission . 2.2

The three dimensions Hagstrom et al. [ 17 ] have introduced three dimensions according to which revocation schemes can be classi ed. These are called propagation, dominance and resilience:

Propagation. The decision of a principal i to revoke an authorization previously granted to a principal j may either be intended to a ect only the direct recipient j or to a ect all the other users in turn authorized by j. In the rst case, we say that the revocation is local, in the second case that it is global.

Dominance. This dimension deals with the case when a principal losing a permission in a revocation still has permissions from other grantors. If these other grantors' are dependent on the revoker, she can dominate these grantors and revoke the permissions from them. This is called strong revocation. The revoker can also perform a weak revocation, where permissions from other grantors to a principal losing a permission are kept.

In order to formalize this dimension, we need to de ne what we mean by a principal's delegation rights to be independent of another principal: De nition 3 A principal j has delegation rights independent of a principal i with respect to permission there is an rooted delegation chain for j with respect to that does not contain the principal i. i

Resilience. This dimension distinguishes revocation by removal of positive authorizations from revocation by negative authorizations which just inactivate positive authorizations. Given that we concentrate on the fragment of Hagstrom et al.'s framework without negative revocations, we will not explain this dimension in detail.

Since there are two options along each of the three dimensions, Hagstrom et al. de ned eight di erent revocation schemes. The technical report of this paper contains an illustration of these revocation schemes [ 9 ]. 3

The knowledge base paradigm and the FO( ) KB project

Declarative systems have proven their merit in many application domains: From planning to scheduling to security contexts, many challenges have been tackled using declarative approach. For example, Barker et al. [ 2 ] used a rule-based approach to determine access rights in an access control system. Advantages of such an approach are readability and maintainability of a speci cation. However, only one task is supported in a rule based system, or in any other decalarative system. Every system has its own syntactical style, terminology, conceptualization, and designated style of inference (rule based systems do chaining, databases do querying, answer set programming generates answer sets, etc.). Yet, in all of them, propositions need to be expressed. Take, e.g., \each lecture takes place at some time slot". This proposition could be an expression to be deduced from a formal speci cation if the task was a veri cation problem, or to be queried in a database, or it could be a constraint for a scheduling problem. It is, in the rst place, just a piece of information and we see no reason why depending on the task to be solved, it should be expressed in a di erent formalism.

The knowledge base (KB ) paradigm [ 14 ] was proposed as an answer to this. The KB paradigm applies a strict separation of concerns to information and problem solving. A KB system allows information to be stored in a knowledge base, and provides a range of inference methods. With these inference methods various types of problems and tasks can be solved using the same knowledge base. As such the knowledge base is neither a program nor a description of a problem, it cannot be executed or run. It is nothing but information. However, this information can be used to solve multiple sorts of problems. Many declarative problem solving paradigms are mono-inferential: they are based on one form of inference. In comparison, the KB paradigm is multi-inferential.

The FO( ) KB project is a research project in which an implementation of the KB paradigm is being developed. Its aim is to integrate di erent useful language constructs and forms of inference from di erent declarative paradigms in one rich declarative language and a KB system. So far, it has led to the KB language FO( ) [ 13 ] and the KB system IDP [ 12 ], which are used in this paper. 3.1

The speci cation language FO( ) FO( ) refers to a class of extensions of rst-order logic (FO). The language of the current version of the IDP system (IDP 3) is FO(T, ID, Agg, arit, PF): FO extended with types, inductive de nitions, aggregates, arithmetic and partial functions (see [ 13, 22 ]). In this work, we will only work (and as such, introduce) a subset of this language: F O(T; ID): typed rst-order logic with inductive de nitions. Abusing notation, we will use FO( ) as an abbreviation of this language. 3.2

An FO( ) speci cation A speci cation of domain knowledge in FO( ) can consist of 3 types of building blocks: a vocabulary , a theory T and a (partial) structure S.

The vocabulary declares the symbols used in the associated theories and structures. It is a set of type symbols (denoted as T ) and predicate symbols (denoted as P ). Every predicate P of arity n has a xed type [ 1; : : : ; n], where 1; : : : ; n are type symbols. Variables, atoms and rst-order formulas are de ned as usual.

A theory is a set of rst-order formulas and inductive de nitions. An inductive de nition in FO( ) is a set of rules of the form P (t) ', with ' a rst-order formula. We call P (t) the head (head( )) and ' the body (body( )) of the rule. The symbols that occur in the head of a rule in are called the de ned symbols in . All other symbols that occur in are called the parameters of . The semantics used for inductive de nitions is the well-founded semantics; as argued in [ 13 ], this captures the intended meaning of all forms of inductive de nitions commonly used in mathematics and computer science. Informally a structure S satis es if the interpretation of a de ned predicate P in the well-founded model of S, constructed relative to the restriction of S to the parameters of , is exactly the relation P S .

The following example illustrates the use of an inductive de nition in a theory by presenting the de ntion of \reachable" in FO( ).

Example 1 Assume a vocabulary containing a type N ode, and 2 predicates: Edge(N ode; N ode) and Reachable(N ode; N ode). Informally, Edge states that there is an edge between two nodes, while Reachable states that there is a path of edges between 2 notes. We de ne what reachability means in terms of the edges, using an inductive de nition in FO( ): ( 8x : Reachable(x; x): )

8x y : Reachable(x; y)

9z : Reachable(x; z) ^ Edge(z; y):

Given a vocabulary , a partial structure gives an interpretation to (a subset of) the elements of . Before we de ne formally what an interpretation is, we de ne the concept of a partial set, which is a generalisation of a set in a 3-valued context: A partial set on domain D is a function from D to ft; u; f g. A partial set is two-valued (or total) if u does not belong to its range. A (partial) structure S consists of a domain D for all types in T and an assignment of a partial set P S to each predicate or function symbol P 2 P , called the interpretation of P in S. The interpretation P S of a predicate symbol P with type [ 1; : : : ; n] in S is a partial set on domain D 1 : : : D n . In case the interpretation of a predicate P in S is a two-valued set, we abuse notation and use P S as shorthand for fdjP S (d) = tg.

We call a partial structure total if the interpretation P S of every predicate symbol P 2 P is a total set. Note that with the abuse of notation just explained, a total structure as we have de ned it can be identi ed with a rst-order structure as it is usually de ned.

Given two partial structures S = (D; I) and S0 = (D; I0), we write S p S0 (and say S is more precise than S0, or S0 expands S) i for every predicate symbol P 2 P with type [ 1; : : : ; n] and every tuple d 2 D 1 : : : D n such that P I (d) 6= u, we have P I0 (d) = P I (d). 3.3

The reasoning engine In the FO( ) KB project, a implementation of a KB System was developed: the IDP system [ 12 ]. IDP takes an FO( ) speci cation (that is, a combination of vocabularies, theories and/or structures) and can do a number of reasoning tasks, by applying a suitable form of inference on this speci cation. Below, we present the inferences that we need in this paper: Modelexpand(T; S): Input: theory T and partial structure S. Output: either a total structure I such that I is a model of T and S p I, or UNSAT if there is no such I. Modelexpand [ 26 ] is a generalization for FO( ) theories of the modelexpansion task as de ned in Mitchell et al. [ 21 ].

Allmodels(T; S): Input: theory T and partial structure S. Output: the set of all total structures I such that

I is a model of T and S p I.

Query(S; E): Input: a (partial) structure S and a set expression E = fx j '(x)g. Output: the set AQ = fx j '(x)S = tg.

Progression(T; Si): In [ 6 ], LTC theories (Linear Time Calculus) are proposed, a syntactic subclass of FO( ) theories that allow to naturally model dynamic systems. An LTC theory consists of three types of constraints: constraints about the initial situation, invariants, and \bistate" formulas that relate the state on the current point in time with that of the next. Note that the speci cation presenten in Subsection 4.1 below is an LTC theory.

The Progression inference: Input: an LTC theory T and a structure Si that provides information about the state of the system on a time point t. Output: a structure St+1 that represents the next state (or a next possible state) at time point t + 1. Repeating this process, we can compute all subsequent states, e ectively simulating the dynamic system de ned by T . 4

Delegation revocation in the KB paradigm

In this section, we explain how the KB paradigm can be applied to delegation revocation. For this purpose, we show how the delegation revocation framework de ned in Section 2 can be speci ed in FO( ), and how inferences on this speci cation can solve various tasks that arise in the domain. Some of these tasks are tasks that any system implementing the delegation revocation framework needs to solve, while others are tasks that support a user of such a system.

We have built a prototype in IDP in which this application of the KB paradigm is realized. This prototype also covers the negative authorizations and negative revocation schemes that this paper does not explain due to space restrictions. This prototype can be downloaded at http://icr.uni.lu/mcramer/downloads/hagstrom-R&DS. zip and run in IDP 3. 4.1

The FO( ) speci cation of the delegation revocation framework In this subsection, we describe how Hagstrom et al.'s delegation revocation framework, which we de ned semiformally in Section 2, can be formally speci ed in FO( ).2 In this subsection, we use IDP syntax for FO( ): The symbols &, |, ~, ! and ? mean ^, _, :, 8 and 9 respectively, and <- means (in inductive de nitions).

The FO( ) speci cation models the change of the authorization speci cation over time. We allow for four types of objects: Time, principal, scheme and permission. Time points are integers. There is a constant SOA of type principal that denotes the source of authority. The type scheme consists of the four delete revocation schemes (WLD, WGD, SLD and SGD) and two schemes for granting the two di erent kinds of permissions (grant access and grant deleg). The permissions are access and deleg. Positive authorizations are modelled by the predicate pos auth. The authorizations cannot be modelled as objects, because they change over time, while FO( ) assumes a constant domain of objects.

As IDP only works with nite domains, the type Time actually just consists of a nite set of consecutive integers. There is a constant Start for the rst time point. The unary partial function Next maps a time point t to the next time point t+1, as long as t is not the last time point included in the domain.

2For a version of the speci cation that includes the formal speci cation of the vocabulary, that also covers negative authorizations, and that contains comments that clarify various details, see the le MainTheory.idp of the prototype that can be downloaded at http://icr.uni.lu/mcramer/downloads/hagstrom-R&DS.zip.

The predicate pos auth for positive authorizations takes four arguments: pos auth(t,i,j,a) means that at time t, a positive authorization from principal i to principal j for permission a is in place. There is a tertiary predicate pos auth start for specifying the positive authorizations that are in place at the rst time point.

Changes in the authorization speci cation are always triggered by some action by a principal: action(t,s,i,j) means that at time t, principal i performs an action of the (revocation or grant) scheme s a ecting principal j. These actions can lead to authorizations being deleted and/or new authorizations being included in the authorization speci cation. delete(t,i,j,a) means that between time points t-1 and t, the positive authorization from i to j for permission a gets deleted. new(t,i,j,a) means that between time points t-1 and t, a new positive authorization from i to j for permission a gets added to the authorization speci cation.

pos auth is de ned inductively by setting its values at the rst time point Start to the start con guration speci ed by pos auth start, and by modifying its values between time t and t+1 according to the changes speci ed by delete and new: f p o s a u t h ( S t a r t , p1 , p2 , a )< p o s a u t h s t a r t ( p 1 , p2 , a ) . p o s a u t h ( N e x t ( t ) , p1 , p2 , a )< p o s a u t h ( t , p1 , p2 , a ) & p o s a u t h ( N e x t ( t ) , p1 , p2 , a )< new(Next(t ) , p1 , p2 , a ) . g d e l e t e ( N e x t ( t ) , p1 , p2 , a ) .

The predicate chain(t,i,a) expresses that at time t, there exists a rooted delegation chain for principal i with respect to permission a. In Section 2, rooted delegation chains are de ned by quantifying over sequences of principals. This is in e ect a second-order quanti cation, which is not possible in the rst-order language FO( ). However, chain(t,i,a) can be equivalently de ned through an inductive de nition as follows:3 f c h a i n ( t , SOA, d e l e g ) .

c h a i n ( t , p1 , a ) < ? p2 : c h a i n ( t , p2 , d e l e g ) & p o s a u t h ( t , p2 , p1 , a ) . g

The predicate can delegate(t,i) expresses that principal i has permission del. The predicate ind(t,i,j,a) models the independence of principal i from principal j with respect to a permission a, and the access right of principal i. These two predicates are de ned as follows: c a n d e l e g a t e ( t , i ) < i n d ( t , SOA, p , a ) < i n d ( t , p1 , p2 , a ) <

? a1 : c h a i n ( t , i , d e l e g ) . g SOA = p .

p1 = p2 & ?p : i n d ( t , p , p2 , a ) & p o s a u t h ( t , p , p1 , a ) . g f f f f

The di erent e ects of the di erent deletion revocation schemes are captured by the de nitions of the predicates delete and new. delete is de ned via an inductive de nition with four clauses: d e l e t e ( N e x t ( t ) , i , j , a )< p o s a u t h ( t , i , j , a ) & a c t i o n ( t , s , i , j ) &

( s=WLD j s=SLD j s=WGD j s=SGD) . d e l e t e ( N e x t ( t ) , j , k , a )< p o s a u t h ( t , j , k , a ) & c a n d e l e g a t e ( N e x t ( t ) , j ) . d e l e t e ( N e x t ( t ) , k , j , a )< p o s a u t h ( t , k , j , a ) & a c t i o n ( t , SLD, i , j ) & i n d ( t , k , i , a1 ) . d e l e t e ( N e x t ( t ) , z , w, a )< p o s a u t h ( t , z , w, a ) & a c t i o n ( t ,SGD, i , j )

& d e l e t e ( N e x t ( t ) , p , w, a1 ) & i n d ( t , z , i , a2 ) . g The rst clause just states that in any deletion revocation scheme from i to j, the positive authorization from i to j is deleted. The second clause de nes the propagation of deletion by specifying that any positive authorization from i to j gets deleted if i is losing its delegation right. The last two clauses capture the meaning of strong vs. weak dominance by specifying the additional deletions that are needed in strong revocation schemes.

The predicate new takes care that new authorizations are added either when an action to grant a new permission takes place ( rst clause of the de nition of new) or when a local revocation requires the addition of a new authorization (second clause): new(Next(t ) , i , j , a ) < ? ds : ( ( d s=g r a n t a c c e s s & a = a c c e s s ) j ( d s=g r a n t d e l e g & a = d e l e g ) ) & a c t i o n ( t , ds , i , j ) & c a n d e l e g a t e ( t , i ) . new(Next(t ) , i , k , a ) < ? j s : ( s=WLD j s=SLD) & a c t i o n ( t , s , i , j ) & ( ? z : p o s a u t h ( t , z , k , a ) & c a n d e l e g a t e ( t , z ) ) &

( ? z : p o s a u t h ( t , z , k , a ) & c a n d e l e g a t e ( N e x t ( t ) , z ) ) . g 3Note that rst-order logic with inductive de nitions has an expressivity that lies strictly between the expressivity of rst-order and second-order logic. Informally, the second clause of this de nition says that if in a local revocation scheme revoking a positive authorization from principal i to principal j, j is losing its delegation right, then every positive authorization from j to another principal k must be replaced by a positive authorization of the same authorization type from i to k. This new authorization from i to k ensures that the propagation de ned in the second clause of the de nition of delete does not continue beyond j.

The predicate access right(t,i) means that principal i has access right at time t: f a c c e s s r i g h t ( t , p ) <

c h a i n ( t , p , a ) . g In this subsection we explain how di erent logical inferences, when applied to the FO( ) speci cation explained above, can solve various tasks that can be useful both for implementing a system which allows for delegation revocation and for supporting a user of such a system.

Let us rst consider tasks that a system that implements Hagstrom et al.'s delegation revocation framework needs to solve. Given a certain state of the system, de ned by which authorizations are currently included in the authorization speci cation, and a given action (a delegation or revocation performed by some principal), the new state of the system after this action needs to be determined. This task can be performed using the Modelexpand inference as follows: Let T be the FO( ) speci cation of the delegation revocation framework. Let S be a partial structure with the following properties:

The time domain of S contains only the two time points 0 and 1.

S assigns to the predicate pos auth start the set of all authorizations currently included in the authorization speci cation.

S assigns to the predicate action the given action at time 0.

The value of all other predicates is unde ned in S.

In this case, Modelexpand(T ,S) is a total structure that expands S and that is a model of T . Being a total structure, it assigns to pos auth a set A of quadruples of the form (t; i; j; a), where t is a time point (0 or 1), i and j are principals and a is a permission. Then the set A0 := f(i; j; a) j (1; i; j; a) 2 Ag is the set of authorizations that constitutes the authorization speci cation after the action. (Note that since all predicates other than pos auth start and action are de ned in T through an inductive de nition, there is a unique model of T that expands S, so that the result of this inference is deterministic.)

This way we can determine the e ect of a single action. It could be iterated by setting the value of pos auth start to be A0 for the next iteration of this procedure. But the IDP system also supports an inference, namely the Progression inference, that is designed for this kind of temporal progression of a structure based on a theory with a type for time. The input structure of this inference provides information about the state of the system on a time point t; in our case that is the authorization speci cation at a given time. The output is a structure that represents the state of the authorization speci cation at time point t + 1. So the step of extracting A0 from A that was required for iterating the above inference is no longer needed. So this inference can more straightforwardly be iterated, giving rise to an interactive simulation of the progression of the system state through time.

Of course, a system implementing Hagstrom et al.'s framework does not only need to determine how the authorization speci cation changes over time, but also needs to determine whether a principal requesting access or performing a certain administrative action actually has access right or the right to perform the action in question. This can be done with the Query inference: For example, if S is the partial structure that assigns to the predicate pos auth start the set of all authorizations currently included in the authorization speci cation, Query(S,fi j access right(Start,i)g) returns the set of principals that have access right according to the current authorization speci cation.

When designing a system, one can avoid an erroneous design by specifying invariants that the system must satisfy at any moment during the execution of the system, and verify that these invariants are actually satis ed by the system. In the case of a system based on Hagstrom et al.'s delegation revocation system, an example of an invariant that the system must satisfy is the connectivity property de ned in subsection 2.1. We must, of course assume, that the system starts in a state that satis es the connectivity property. All that remains to be shown, then, is that if the connectivity property holds at some time point t, it must also hold at the next time point t + 1.

One way that this can be done is by calling an automated theorem prover to prove this implication. However, this is not always viable, as the theory may be too complex for an automated theorem prover to be able to nd a proof of the invariant. This is the case for our speci cation.

Another possibility is to prove that the invariant holds in xed structures. In our case, we can x a partial structure S with time points 0 and 1 and without any information about the predicates. In this case, the only information that we are xing is the number of principals. We can then prove that the invariant holds for a xed number of principals by establishing, using Modelexpand(T 0,S), that there is no total structure expanding S that is a model of the theory T 0 consisting of our speci cation T together with the statement that the connectivity property holds at time point 0 but not at time point 1. With this method, we have veri ed the connectivity property for any system with n principals for n 8.

Despite this limitation to very small domains, this limited veri cation can be useful for avoiding erroneous design, as errors tend to already show up at relatively small domains. It should be added that the logical methodology of the KB paradigm lends itself well to the usage of interactive theorem provers common in software veri cation in order to fully verify invariants over complex speci cations. The integration of IDP and interactive theorem provers is, however, still future work.

Finally, let us turn to a task that supports a user of a system based on Hagstrom et al.'s delegation revocation framework: A principal i may want to reach a certain outcome, e.g. that a given principal j should no longer have a certain right while another principal k is una ected. i may want to nd out all revocation schemes that lead to the desired outcome. This can be achieved by computing Allmodels(T2,S), where S is the structure that assigns the current authorization speci cation to pos auth start, and T2 is the theory consisting of our speci cation of the delegation revocation framework together with the statement that the action at time point 0 is performed by i, and the statement that the desired outcome holds at time point 1. The values of the predicate action at time point 0 in the models returned by Allmodels(T2,S) are the actions that i can perform in order to get the desired outcome.

Furthermore, i may want to reach a certain outcome for some given principals while minimally in uencing the permissions of other principals. In that case, i can de ne a cost function, e.g. that every change in a permission of a principal has a cost of 1, and search the models returned by Allmodels(T2,S) for the one with the minimal cost.

The IDP prototype that we have built can perform all the di erent tasks described in this subsection. 5

Related work

While the KB paradigm and its implementation IDP, are fairly young, its applicability has been investigated and illustrated in multiple domains. In [ 19 ], the connection with Business Rules was investigated. Business Rules are well-represented in industry for knowledge-intensive applications and as such were used as a comparison to evaluate the KB paradigm. A typical Business Rules application, the EU-Rent Car-Rental company, was modelled in FO( ), and two use cases were investigated.

In [ 25 ], the authors looked at applications of the IDP system, for interactive con guration systems, where the system is used to guide a user through a search space, looking for a valid con guration. The advantages of an explicit modeling of domain knowledge in con guration were large: the adaptability in case the domain knowledge changes and the fact that the same speci cation of knowledge could be reused in di erent tasks being the most important. This work was extended in [ 18 ], where eight di erent reasoning tasks used in a con guration system were identi ed and implemented using logical inferences on 1 knowledge base, containing all domain knowledge.

While the KB paradigm has not been previously applied to the problem of delegation revocation, other logical methods have been applied to this access control problem: Aucher et al. [ 1 ] presented a formalization of Hagstrom et al.'s eight revocation schemes in a dynamic variant of propositional logic that resembles imperative programming languages. Furthermore, they extended their formalization with a notion of trust. Their formalization only supports the tasks of determining the state of the system after a certain action and of determining whether a user has a certain permission given a certain state of the system; the other tasks described in this paper are not supported by their formalization.

Two of the authors of the current paper have de ned a modi ed version of Hagstrom et al.'s delegation revocation framework as well as Trust Delegation Logic, a logic of trust designed for studying the reasons for performing di erent revocation schemes de ned [ 8 ]. This work was motivated by problems we discovered with Hagstrom et al.'s delegation revocation framework when we produced the rst FO( ) speci cation of the framework, e.g. the problem that variations in the timing of the actions of various principals can have undesirable side-e ects. These problems are documented in [ 8 ], [ 11 ] and [ 10 ], and a systematic methodology to avoid problems of this kind is studied in [ 10 ]. As this example shows, formally specifying something in FO( ) can generally help understanding it better and uncovering problematic features.

In another related work, two of the authors of the current paper have de ned a modeling language for access control based on autoepistemic logic and have exempli ed its applicability to access control by modeling delegation revocation in a way that is similar to the way delegation revocation is modeled in the current paper [ 24 ]. 6

Conclusion

In this paper, we have explained the bene ts of the knowledge base paradigm when applied to delegation revocation. The knowledge base paradigm proposes a strict separation between knowledge and problem solving. In our application, the knowledge is represented by an FO( ) speci cation of Hagstrom et al. [ 17 ] delegation revocation framework. By applying various logical inferences to this speci cation, multiple tasks that arise when implementing or using a delegation revocation system were solved. This way, the same information was reused for solving various problems.

Our work constitutes a proof of concept, and we hope that it will inspire other researchers in computer security to consider the possibility of applying the methodology of the knowledge base paradigm to their research.

References

[1] Guillaume Aucher , Steve Barker, Guido Boella, Valerio Genovese, and Leendert van der Torre. Dynamics in Delegation and Revocation Schemes: A Logical Approach . In Yingjiu Li, editor, Data and Applications Security and Privacy XXV , volume 6818 of Lecture Notes in Computer Science, pages 90 { 105 . Springer Berlin, 2011 .

[2] Steve Barker . The next 700 access control models or a unifying meta-model? In Proceedings of the 14th ACM symposium on Access control models and technologies , SACMAT '09 , pages 187 { 196 . ACM, 2009 .

[3] Steve Barker , Guido Boella, Dov Gabbay, and Valerio Genovese . Reasoning about delegation and revocation schemes in answer set programming . Journal of Logic and Computation , 2014 .

[4] E. Bertino , P. Samarati , and S. Jajodia . An extended authorization model for relational databases . Knowledge and Data Engineering , IEEE Transactions on, 9 ( 1 ): 85 { 101 , Jan 1997 .

[5] Elisa Bertino , Sushil Jajodia, and Pierangela Samarati . A Non-timestamped Authorization Model for Data Management Systems . In Proceedings of the 3rd ACM Conference on Computer and Communications Security, CCS '96 , pages 169 { 178 , New York, NY, USA, 1996 . ACM.

[6] Bart Bogaerts , Joachim Jansen, Maurice Bruynooghe, Broes De Cat, Joost Vennekens, and Marc Denecker . Simulating Dynamic Systems Using Linear Time Calculus Theories . TPLP, 14 ( 4 {5): 477 { 492 , 7 2014 .

[7] Ajay Chander , Drew Dean , and John C. Mitchell . Reconstructing trust management . Journal of Computer Security , 2004 .

[8] Marcos Cramer , Diego Agust n Ambrossio, and Pieter van Hertum. A Logic of Trust for Reasoning about Delegation and Revocation . In Proceedings of the 20th ACM Symposium on Access Control Models and Technologies , pages 173 { 184 , 2015 .

[9] Marcos Cramer , Zohreh Baniasadi, and Pieter Van Hertum. Technical report of \The Knowledge Base Paradigm Applied to Delegation Revocation" . arXiv e-prints, page arXiv: 1908 .11132, Aug 2019 .

[10] Marcos Cramer and Giovanni Casini . Postulates for Revocation Schemes . In International Conference on Principles of Security and Trust , pages 232 { 252 . Springer, 2017 .

[11] Marcos Cramer , Pieter Van Hertum, Ruben Lapauw , Ingmar Dasseville, and Marc Denecker . Resilient Delegation Revocation with Precedence for Predecessors is NP-Complete . In Proceedings of the Computer Security Foundations Symposium (CSF) 2016 , in print.

[12] Broes De Cat , Bart Bogaerts, Maurice Bruynooghe, Gerda Janssens, and Marc Denecker . Predicate Logic As a Modeling Language: The IDP System . In Michael Kifer and Yanhong Annie Liu, editors, Declarative Logic Programming , pages 279 { 323 . Association for Computing Machinery and Morgan & Claypool, New York, NY, USA, 2018 .

[13] Marc Denecker and Eugenia Ternovska . A Logic of Nonmonotone Inductive De nitions . ACM Trans. Comput. Log. , 9 ( 2 ): 14 :1{ 14 : 52 , April 2008 .

[14] Marc Denecker and Joost Vennekens . Building a Knowledge Base System for an Integration of Logic Programming and Classical Logic. In Mar a Garc a de la Banda and Enrico Pontelli, editors, ICLP , volume 5366 of LNCS , pages 71 { 76 . Springer, 2008 .

[15] Ronald Fagin . On an Authorization Mechanism . ACM Trans. Database Syst ., 3 ( 3 ): 310 { 319 , September 1978 .

[16] Patricia P. Gri ths and Bradford W. Wade . An Authorization Mechanism for a Relational Database System . ACM Trans. Database Syst ., 1 ( 3 ): 242 { 255 , September 1976 .

[17] Asa Hagstr om, Sushil Jajodia, Francesco Parisi-Presicce, and Duminda Wijesekera. Revocations { A Classi cation . In Proceedings of the 14th IEEE Workshop on Computer Security Foundations, CSFW '01 , pages 44 {, Washington, DC, USA, 2001 . IEEE Computer Society.

[18] Pieter Van Hertum , Ingmar Dasseville , Gerda Janssens, and Marc Denecker . The KB Paradigm and Its Application to Interactive Con guration . In Marco Gavanelli and John H. Reppy, editors, Practical Aspects of Declarative Languages - 18th International Symposium, PADL 2016 , St . Petersburg, FL, USA, January 18 - 19 , 2016 . Proceedings, volume 9585 of Lecture Notes in Computer Science, pages 13 { 29 . Springer, 2016 .

[19] Pieter Van Hertum , Joost Vennekens , Bart Bogaerts, Jo Devriendt, and Marc Denecker . The e ects of buying a new car: an extension of the IDP Knowledge Base System . TPLP , 13 ( 4 { 5 - Online-Supplement ) , 2013 .

[20] Ninghui Li , Benjamin N. Grosof , and Joan Feigenbaum . Delegation Logic: A Logic-based Approach to Distributed Authorization . ACM Transaction on Information and System Security , 2003 .

[21] David G. Mitchell and Eugenia Ternovska . A Framework for Representing and Solving NP Search Problems . In Manuela M. Veloso and Subbarao Kambhampati, editors, AAAI , pages 430 { 435 . AAAI Press / The MIT Press, 2005 .

[22] Nikolay Pelov , Marc Denecker , and Maurice Bruynooghe. Well-founded and Stable Semantics of Logic Programs with Aggregates . TPLP , 7 ( 3 ): 301 { 353 , 2007 .

[23] Roberto Tamassia , Danfeng Yao, and William H. Winsborough . Role-Based Cascaded Delegation . In Proceedings of the 9th ACM symposium on Access control models and technologies , 2004 .

[24] Pieter Van Hertum , Marcos Cramer , Bart Bogaerts, and Marc Denecker . Distributed Autoepistemic Logic and Its Application to Access Control . In Proceedings of the Twenty-Fifth International Joint Conference on Arti cial Intelligence , IJCAI'16 , pages 1286 { 1292 . AAAI Press, 2016 .

[25] Hanne Vlaeminck , Joost Vennekens, and Marc Denecker . A logical framework for con guration software . In Antonio Porto and Francisco Javier Lopez-Fraguas, editors, Proceedings of the 11th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, September 7-9 , 2009 , Coimbra, Portugal, pages 141 { 148 . ACM, 2009 .

[26] Johan Wittocx , Maarten Marien, and Marc Denecker . The idp system: A model expansion system for an extension of classical logic . In Marc Denecker, editor, LaSh , pages 153 { 165 . ACCO , 2008 .

[27] Danfeng Yao and Roberto Tamassia . Compact and Anonymous Role-Based Authorization Chain . ACM Transactions on Information and System Security , 2009 .

[28] Longhua Zhang , Gail-Joon Ahn , and Bei-Tseng Chu . A rule-based framework for role-based delegation and revocation . ACM Transactions on Information and System Security , 2003 .