# Dynamics in Delegation and Revocation Schemes: A Logical Approach

Guillaume Aucher, Steve Barker, Guido Boella, Valerio Genovese, Leendert van Der Torre

► To cite this version:

Guillaume Aucher, Steve Barker, Guido Boella, Valerio Genovese, Leendert van Der Torre. Dynamics in Delegation and Revocation Schemes: A Logical Approach. 23th Data and Applications Security (DBSec), Jul 2011, Richmond, United States. pp.90-105, 10.1007/978-3-642-22348-8_9. inria-00593654v2

HAL Id: inria-00593654

https://inria.hal.science/inria-00593654v2

Submitted on 8 Sep 2013

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>
# Dynamics in Delegation and Revocation Schemes: A Logical Approach

Guillaume Aucher<fnref n="1" />, Steve Barker<fnref n="2" />, Guido Boella<fnref n="3" />, Valerio Genovese<fnref n="3" />,<fnref n="4" />, and Leendert van der Torre<fnref n="4" />

**Abstract.** In this paper we first introduce a logic for describing formally a family of delegation and revocation models that are based on the work in Hagström et al.. We then extend our logic to accommodate an episodic interpretation of trust within the framework that we define. What emerges from this work is a rich framework of formally well-defined delegation and revocation schemes that accommodates an important trust component.

# 1 Introduction

Delegation and revocation are broad concepts that are fundamentally important in modelling and reasoning about (dynamic) distributed systems. In the context of multi-agent systems (MAS), delegation is important in relation to the coordination of agents and for the coordinating of activities within organizational structures [5]. Trust is, in turn, a fundamental notion in delegation and revocation; ordinarily, a principal *i* may delegate an access privilege *a* on an object *o* to a principal *j* iff *i* trusts *j* sufficiently not to abuse the trust *i* has in *j* to perform the action *a* in relation to *o*. In the context of revocation, it is when *i* loses trust in *j*, in relation to exercising the privilege *a* on *o*, that *i* revokes the *a* privilege on *o* from *j*. Although the importance of the trust dimension has been recognized in delegation-revocation, it is our contention that more work is required on the formal specification and reasoning about trust in the context of delegation and revocation. In this paper, our focus is on formally defining a general, dynamic delegation-revocation framework that accommodates an important aspect of trust. A feature of MAS is that agents are autonomous and therefore they can act with respect to a subjective perception of the environment. For instance, a verifier may decide not to concede access to agents that she does not trust or that have been delegated by other untrusted agents. In relation to this observation, in this paper we contribute to the study of delegation and revocation in the context of distributed systems, and multi-agent systems in particular, by addressing the following key research question: *How to define a formal framework to model and reason about delegation and revocation in the context of multi-agent (and*

<footnote n="1">¹ University of Rennes 1 - INRIA, France</footnote>

<footnote n="2">² King's College London, UK</footnote>

<footnote n="3">³ University of Torino, Italy</footnote>

<footnote n="4">⁴ University of Luxembourg, Luxembourg</footnote>
*other distributed) systems?* This generally stated question breaks down into at least three important sub-questions that we intend to address: *How to update privileges on objects in a dynamic, multi-agent environment? How to specify and reason about different types of delegation and revocation schemes? How to study delegation of access privileges when trust interferes with the fact that an agent has been permitted to access?*

Our main question and each of the subquestions that we consider have been considered in the past, but the novelty of what we describe is to be understood in terms of the new formal approaches that we introduce to address them. The need for formal representations of security concepts is well understood (e.g., formal representations of security concepts are important for constructing assurance proofs). Our work is also motivated by the more specific observations that distributed access control systems can be seen as a type of a multi-agent system for which delegation models in “classical” security need to be extended. We need to also *use* our logical framework to reason about delegation-revocation policies and we require fast and effective tools for that. Delegation is an intrinsically dynamic process, therefore we additionally need to define dynamic operators that formalize a range of delegation-revocation schemes. The explicit representation of trust that we accommodate requires us to face two challenges: first, how to make the verifier autonomous to decide whether to give access in case of there being authorized but untrusted agents. Second, how to generalize the revocation policies of Hagström et al. [9] by considering whether an agent who delegated a permission is trusted or not. We address all of these issues in this paper.

The methodology that we employ in addressing these issues can be understood in the following way. First, we show that our framework can embody delegation and revocation schemes as addressed by the distributed access control community. In particular, we model all of the revocation schemes that are semi-formally introduced in [9] by using a dynamic variant of propositional logic. The work in [9] is among the most general models to handle dynamics in delegation chains and is the basis of several applied delegation models in security (Section 5 of [9]). Second, we extend the proposed framework to study relationships between trust and privilege delegation by explicitly modeling beliefs about trust relationships among agents.

Our contributions on these things can be summarized thus: (i) we formalize, in logic, the Hagström et al. framework (in [9], a semi-formal account is provided), (ii) we demonstrate the translation of our logic into “programs” (a notion that we will define later) that describe the effects of performing delegation and revocation actions, and (iii) we describe an extended form of our logic that allows for representing and reasoning about the beliefs that agents have of principals in a distributed delegation-revocation framework.

In Section 2, we describe a general authorization system, along the lines of [9], and we give some basic definitions. In Section 3, we introduce the logic that we use in order to represent formally the range of delegation and revocation schemes, of the Hagström et al. type, that we consider. In Section 4, we describe the use of our logic for representing delegation policies and, in Section 5, we
describe the use of our logic for representing revocation schemes. In Section 6, we make the key move of extending the formalization of policies expressible in the Hagström et al. framework to accommodate an epistemic logic of trust. The latter is used to account for reasoning about belief and trust in the delegation-revocation context. In Section 7, we describe related work and, in Section 8, we draw conclusions and make some suggestions for further work.

## 2 System Description

In this Section, we formalize the general concepts and notation introduced informally in [9]. The notation is intended to represent a generic access control framework using an ownership-based model with grant option for both positive and negative permissions, and where negative permissions dominate positive ones. We draw the reader's to a simplified version of the distributed authorization model described in [1,8], and illustrated in Figure 1, where an agent receives a privilege, directly or indirectly, from a *source of authority* (SOA). The SOA is an agent that has full power over a resource and is the ultimate authority w.r.t. accesses to that specific resource. The verifier is a particular agent in charge of checking whether another agent, who received a privilege directly or indirectly from the SOA, that wants to exercise an access permission is authorized so to do.

<figure><img src="image_2.png" /><figcaption>Fig. 1. The Authorization Model</figcaption></figure>

<figure><img src="image_3.png" /><figcaption>Fig. 2. Dominance Relation $\mathcal{R}$</figcaption></figure>

### 2.1 Basics

Let $\mathcal{A}\mathcal{G}$ be a finite set of *agents* (users) in the authorization system. Let $\emptyset$ be the (finite) set of system *objects* for which authorizations can be stated. Finally, let $\mathcal{A}$ be the (finite) set of *accesses* over objects; by accesses we mean the actions that agents may perform on objects. We assume that all authorizations in the system are stored in an authorization specification $\mathit{AUTH}$, and that every authorization is of the form $(i, j, (a, o), \mathit{alp}, \mathit{dlp})$ where, $i$ and $j$ are two agents, the *grantor* and the *subject*; $(a, o)$ is an *access type* and specifies an action $a$ on an object $o$; $\mathit{alp} \in \{\top, \bot\}$ (access level permission) is a flag which specifies if the authorization is an access level permission $\mathit{alp} = \top$ or an access level denial $\mathit{alp} = \bot$; $\mathit{dlp} \in \{\top, \bot\}$ (delegation level permission) is a flag which specifies whether or not the authorization gives to $j$ the authority to further delegate the permission. For instance, the authorization $(i, j, (a, o), \top, \top) \in \mathit{AUTH}$ says that agent $i$ gives agent $j$ the permission to perform action $a$ on object $o$ and
the authority to further delegate this permission to other principals. On the contrary, $(i, j, (a, o), \top, \bot) \in \mathbf{AUTH}$ means that $j$ still gets from $i$ the permission to perform the $a$ action on $o$ but she is not granted by $i$ to further delegate the permission. In case of an authorization being a denial, i.e., $alp = \bot$, we require also $dlp$ to be $\bot$ in order to represent that the agent cannot delegate a permission to access what she does not have herself. Hence, in our model we have three possible permissions (i.e., $(\top, \top)$, $(\top, \bot)$, $(\bot, \bot)$).

**Definition 1 (Positive and Negative Permissions).** *Given an authorization* $(i, j, (a, o), alp, dlp)$, *we refer to* $(alp, dlp)$ *as a negative permission if* $alp = \bot$; *otherwise, we call it a positive permission.*

When a user receives both a positive and a negative permission for the same (action, object) pair, there is a “conflict” between the two assignments. Hence, the set of permissions is divided into one set of active permissions and one set of inactive permissions. Active permissions can be inactivated when a negative permission is granted (e.g., during a revocation). Inactive permissions, instead, can be activated when a negative permission for the same target is removed.

In Figure 2, we illustrate a dominance relation $\mathcal{R}$ between permissions such that if $(alp, dlp)\mathcal{R}(alp', dlp')$ reads as, if an agent $i$ has permission $(alp, dlp)$ then it can grant an authorization of type $(i, \bot, (\bot, \bot), alp', dlp')$. Intuitively, $(alp, dlp)\mathcal{R}(alp', dlp')$ means that permission $(alp, dlp)$ is stronger than $(alp', dlp')$.

In line with [9], we require an authorization specification to satisfy the following property:

**Definition 2 (Connectivity Property).** *For all authorizations in AUTH, if an agent $i$ is the grantor of a permission $(alp, dlp)$ for permissions target $(a, o)$ to the subject $j$, then $i$ must have a permission $(alp', dlp')$ such that $(alp', dlp')\mathcal{R}(alp, dlp)$.*

The connectivity property can be considered as a constraint over the authorization specification `AUTH`. Intuitively, it assures that if an agent $i$ delegates a permission $(alp, dlp)$ to $j$ for the access type $(a, o)$ then she has the permission to do so.

**Definition 3 (Delegation Chain).** *Given an access type $(a, o)$, a delegation chain $[x_1, x_2, \dots, x_n]_{(a,o)}$ is a sequence of authorizations of the form $(x_1, x_2, (a,o), alp_1, dlp_1), \dots, (x_{n-1}, x_n, (a,o), alp_n, dlp_n)$.*

An agent $j$ is granted the access type $(a, o)$ if and only if the verifier can check the existence of a *rooted delegation chain*, which we define next.

**Definition 4 (Rooted Delegation Chain).** *A delegation chain $[x_1, x_2, \dots, x_n]_{(a,o)}$ is rooted if and only if the following hold: $x_1$ is a source of authority for object $o$; all agents $x_2, \dots, x_{n-1}$ have an active privilege $(\top, \top)$ for access type $(a, o)$; agent $x_n$ has an active privilege $(\top, dlp)$ with $dlp \in \{\top, \bot\}$.*
The notion of rooted delegation chain is pivotal because it corresponds to the notion of permission in standard access control. In this view, the connectivity property assures that if $(i, j, (a, o), alp, dlp) \in AUTH$ then there is a rooted delegation chain that links $j$ to a source of authority for $o$. In [9], Hagström et al. impose the above property to hold in any authorization specification. However, in highly distributed scenarios (e.g., GRID systems) it may be extremely difficult to enforce the connectivity property a priori for every access type $(a, o)$ (see [8] for an example). In Section 3, we relax this requirement and we give a formal account of the properties reported above in order to check whether a node in the authorization specification is part of a rooted chain.

As reported in [9], the chains of granted authorizations in a system can be represented by directed graphs. The nodes contain information about subject, object and access type, and the arcs are labelled with the granted permission $(alp, dlp)$. There is an arc from node $(i, (a, o))$ to node $(j, (a, o))$ if there is an entry in the authorization specification with $(i, j, (a, o), alp, dlp)$. An arc from node $i$ to node $j$ is labelled with the permission granted by user $i$ to user $j$.

Active arcs have unbroken lines and inactive arcs have dashed lines to indicate that although they are still in AUTH, they are not in effect because they have been overruled by a negative permission.

## 3 The Logic

We extend the propositional language Prop with dynamic operators to specify programs that update an authorization specification by issuing (or revoking) credentials certificates.

**Definition 5 (Syntax).** We define inductively the language $\mathcal{L}$ as follows:

$$ \varphi ::= p \mid \varphi \land \varphi \mid \neg \varphi \mid [\pi]\varphi \quad \pi ::= +p \mid -p \mid \varphi? \mid \pi \cup \pi \mid \pi; \pi $$

where $p$ ranges over $\Phi = \{soa_{i,o}, (i, (a, o), j)_+^D, (i, (a, o), j)_-^D, (i, (a, o), j)_+^P, (i, (a, o), j)_-^P \mid a \in A, o \in O, i, j \in AG\}$, with $A, O$ and $AG$ being finite sets.

The propositional atoms in $\Phi$ describe the state of the authorization system. $soa_{i,o}$ reads as: "agent $i$ is the source of authority over object $o$". To describe the steps of delegation chains we use triples such that $(i, (a, o), j)_+^P$ (resp. $(i, (a, o), j)_+^D$) reads as: "there is a certificate supporting that $i$ delegates an access (resp. delegation) level permission to $j$" while $(i, (a, o), j)_-^P$ (resp. $(i, (a, o), j)_-^D$) reads as: "there is a certificate supporting that $i$ gives a negative access (resp. delegation) level permission".

Given a generic dynamic formula $[\pi]\varphi$ we read it as follows: "after executing program $\pi$, the formula $\varphi$ holds true". A program is therefore intended as a sequence of instructions such that: $[+p]\varphi$ (resp. $[-p]\varphi$) reads as: "after making $p$ true (resp. false), $\varphi$ holds"; $[\varphi?]\psi$ reads as: "If $\varphi$ is true, then $\psi$ is the case"; $[\pi \cup \pi']\varphi$ reads as: "after executing $\pi$, $\varphi$ holds and, after executing $\pi'$, $\varphi$ holds"; $[\pi; \pi']\varphi$ reads as: "After executing $\pi$ and then $\pi'$, $\varphi$ holds". For readability, we adopt the following abbreviations: $(i, (a, o), j)_+^{P,D} \stackrel{\text{def}}{=} (i, (a, o), j)_+^P \land$
$(i, (a, o), j)^D_+; \neg(i, (a, o), j)^{P,D}_- \stackrel{\text{def}}{=} \neg(i, (a, o), j)^P_- \wedge \neg(i, (a, o), j)^D_-; \text{ if } \varphi \text{ then } \tau_1$ \\
\textbf{else } $\tau_2 \stackrel{\text{def}}{=} ((\varphi?; \tau_1) \cup (\neg\varphi?; \tau_2)); \text{ for all } (x \in \{s_1, \dots, s_n\}) \text{ do } \tau_1(x) \text{ end for}$ \\
$\stackrel{\text{def}}{=} \tau_1(s_1); \dots; \tau_1(s_n).$

**Definition 6 (Semantics).** A valuation $\Theta$ is a function assigning a truth value to each propositional atom: $\Theta : \Phi \to \{\top, \bot\}$. Given a valuation $\Theta$ of propositional logic and $p \in \Phi$, the updates $\Theta^{+p}$ and $\Theta^{-p}$ are defined as follows.

$$ \Theta^{+p}(q) = \begin{cases} \top & \text{if } p = q, \\ \Theta(q) & \text{otherwise.} \end{cases} \qquad \Theta^{-p}(q) = \begin{cases} \bot & \text{if } p = q, \\ \Theta(q) & \text{otherwise.} \end{cases} $$

Let $\Theta$ be a valuation and $\phi \in \mathcal{L}$. The satisfaction relation $\Theta \models \phi$ is defined inductively as follows (we omit $\neg$ and $\wedge$).

$$ \begin{align*} \Theta \models p & \iff \Theta(p) = \top \\ \Theta \models [+p]\phi & \iff \Theta^{+p} \models \phi \\ \Theta \models [-p]\phi & \iff \Theta^{-p} \models \phi \end{align*} \qquad \begin{align*} \Theta \models [\psi?]\phi & \iff \Theta \models \psi \rightarrow \phi \\ \Theta \models [\pi; \pi']\phi & \iff \Theta \models [\pi][\pi']\phi \\ \Theta \models [\pi \cup \pi']\phi & \iff \Theta \models [\pi]\phi \wedge [\pi']\phi \end{align*} $$

We exploit our basic dynamic operators to model certificate creation (granting) and deletion (revoking) by defining the following programs: $i \xrightarrow{(a,o)}_D j \stackrel{\text{def}}{=} +(i, (a, o), j)^D_+; i \xleftarrow{(a,o)}_D j \stackrel{\text{def}}{=} -(i, (a, o), j)^D_+; i \xrightarrow{(a,o)}_P j \stackrel{\text{def}}{=} +(i, (a, o), j)^P_+; i \xleftarrow{(a,o)}_P j \stackrel{\text{def}}{=} -(i, (a, o), j)^P_+; i \xleftarrow{-(a,o)}_P j \stackrel{\text{def}}{=} +(i, (a, o), j)^{-P}_-; i \xleftarrow{-(a,o)}_P j \stackrel{\text{def}}{=} -(i, (a, o), j)^{-P}_-; -(i, (a, o), j)^D_-; i \xrightarrow{-(a,o)}_P j \stackrel{\text{def}}{=} -(i, (a, o), j)^P_-; -(i, (a, o), j)^D_-$. For instance, $i \xrightarrow{(a,o)}_D j$ reads as: "a certificate supporting that $i$ grants $j$ the authority to delegate $(a, o)$ is issued." while $i \xrightarrow{-(a,o)}_P j$ reads as: "a certificate supporting a negative permission granted by $i$ to $j$ for $(a, o)$ is issued".

Next, we define the logic that we use for our delegation-revocation framework.

**Definition 7.** The logic $\mathcal{L}$ is defined by the following axiom schemes and inference rules.

$$ \begin{array}{l@{\quad}l@{\quad}l} \text{Taut} & \vdash & \phi \text{ for all propositional tautologies } \phi \text{ based on } \Phi \\ \text{K+} & \vdash & [+p](\phi \to \psi) \to ([+p]\phi \to [+p]\psi) \\ \text{K-} & \vdash & [-p](\phi \to \psi) \to ([-p]\phi \to [-p]\psi) \\ \text{Det+} & \vdash & \neg [+p]\phi \leftrightarrow [+p]\neg\phi \\ \text{Det-} & \vdash & \neg [-p]\phi \leftrightarrow [-p]\neg\phi \\ \text{Test} & \vdash & [\psi?]\phi \leftrightarrow (\psi \to \phi) \\ \text{Red1} & \vdash & [+p]p \\ \text{Red2} & \vdash & [+p]q \leftrightarrow q & \text{if } p \neq q \\ \text{Red3} & \vdash & [-p]\neg p \\ \text{Red4} & \vdash & [-p]q \leftrightarrow q & \text{if } p \neq q \\ \text{Comp} & \vdash & [\pi; \pi']\phi \leftrightarrow [\pi][\pi']\phi \\ \text{Choice} & \vdash & [\pi \cup \pi']\phi \leftrightarrow [\pi]\phi \wedge [\pi']\phi \\ \text{Nec} & \text{If } \vdash \phi \text{ then } \vdash [+p]\phi \text{ and } \vdash [-p]\phi \\ \text{MP} & \text{If } \vdash \phi \text{ and } \vdash \phi \to \psi \text{ then } \vdash \psi \end{array} $$

**Proposition 1.** For all formulae $\phi \in \mathcal{L}_D$, there is Red($\phi$) $\in$ Prop such that $\vdash \phi \leftrightarrow Red(\phi)$. The reduction of $\phi$ to Red($\phi$) is polynomial in the size of $\phi$
Proof (sketch). We prove it by successive inductions. We use in great extent the 'reduction' axioms K+, K-, Det+, Det-, Test, Red1 to Red4: they all 'push through' the connectives, except for the basic cases Test and Red1-Red4 where the dynamic modalities [+p] and [-p] disappear.

The above proposition is extremely important because it shows that every dynamic formula of the type $[\pi]\varphi$ can be reduced in an equivalent static formula in standard propositional logic. As a consequence of Proposition 1 we get the following theorem:

**Theorem 1.** *The semantics of $\mathcal{L}_D$ is sound and complete w.r.t. the logic L. The logic L is also decidable and NP-complete.*

**Definition 8 (Rooted Delegation Chain).** In the system represented by a valuation $\Theta$, there is a rooted delegation chain ending at the node $(j, (a, o))$ iff $\Theta \models CP_\emptyset(j, (a, o))$, where

$$CP_S(j, (a, o)) = \bigvee_{i \notin S} (((i, (a, o), j)_+^P \wedge \neg(i, (a, o), j)_-^P \wedge soa_{i,o}) \vee ((i, (a, o), j)_+^P \wedge \neg(i, (a, o), j)_-^P \wedge CP_{S \cup \{i,j\}}^{P,D}(i, (a, o)))$$

$$CP_S^{P,D}(j, (a, o)) = \bigvee_{i \in A \cup G} (((i, (a, o), j)_+^{P,D} \wedge \neg(i, (a, o), j)_-^{P,D} \wedge soa_{i,o}) \vee ((i, (a, o), j)_+^{P,D} \wedge \neg(i, (a, o), j)_-^{P,D} \wedge CP_{S \cup \{i,j\}}^{P,D}(i, (a, o)))$$

Intuitively, $CP_S(j, (a, o))$ reads as: "There is a rooted delegation chain (with no agent in $S$) such that $j$ is granted an access level permission (i.e., $alp = \top$) for $(a, o)$". Notice that our definition of $CP_S(j, (a, o))$ is well-founded because we have a finite number of agents, object and actions.

An authorization that has the connectivity property as reported in Definition 2 can be seen as a particular valuation which complies with the following definition.

**Definition 9 (Connectivity Property).** A system represented by a valuation $\Theta$ has the connectivity property iff for all access types $(a, o)$, $\Theta \models CP(a, o)$, where $CP(a, o) = \bigwedge_{i \in A \cup G} ((i, (a, o), j)_+^P \rightarrow CP_\emptyset(i, (a, o)))$

We now introduce two notions that are pivotal in formally defining the revocation schemes presented in Section 5.

**Definition 10 (Independency).** In a system represented by $\Theta$, given a subject $j$ with a permission $(alp, dlp)$ for access type $(a, o)$, $j$ is said to be independent of a subject $i$ iff $\Theta \models CP_{\{i\}}(j, (a, o))$

**Definition 11 (Reachability).** In a system represented by a valuation $\Theta$ we say that $j$ is reachable from $i$ via a delegation chain for access type $(a, o)$ iff $\Theta \models R_\emptyset(j, i, (a, o))$ where $R_S(j, i, (a, o)) = (i, (a, o), j)_+^P \vee \bigvee_{x \notin S} ((x, (a, o), j)_+^{P,D} \wedge R_{S \cup \{x\}}(x, i, (a, o)))^1$

<footnote n="1">¹ Notice that we do not check for the arc in the delegation chain to be active.</footnote>
**Automated Theorem Proving.** As shown in Proposition 1, the logic defined above is sound and complete w.r.t. propositional logic. In order to show how to use state of the art theorem provers to reason about delegation and revocation schemes, we developed a parser (written in SCHEME) which implements a set of complete reduction axioms and translates dynamic formulas, as reported in Definition 5, into (static) propositional logic. The parser translates a set of formulas written in our logical framework into first-order formulas compatible with SPASS [15] syntax. Due that our language is finite, SPASS automatically instantiates the translated formulas into propositional logic and then uses a SAT solver to check satisfiability<fnref n="2" />.

# 4 Delegation Schemes

As pointed out in [8], in the information security literature, delegation normally describes the act of distributing privileges to agents in distributed systems. In general, there are two possible kinds of delegation:

**Delegation as creation of new privilege:** the delegatee receives its own privilege which is independent of the delegator's privilege in the sense that if the delegator's privilege is revoked, then it does not necessarily mean that the delegatee's privilege is revoked. A special case is the *transfer* of a new privilege, which models the creation of a new privilege and a revocation of an old one;

**Delegation by proxy:** The delegatee does not receive its own privilege, but can exercise the privilege through the delegator, in the sense that the delegator speaks for or acts on behalf of the delegator.

On the first type of delegation, an agent *i* has a direct privilege to act on an object *o* if she is the SOA for it (i.e., *soa*<sub>*i*,*o*</sub>). To model delegation by proxy instead, we need to keep track of the delegation chains (represented through atoms like (*i*, (*a*, *o*), *j*)<sub>+</sub><sup>*P*,*D*</sup>) on which an agent depends for a given privilege.

We can accommodate the different types of delegation by exploiting the dynamic operators defined in the previous section. For instance, we can model delegation as creation of new privileges with the following programs: “Agent *i* assigns (if she has the power) a new privilege on object *o* to agent *j*”: (if *soa*<sub>*i*,*o*</sub> then +*soa*<sub>*j*,*o*</sub>); “Agent *i* transfers her privilege over *o* to agent *j*”: (if *soa*<sub>*i*,*o*</sub> then -*soa*<sub>*i*,*o*</sub> +*soa*<sub>*j*,*o*</sub>).

# 5 Revocation Schemes

In this section, we define the revocation operations that are informally described in [9]. The following schemes are sufficiently general to model a great deal of real-world distributed authorization architectures. The main contribution of this section is that for each revocation scheme *S* we define a program *π*<sub>*S*</sub> such that we read [*π*<sub>*S*</sub>]{*ϕ*} as: “after the execution of a revocation operation *S*, *ϕ* holds”.

<footnote n="2">² The parser is available at
http://www.di.unito.it/~genovese/tools/delegation2spass.zip</footnote>
Due to space constraints, we refer to $\pi_S[n-m]$ as the block instructions from line *n* to *m* of the program $\pi_S$.

As in [9], we divide revocation schemes into *positive* and *negative*, depending on the revocation action of deleting a certificate or of issuing a negative permission.

When *i* revokes a permission to *j*, we identify two types of agents: (i) those that are not independent from *i* and delegated the same permission to *j* (see Definition 10) and (ii) those that are reachable from *j* (see Definition 11) in the delegation chain. We classify a revocation operation as *weak/strong* and *local/global*, depending on how it influences agents of type (i) and (ii). A revocation operation is *weak* (resp. *strong*) if, in revoking a permission from *i* to *j*, none (resp. all) of the agents of type (i) are forced to revoke their delegation. Instead, we classify a revocation operation as *local* (resp. *strong*) if the algorithm influences none (resp. all) of the agents of type (ii).

An important property of *all* the programs implementing the revocation schemes is as follows

**Theorem 2 (Invariance under connectivity).** After the execution of any program implementing the revocation schemes, the resulting delegation chain satisfies the connectivity property.

## 5.1 Positive Revocation Schemes

**Weak Local Delete.** The *weak local delete* operation is the simplest form of revocation. After the application of the weak local delete operation on a permission (*alp*, *dlp*) for a given access type (*a*, *o*) granted by agent *i* to *j*, the following three post-conditions must be satisfied [9]: *i* no longer grants *j* the permission (*alp*, *dlp*); Permissions for (*a*, *o*) granted to *j* by users other than *i* are intact; Permissions for subjects other than *j* are intact. However, the grantors of permissions for users directly following *j* in the graph for (*a*, *o*) may have changed in order for the connectivity property to be satisfied;

In Figure 4 we show the resulting delegation chain after the execution of program *WLD*<sub>*i*,j*</sub>.

**Strong Local Delete.** The application of the *strong local delete* operation on a permission (*alp*, *dlp*) for access type (*a*, *o*) granted by agent *i* to agent *j* has to satisfy the following post-conditions: *i* no longer grants *j* the permission (*alp*, *dlp*); Permissions for access type (*a*, *o*) granted to *j* by every agent *z* other than *i* are intact if they are independent of *i*. Otherwise, they are restricted to satisfy the connectivity property for those paths from *z* that are independent of *i*; Positive (and negative) permissions for agents other than *j* are intact. However, the grantors of permissions for agents directly following *j* in the graph for (*a*, *o*) may have changed in order for the connectivity property to be satisfied. In Figure 6, we show the resulting delegation chain after the execution of program *SLD*<sub>*i*,j*</sub>.

**Weak global delete.** After the application of a weak global delete operation on a permission (*alp*, *dlp*) for an access type (*a*, *o*) granted by *i* to *j*, the following
<figure><img src="image_4.png" /><figcaption>Fig. 3. A Delegation Chain</figcaption></figure>

<figure><img src="image_5.png" /><figcaption>Fig. 4. Weak Local Delete</figcaption></figure>

<figure><img src="image_6.png" /><figcaption>Fig. 5. $WLD_{i,j}$ Program</figcaption></figure>

<figure><img src="image_7.png" /><figcaption>Fig. 6. Strong Local Delete</figcaption></figure>

<figure><img src="image_8.png" /><figcaption>Fig. 7. $SLD_{i,j}$ Program</figcaption></figure>

<figure><img src="image_9.png" /><figcaption>Fig. 8. Strong Global Delete</figcaption></figure>

<figure><img src="image_10.png" /><figcaption>Fig. 9. Weak Global Delete</figcaption></figure>

post-conditions must be satisfied: *i* no longer grants *j* the permission (*alp*, *dlp*) for access type (*a*, *o*); Permissions from the same access type (*alp*, *dlp*) granted to *j* by users other than *i* are intact; The permissions of all subjects that have been granted by *j* may change depending on whether other principals granted some permission for the same access type. A suitable situation to use the weak global delete operation is when *i* loses her trust in *j* but she still trusts that other guarantees to make their own judgements about him. Also, since *i* no longer trusts *j* with the permission previously given, in turn she no longer trusts any subject trusted by *j*, and so on. In Figure 9, we show the resulting delegation chain after the execution of program *WGD*<sub>*i*,j*</sub>.

**Strong global delete.** After the application of a strong global delete opera-
tion on a permission (*alp*, *dlp*) for an access type (*a*, *o*) granted by *i* to *j*, the
following post-conditions must be satisfied: *i* no longer grants *j* the permission
(*alp*, *dlp*); Positive permissions for the same access type (*a*, *o*) granted to *j* or any
descendant of *j* by every user *z* other than *i* are intact if they are independent
of *i*. Otherwise, they are adjusted (i.e., restricted) to satisfy the connectivity
1: $i \leftarrow^{(a,o)}_{P,D} j;$

2: **for all** $x \in \mathbb{A} \mathbb{G}$ **do**

3: if $((x, (a, o), j)_+^P \land \neg CP_{\{i\}}(x, (a, o)))$ then

4: $x \leftarrow^{(a,o)}_{P} j; x \leftarrow^{(a,o)}_{D} j;$

5: **end if**

6: if $R_{\emptyset}(x, j, (a, o))$ then

7: $WGD_{i,j}[2-10]$

8: **end if**

9: **end for**

<caption>Fig. 10. SGD<sub>i,j</sub> Program</caption>

1: $i \leftarrow^{(a,o)}_{P,D} j;$

2: **for all** $x \in \mathbb{A} \mathbb{G}$ **do**

3: if $R_{\emptyset}(x, j, (a, o))$ then

4: **for all** $y \in \mathbb{A} \mathbb{G}$ **do**

5: if $((y, (a, o), x)_+^P \land \neg CP_{\emptyset}(y, (a, o)))$ then

6: $y \leftarrow^{(a,o)}_{P} x; y \leftarrow^{(a,o)}_{D} x;$

7: **end if**

8: **end for**

9: **end if**

10: **end for**

<caption>Fig. 11. WGD<sub>i,j</sub> Program</caption>

property for those paths from *z* back to a SOA that is independent of *i*. Negative permissions of the same type are intact; The permissions of all subjects that have been granted either directly or transitively, by *j* may have been adjusted in order for the connectivity property to be satisfied. In Figure 8 we show the resulting delegation chain after the execution of program SGD<sub>i,j</sub>.

**Negative Revocation Schemes.** Negative revocation schemes differ from positive ones in that revocation is done not by deleting a positive certificate but by issuing a negative permission. The outcome of such schemes is exactly the same as the positive ones (permission is revoked) but a negative permission make it easier to go back to the previous state when negative permission is in turn revoked. For this reason we refer to [9] for an intuitive description of the schemes.<fnref n="3" />

# 6 An Epistemic Approach to Trust

The outcomes of executing a delegation or a revocation action, as presented in Sections 4 and 5, depend only on the authorization policy. The decision points of the programs presented so far are checked against the presence of information that is at system (institutional) level, like “is this agent a source of authority?” or “do we have evidence of a particular delegation certificate being held?”.

However, one of the features of MAS is that agents are autonomous and therefore they can act w.r.t. a subjective and internal perception of the environment. We next show that this subjective dimension can be naturally accommodated in our logic by explicitly representing *beliefs* of agents with a standard epistemic modal operator.

A crucial subjective dimension in authorization is the one of *trust* among agents. In particular, we are interested in policy requirements like: *“An agent *i* trusts agent *j* on (a, o) while *j* is not considered trustworthy by agent *k*”*.

The possibility of expressing subjective statements about trust enriches the model, which we describe above, in several respects:

<footnote n="3">³ For space constraints we refer to a companion technical report [4] for a formalization of negative schemes.</footnote>
**Verification:** For a verifier to grant a privilege it is not sufficient that the delegation chain is rooted according to Definition 4, but we require the chain to be such that all the agents are trusted by the verifier.

**Delegation:** An agent $i$ delegates a permission to agent $j$ not only if $i$ has the privilege to do so but also if $i$ trusts $j$.

**Revocation:** The introduction of trust can generalize the revocation schemes presented in Section 5. To see that, suppose that agent $i$ wants to revoke a permission from agent $j$, then depending on whether $i$ trusts $j$ or not: 1. The agent $i$ may want to remove the same permission from of all the other agents delegated by $j$ that are not trusted by $i$; 2. The agent $i$ may force all the other agents that gave the same privilege to $j$ to revoke it if $i$ does not trust them.

In what follows, we give a formal account of how to accommodate trust in all of the different respects that we reported above.

**Definition 12.** A trust model is a tuple $M = (W, R, V, w)$ where: $W$ is a set of possible worlds and $w \in W$; $R: \mathbb{A} \to 2^{W \times W}$ is a function assigning to each agent an accessibility relation on $W$; $V: \Phi \to 2^W$ is a function assigning to each propositional letter a set of possible worlds.

**Definition 13.** The language $\mathcal{L}_T$ is defined inductively as follows:

$$ \mathcal{L}: \phi ::= p \mid \neg\phi \mid \phi \land \phi \mid B_j\phi $$

where $p$ in $\Phi_T = \{t(i, (a, o)), | a \in A, o \in \mathbb{O}, i, j \in \mathbb{A}\}$.

The truth conditions of the relation $M, w \models \phi$ are defined inductively as usual (we omit $\neg$ and $\land$).

$$ M, w \models p \quad \text{iff} \quad w \in V(p) $$

$$ M, w \models B_j\phi \quad \text{iff} \quad \text{for all } v \in R_j(w), M, v \models \phi $$

Intuitively, $t(j, (a, o))$ reads as: "j is trusted on $(a, o)$" and $B_i(t(j, (a, o)))$ reads as: "i trusts j on $(a, o)$".

In the remainder of this section, we show how we can (independently) merge the trust model as described above, with the delegation model introduced in previous sections.

**Definition 14.** A trust-authorization model is a pair $\{(M, w), \Theta\}$ of an internal trust-model $(M, w)$ and a valuation $\Theta$ on $\Phi$.

**Definition 15.** We define inductively the language $\mathcal{L}$ as follows:

$$ \phi ::= p \mid \psi \mid \phi \land \phi \mid \neg\phi \mid [\pi]\phi \quad \pi ::= +p \mid -p \mid \phi? \mid \pi \cup \pi \mid \pi;\pi $$

where $p$ ranges over $\Phi$ and $\psi$ ranges over $\mathcal{L}_T$. Its truth conditions on the set of internal trust delegation models are defined as follows (we omit $\neg$ and $\land$):

$$ \{(M, w), \Theta\} \models p \quad \text{iff} \quad \Theta \models p $$

$$ \{(M, w), \Theta\} \models \psi \quad \text{iff} \quad M, w \models \psi $$

$$ \{(M, w), \Theta\} \models [\pi]\phi \quad \text{iff} \quad \{(M, w), \Theta^\pi\} \models \phi $$
**Theorem 3.** The semantics of the language $\mathcal{L}$ is completely axiomatized by the following axiom schemes and inference rules:

<table><tr><td>$L_D$</td><td>All axiom schemes and inference rules of $L_D$</td></tr><tr><td>$K_B$</td><td>$\vdash B_j(\phi \rightarrow \phi') \rightarrow (B_j\phi \rightarrow B_j\phi')$</td></tr><tr><td>$\text{Red5}$</td><td>$\vdash [\pi]\psi \leftrightarrow \psi$</td></tr><tr><td>$\text{Nec}$</td><td>If $\vdash \phi$ then $\vdash B_j\phi$</td></tr></table>

where $\psi$ ranges over $L_T$ and $j$ over $A\Gamma$.

More generally, as put forward by Abadi in [2], the use of an (epistemic) modal language permits to specify and reason about authorization in distributed environments by associating policies (i.e., formulae) to agents. For space constraints, we only give some examples of how to express such policies: If the computer science department supports that the university is trusted on $(a, o)$, then the department will trust any other agent trusted by the university on the same access type: $(B_{cs\_dep}t(uni, (a, o)) \rightarrow \bigwedge_{j \in A\Gamma} (B_{unit}(j, (a, o)) \rightarrow B_{cs\_dep}(j, (a, o)))$; If $j$ does not trust $i$ then he will not trust any other agent $k$ that delegates a permission to $j$: $(B_j(\neg t(i, (a, o))) \rightarrow \bigwedge_{k \in A\Gamma} ((k, (a, o), j)^P_+ \rightarrow B_j(\neg t(k, (a, o))))$; Whatever is supported by the university is supported by the computer science department too: $(B_{uni}\varphi \rightarrow B_{cs\_dep}\varphi)$, for any $\varphi^4$.

**Verification.** When a verifier $i$ has to check whether an agent $j$ is permitted to perform action $a$ on object $o$, she does not check for a rooted chain in which all the agents involved are trusted by $i$. Note that this is an inherently internal perspective which is independent from the external point of view of institutional notions, like authorization and permission. Faced with the same request, two verifiers can react differently depending on which agents they trust.

**Definition 16.** In a trust-authorization system represented by $\{(M, w), \Theta\}$ a verifier $i$ supports that $j$ has the privilege for $(a, o)$ iff $\{(M, w), \Theta\} \models \mathcal{D}T_{\emptyset}(i, j, (a, o))$, where

$$ \mathcal{D}T_S(i, j, (a, o)) = B_i t(j, (a, o)) \wedge \left( \bigvee_{w \notin S} \left( \left( \left( (w, (a, o), j)^P_+ \wedge \neg (w, (a, o), j)^P_- \wedge \text{soa}_{w,o} \right) \wedge B_i t(w, (a, o)) \wedge B_i t(j, (a, o)) \right) \vee \left( (w, (a, o), j)^P_+ \wedge \neg (w, (a, o), j)^P_- \wedge B_i t(w, (a, o)) \wedge B_i t(j, (a, o)) \right) \wedge \mathcal{D}T_{S \cup \{w,j\}}^{P,D}(i, w, (a, o)) \right) $$

$$ \mathcal{D}T_S^{P,D}(i, j, (a, o)) = B_i t(j, (a, o)) \wedge \left( \bigvee_{w \notin S} \left( \left( \left( (w, (a, o), j)^{P,D}_+ \wedge \neg (w, (a, o), j)^{P,D}_- \wedge \text{soa}_{w,o} \right) \wedge B_i t(w, (a, o)) \wedge B_i t(j, (a, o)) \right) \vee \left( (w, (a, o), j)^{P,D}_+ \wedge \neg (w, (a, o), j)^{P,D}_- \wedge B_i t(w, (a, o)) \wedge B_i t(j, (a, o)) \right) \wedge \mathcal{D}T_{S \cup \{w,j\}}^{P,D}(i, w, (a, o)) \right) $$

<footnote n="4">⁴ This formula has to be intended as an axiom schema, the corresponding canonical property is: $\forall x, y (x R_{cs\_dep} y \rightarrow x R_{uni} y)$.</footnote>
**Delegation.** Also delegation schemes can be naturally parameterized in terms of a subjective dimension of trust. For instance, w.r.t. delegation via transfer we can define the following programs: - `(if (soa<sub>i,o</sub> ∧ B<sub>i</sub>(t(j, o))) then +soa<sub>j,o</sub>) - (if (soa<sub>i,o</sub> ∧ B<sub>i</sub>(t(j, o))) then -soa<sub>i,o</sub> + soa<sub>j,o</sub>)`

**Revocation.** The schemes in Section 5 can be generalized with the revocation program in Figure 12 whose effects depend on the trust relationships between the revokee and the other agents in the delegation chain. The program generalizes the weak/strong and global/local dimensions of positive^5 revocation algorithms as presented in Section 5. For instance, in [9] WGD<sub>i,j</sub> is motivated as “... agent *i* loses trust in agent *j* but still trusts other agents to make their own judgement on *j*”. The block TBR[21 – 25] generalizes precisely this case, depending on whether *i* trusts other agents that are not independent from him, the relative permission may be revoked.

<figure><img src="image_11.png" /><figcaption>Fig. 12. Trust Based Revocation Program TBR<sub>i,j</sub></figcaption></figure>

## 7 Related Work

As we have stressed throughout our discussion, the delegation-revocation framework described by Hagström et al. is the basis for much of what we have described. The Hagström et al. work gives a semi-formal account of a range of delegation-revocation schemes, which we have formally represented in the logic language that we have introduced. We have also described an extension that allows for representing and reasoning about the beliefs.

We note that ABLP logic [3] and the RT^D model [12] allow for some restricted forms of delegation policies to be represented, but neither approach accommodates the rich range of delegation and revocation schemes that our approach admits. SPKI/SDSI [6] allows for delegation of privileges on objects via authorization certificates. However, the delegation policies that may be represented in the SPKI/SDSI approach are limited to a simple 1-step passing on of privileges

<footnote>^5 The algorithm can be adapted to work over negative permissions.</footnote>
on objects; revocation is limited to being typically effected via the expiration of short-lived certificates.

Hoek et al. [14] introduce a logic to reason how the abilities of agents and coalitions of agents are altered by transferring control from one agent to another. They adopt a dynamic propositional language in which atomic programs are of the form “agent *i* transfers the control of variable *p* to agent *j*”. Herzig et al. [10] generalize the logic introduced in [14] by relaxing the assumption that at most one agent can control a variable. Nevertheless, delegation is still modelled as transfer and it is not possible to keep track of the delegation chain. In [13], the main focus is on reasoning about the dynamics of how responsibility can be acquired, transferred and discharged; delegation is analyzed in relation to obligations. The approach of accounting for delegation in terms of obligation creation has some merit, but the proposal does not naturally accommodate the very rich delegation-revocation framework that we have described. The work by Demolombe [7] is related to ours in the sense that an epistemic logic is described for reasoning about trust. However, Demolombe does not consider trust in the context of the range of delegation-revocation schemes that we have.

## 8 Conclusions and Further Work

Recall that the principal research question that we have considered is how to define a formal framework to model and reason about management structures for distributing access privileges in multi-agent systems? On that, we have described a very general framework for modelling and reasoning about delegation and revocation schemes in the context of multi-agent authorization. In particular, we introduced a (dynamic) propositional logic (Section 3) for formulating policies, we demonstrated how a range of delegation schemes (Section 4) and revocation schemes (Section 5) can be treated formally within our logic language. Our logic enables the effects of delegation and revocation actions to be expressed in terms of the changes they make to a delegation graph. The effects of performing delegation and revocation actions are expressible in terms of the “programs” that we have defined. Evidence for the applicability of our formalization is apparent in our demonstration that the eight revocation schemes informally presented in [9] and the delegation types presented in [8] can be represented in our formal framework. We also showed (Section 6) how a notion of trust can be incorporated into an extended form of our delegation-revocation framework. To the best of our knowledge, ours is the first logical framework for distributed authorization that is able to represent the range of delegation-revocation schemes that are described in [9] and [8] and that accommodates an epistemic language for explicitly representing trust relations among agents.

In terms of future work, we plan to extend the epistemic model for trust that we have introduced (Section 6). In distributed authorization, it is often quite reasonable to model trust as a simple relation between predicates (see [16]). However, in MAS things can be more complex. For instance, we may need to admit a transitive model of trust [11] and express policies like “If *i* believes
that $j$ trusts $z$ then $i$ believes that $z$ is trustworthy" (e.g., $B_iB_jt(z, (a,o)) \to B_it(z, (a,o)))$. In such cases, it is useful to have a modal language to nest belief modalities. The development of such a language is a matter for future work. We also intend to investigate the possibility of further developing our delegation-revocation framework to incorporate a notion of time, e.g., for time-constrained delegation of privileges on objects.

**Acknowledgements.** Valerio Genovese is supported by the National Research Fund, Luxembourg. The authors thank the reviewers for their comments, which proved to be helpful for improving the clarity of the paper.

## References

1. FPDAM on Certificate Extensions. Final Proposed Draft Amendment on Certificate Extensions (V6), Collaborative ITU and ISO/IEC USA (April 1999)

2. Abadi, M.: Logic in access control. In: 18th IEEE Symposium on Logic in Computer Science (LICS), p. 228 (2003)

3. Abadi, M., Burrows, M., Lampson, B., Plotkin, G.: A calculus for access control in distributed systems. ACM Trans. Program. Lang. Syst. 15(4), 706-734 (1993)

4. Aucher, G., Barker, S., Boella, G., Genovese, V., van der Torre, L.: Dynamics in delegation and revocation schemes: a logical approach, technical report (2011), http://www.di.unito.it/~genovese/publications.html

5. Boella, G., van der Torre, L.W.N.: Delegation of power in normative multiagent systems. In: Goble, L., Meyer, J.-J.C. (eds.) DEON 2006. LNCS (LNAI), vol. 4048, pp. 36-52. Springer, Heidelberg (2006)

6. Clarke, D.E., Elien, J.-E., Ellison, C.M., Fredette, M., Morcos, A., Rivest, R.L.: Certificate chain discovery in SPKI/SDSI. J. Comp. Sec. 9(4), 285-322 (2001)

7. Demolombe, R.: Reasoning about trust: A formal logical framework. In: Jensen, C., Poslad, S., Dimitrakos, T. (eds.) iTrust 2004. LNCS, vol. 2995, pp. 291-303. Springer, Heidelberg (2004)

8. Firozabadi, B.S., Sergot, M.J., Bandmann, O.L.: Using authority certificates to create management structures. In: Christianson, B., Crispo, B., Malcolm, J.A., Roe, M. (eds.) Security Protocols 2001. LNCS, vol. 2467, pp. 134-145. Springer, Heidelberg (2002)

9. Hagström, A., Jajodia, S., Parisi-Presicce, F., Wijesekera, D.: Revocations-a classification. In: Procs. of CSFW-14, pp. 44-58 (2001)

10. Herzig, A., Troquard, N.: The dynamic logic of propositional control. In: Procs. of LIS@ESSLLI2010, pp. 107-121 (2010)

11. Kuntze, N., Schmidt, A.U.: Transitive trust in mobile scenarios. In: Müller, G. (ed.) ETRICS 2006. LNCS, vol. 3995, pp. 73-85. Springer, Heidelberg (2006)

12. Li, N., Mitchell, J., Winsborough, W.: Design of a role-based trust-management framework. In: IEEE Symp. on Sec. and Privacy, pp. 114-130 (2002)

13. Norman, T.J., Reed, C.: A logic of delegation. Artif. Intell. 174(1), 51-71 (2010)

14. van der Hoek, W., Walther, D., Wooldridge, M.: Reasoning about the transfer of control. J. Artif. Intell. Res. (JAIR) 37, 437-477 (2010)

15. Weidenbach, C., Dimova, D., Fietzke, A., Kumar, R., Suda, M., Wischnewski, P.: SPASS version 3.5. In: Schmidt, R.A. (ed.) CADE-22. LNCS, vol. 5663, pp. 140-145. Springer, Heidelberg (2009)

16. Wen, W., Mizoguchi, F.: An authorization-based trust model for multiagent systems. Applied Artif. Intell. 14(9), 909-925 (2000)