This document was made by OCR from a scan of the technical report. It has not been edited or proofread and is not meant for human consumption, but only for search engines. To see the scanned original, replace OCR.htm with Abstract.htm or Abstract.html in the URL that got you here.

A Calculus for Access Control in Distributed Systems
MARTuIN ABADI, MICHAEL BURROWS, and BUTLER LAMPSON Digital Equipment Corporation

and

GORDON PLOTKIN University of Edinburgh

We study some of the concepts, protocols, and algorithms for access control in distributed systems, from a logical perspective. We account for how a principal may come to believe that another principal is making a request, either on his own or on someone else's behalf. We also provide a logical language for access control lists and theories for deciding whether requests should be granted.

Categories and Subject Descriptors: C.2.4 [Computer-Communication Networks[: Distribut‑

ed Systems; D.4.6 [Operating Systems[: Security and Protectionaccess control; authentica­tion; verification; F.4.1 [Mathematical Logic and Formal Languages[: Mathematical Logic

General Terms: Security, Theory

Additional Key Words and Phrases: cryptography, cryptographic protocols, modal logic

1. THE PROBLEM

At least three ingredients are essential for security in computing systems:

(1)  A trusted computing base: the hardware and systems software should be ca~ pable of preserving the secrecy and integrity of data.

(2)  Authentication: it should be possible to determine who made a statement; for example, a user should be able to request that his files be deleted and to prove that the command is his, and not that of an intruder.

(3) Authorization, or access control: access control consists in deciding whether the agent that makes a statement is trusted on this statement; for example, a user may be trusted (hence obeyed) when he says that his files should be deleted.

These ingredients are fairly well understood in centralized systems.

This is an extended version of a paper presented at the Crypto '91 conference, August 1991. Part of the work of G. Plotkin was completed while at Digital Equipment Corporation, Systems Hesearch Center. Authors' address: M. Abadi, M. Burrows, and B. Lampson, Systems Hesearch Center, Digital Equipment Corporation, 130 Lytton Avenue, Palo Alto, CA 94301, IJSA; G. Plotkin, Department of Computer Science, IJniversity of Edinburgh, King's Building, Edinburgh EH93JZ, Scotland, IJK.

Distributed systems pose new problems. Scale becomes an issue, as ultimately one would want to envision a global distributed system with a global name space and global security. In addition, there are difficulties with communication, booting, loading, authentication, and authorization.

The computing base of a distributed system need not reside in a single location under a single management. This implies, in particular, that secure communica­tion cannot be taken for granted. Since it is hard to provide physically secure communication lines, some form of encryption is typically required. In what fol­lows, we assume that shared-key encryption (e.g., [8]) and public-key encryption (e.g., [9, 22]) are available where needed, but we use them frugally. In addition, there are problems of secure booting and loading of software. For instance, the operating system that a host runs may be obtained from a repository across the network; a mechanism is needed to guarantee that this software is an authentic release, free of viruses. This mechanism will inevitably rely on authentication and access control, as it is necessary to restrict who can make a release.

The nodes of a distributed system may act on their own behalf or on behalf of users. Users and nodes trust one another to different extents. Moreover, a user may be trusted only when he is working at certain nodes; he may have more rights at his office than at a remote public terminal. Therefore, both users and nodes need to be authenticated and their identities considered in access control decisions.

These issues give rise to a change in the nature of authentication and access control. The basic questions of authentication and access control are, always, "who is speaking?" and "who is trusted?" Typically the answer is the name of a simple principal (a user or a host). In a distributed environment these questions can receive a variety of answers; the notion of principal can be extended, to include:

Users and machines.

Channels, such as input devices and cryptographic channels. There is no formal reason to distinguish channels from users and machines, and it is advantageous not to. Cryptographic channels are identified by keys, and so we may write that the key K says s when s is asserted in a message decrypted with K.

_ Conjunctions of principals, of the form A A B. If A and B make the same statement s, then A A B says s as well. It often happens that A A B is trusted on s, but neither A nor B is trusted by himselfa "joint signature" is required.

_ Groups. It is often inconvenient to list explicitly all of the principals that are trusted in some respect, both because the list would be long and because it may change too often. Groups provide an indirection mechanism. The use of groups implies the need for a scheme for deciding whether a principal is a member of a group. This is not always straightforward, for example when the registrar for a group is remote; group membership certificates then become necessary.

_ Principals in roles, of the form A as R. The principal A may adopt the role R and act under the name A as R when he wants to diminish his powers, in particular as a protection against blunders. For example, a system manager may act in the role normal-user most of the time, and enable the manager role only on occasion. Similarly, a machine may adopt a weak role before running a piece of untrusted software or before delegating authority to an untrusted machine.

Principals on behalf of principals, of the form B for A. The principal A may delegate authority to B, and B can then act on behalf of A, using the identity

B for A. In the most common case, a user A delegates to a machine B. It is also possible for a machine to delegate to another machine and for delegations to be cascaded (iterated); then we encounter expressions such as C for (B for A).

This list raises formal questions of some practical importance. First, there is a need to determine which of the operations on principals should be viewed as primitive and which can be defined from the others. Then one may ask what laws the operations satisfy, as for example whether the principals B for (A A A') and (B for A) A (B for A') are in some sense equivalent; if two principals are equivalent then they should be granted the same requests.The resulting theory of principals should provide a reasonable degree of expressiveness and it should be amenable to a mathematical justification. It is also essential that the theory of principals be simple, because users need to specify permissions on resources and programs need to make access control decisions.

Further, a variety of protocols and algorithms must be designed and analyzed. Mechanisms are required for secure booting and loading, for joining groups and for proving membership, for adopting roles, for delegations of authority and for certifying such delegations, and for deciding whether a request should be granted.

This paper is a study of some of the concepts, protocols, and algorithms for security in distributed systems, with a focus on access control. Our treatment is fairly formal, as it is based on logics. Our main goal is to isolate some useful and mathematically tractable concepts. We account for how a principal may come to believe that another principal is making a request, either on his own or on someone else's behalf. We also provide a logical language for access control lists (ACLs) and theories for deciding whether requests should be granted. The logic enables us to explain a variety of protocols which can differ from one another in subtle but important ways.

On occasion, the formal analysis has suggested ideas for implementations, for example that some digital signatures could be saved. Moreover, logics make it possible to describe protocols and policies at a reasonable level of abstraction; we avoid the need for ad hoc arguments about particular implementations. This abstraction is important in the context of heterogeneous distributed environments, where several implementations of a design may coexist.

Our study is intended as a formal basis for parts of a security architecture, and for the Digital Distributed Systems Security Architecture (DSSA) in particular [11]; this architecture is currently under implementation. Other formal explanations of security are conceivable. We hope that this work clarifies some of the issues that these alternative accounts may address.

The next section is an overview. We describe the basic logical framework in Section 3. Sections 4 and 5 extend the treatment with roles and delegation. Then, in Section 6, we consider delegation schemes and algorithms for making access control decisions. Section 7 is a brief discussion of additional constructs. A short glossary appears at the end.

This paper does not cover many issues in the area; some of these issues are briefly mentioned in passing. We study only authorization mechanisms based on ACLs; we do not examine particular security policies nor matters connected with manda~ tory access control. Most implementation considerations are left to a companion paper [17] and to future work.

2. OVERVIEW

Composite principals play a central role in informal reasoning; for example, one often talks about "A and B" and "B on behalf of A." Therefore, we start by introducing formal notations for composite principals.

Some classical constructors for composite principals such as conjunction and disjunction come to mind first:

A A B: A and B as cosigners. A request from A A B is a request that both A and B make. (It is not implied that A and B make this request in concert.)

_ A V B is the dual notation; A V B represents the group of which A and B are the sole members.

Conjunction is important in our designs. Disjunction is often replaced with impli~ cation, in particular in dealing with groups. As discussed further below, "A is a member of the group C" can be written A = C. The group C can be named, as all other principals; it need not be given a definition beyond that implicit in formulas such as A = C. The membership of C can be deduced from what formulas of the form A = C have been asserted. We do not include disjunction among our basic primitives.

There are also new connectives, in particular:

A as R: the principal A in role R.

_ B A: the principal obtained when B speaks on behalf of A, not necessarily with a proof that A has delegated authority to B; by definition, B A says s if B says that A says s; we pronounce B A as "B quoting A."

B for A: the principal obtained when B speaks on behalf of A, with appropriate delegation certificates; B for A says s when A has delegated to B and B says that A says s, possibly after some checking that s is reasonable.

Of these, only is primitive in our approach; for and as are important but they are coded in terms of A and . Since for is stronger than ,we tend to use only for encoding for and as.

In order to define the rights of these composite principals, we develop an algebraic calculus. In this calculus, one can express equations such as

(B A C) for A = (B for A) A (C for A)

and then examine their consequences. Since A is the standard meet in a semilattice, we are dealing with an ordered algebra, and we can use a partial order = among principals:A = B stands for A = A A B and means that A is at least as powerful as B; we pronounce this "A implies B" or "A speaks for B."

A modal logic extends the algebra of principals. In this logic, A says s represents the informal statement that the principal A says s. Here s may function as an imperative ("the file should be deleted") or not ("C's public key is K"); imperative modalities are not explicit in the formalism.

The modal logic is a basis for various algorithms and protocols. For example, it is possible to explain logically how two principals A and B establish a public key Kd for B for A.

The logic also underlies a theory of ACLs. We write D for the usual logical implication connective and A controls s as an abbreviation for (A says s) D s,

which expresses trust in A on the truth of s; in the logic, an ACL for a formula s is a list of assertions of the form A controls s. If s represents a command to a server, then the ACL entry A controls s records the server's trust in A on s, and hence that A will be obeyed when he says s. When s is clear from context, the ACL for s may simply be presented as the list of principals trusted on s.

If A = B and B controls s, then A controls s as well. Therefore, ACLs may not mention all trusted principals explicitly; when B is listed, access should be granted to any A such that A = B. It is not always entirely trivial to decide whether a request should be granted, and our theory addresses this issue.

So far we have discussed ACLs for logical formulas, with the view that each formula corresponds to a separate assertion or command, and that it can have a separate ACL. In practice these ACLs could be combined, and there may be dependencies between them. For example, the ACLs that pertain to reading and writing a file might be related, and an ACL that controls modifications to another ACL might also control modifications to itself. We do not model these combinations and dependencies.

Secure channels, including those secured by cryptography, are represented as principals; we have no formal treatment of encryption functions. The logic does not consider the problems associated with timestamps and lifetimes, either. There­fore, we do not explain how principals come to believe that messages are recent and are not replays. In these respects the logic is more abstract than the logic of authentication proposed in [4]. The logic of authentication has as its goal describ­ing and debugging fairly low-level authentication protocols; in contrast, the logic discussed here is intended as an aid in developing and applying a general design.

3. THE BASIC LOGIC

This section describes the basic logical framework, with syntax, axioms, and se­mantics. The laws for as and for appear in Sections 4 and 5.

This section includes discussions of alternative approaches and of relevant math­ematical concepts; in particular, Section 3.4 presents some interesting axioms that we do not adopt. The essential material is in the main bodies of Sections 3.1 and 3.2.

3.1 A Calculus of Principals

We study a calculus of principals in a minimal syntax. As discussed later, this syntax suffices for expressing roles and the needed delegation connectives.

Principals form a semilattice under the operation of conjunction, and obey the usual semilattice axioms:

A is associative, commutative, and idempotent.

As usual, A = B can be taken as an abbreviation for A = A A B, or = can be defined in terms of = .

Implication is often used to represent group membership. This notion of mem­bership is slightly peculiar, and in particular it is transitive. We have found that transitivity is rather convenient for reasoning about hierarchical groups (groups with subgroups). For example, if A is a member of C and C a subgroup of F, we may write A = C and C = F, and then it follows that A = F, which expresses

that A is a member of F. Moreover, =has a fairly pleasant interaction with the other connectives of our calculus.

However, our treatment of groups is incomplete. It would be desirable to provide group subtraction and intersection operations. It would also be desirable to provide naming support for usual subgroups—so that there would be a standard operation that one applies to a group name C to obtain the group of principals with a certain position or job in C. Most probably these operations would appear only at the lowest level of logical formulas, and would not mix with other constructs. Therefore, we do not include these additional operations here; intersection and subtraction are discussed in Section 7.

The principals form a semigroup under M:

M is associative.

The final axiom is the multiplicativity of M in both of its arguments, which means: M distributes over A.

Multiplicativity implies monotonicity.

In short, the axioms given for principals are those of structures known as multi­plicative semilattice semigroups. (Often, these same axioms are taken for structures with some sort of union or disjunction, instead of A, and then the term additive is preferred to multiplicative.) A common example of a multiplicative semilattice semigroup is an algebra of binary relations over a set, with the operations of union and composition; algebras of binary relations are discussed further below.

The syntax for reasoning about principals is much the obvious one. We manipu­late equations between principal expressions, built from atoms A0, A1, A2, ~~~ with the symbols A and . We combine equations into boolean formulas and then adopt the usual axioms from propositional logic and the axioms for the algebraic struc­tures of choice (multiplicative semilattice semigroups, when not stated otherwise).

Section 6 discusses decidability issues for the calculus of principals.

On binary relations. As mentioned, an example of a multiplicative semilattice semigroup is an algebra of binary relations over a set, with the operations of union and composition. Now we discuss binary relations in some detail; we use them in the rest of the paper in semantic discussions. Those readers not interested in formal semantics may wish to skip all references to binary relations.

A multiplicative semilattice semigroup isomorphic to an algebra of binary rela­tions is called representable. In fact, the binary-relation example is common in a mathematical sense: every free multiplicative semilattice semigroup is representable (e.g., [3, 21]). This implies that the equational theory of multiplicative semilattice semigroups coincides with that of binary-relation algebras.

Equational theories do not suffice for reasoning about access rights, as for example group-membership assumptions are needed. Since the binary-relation model is a clear, appealing one, it is then natural to hope that every multiplicative semilattice semigroup is representable. Andréka has recently proved that this is not the case [3]. She has also studied the distributive multiplicative semilattice semigroups, which are defined by the additional distributivity axiom:

if B A C = A then there exist B' and C' such that B = B', C = C', and A= B' A C'.

Every distributive multiplicative semilattice semigroup is representable. The class of distributive multiplicative semilattice semigroups is a quasi-variety, but neither a variety nor finitely axiomatizable.

The algorithmic applications of the distributivity axiom are hard to see because of its existential nature. Therefore, in the remainder of the paper, we examine both the axiomatic and the model-theoretic possibilities. We tend to work axiomatically, with the theory of multiplicative semilattice semigroups, but rely on binary relations as a way of constructing models. Moreover, Section 6 describes an algorithm for the binary-relation model.

Other algebraic structures. It is possible, and somewhat natural, to consider op­erators on principals beyond A and . Here we consider a few operators with a mathematical origin. These operators are used very seldom elsewhere in this pa­per.

A unit 1 turns the semigroup into a monoid; 1 can be viewed as a perfectly honest principal. The unit introduces further distinctions between the axiomatic and the binary-relation viewpoints. For example, any relation smaller than the unit is idempotent, but this is not a theorem of multiplicative semilattice monoids. Thus, Andréka's remarkable representability result seems intriguingly fragile.

A disjunction operation turns the distributive semilattice into a distributive lat­tice. Andréka has proved that some multiplicative semigroup distributive lattices are not representable, but the free ones are representable.

If the lattice operations are generalized to the infinite case, then we have a quan­tale. In a quantale, the product fully distributes over one of the lattice operations; here it is A. In particular, this says that the empty meet 0 is absorbent for M. Quantales provide models for (intuitionistic) linear logics [13, 26]. In these logics the multiplicative conjunction connective (M, in our case) is often understood as a form of parallel composition [1, 7, 25]. In our setting, M is in fact a special form of parallel composition, though a noncommutative one.

Finally, it is possible to add the remaining operator of Kleene algebras [16], namely Kleene's iteration operator ( )e. We have not yet found a need for this.

3.2 A Logic of Principals and Their Statements

Here we develop a modal logic based on the calculus of principals. Syntax. The formulas are defined inductively, as follows:

_ a countable supply of primitive propositions Po, Pi, P2, ~~~ are formulas; if s and s' are formulas then so are -is and s A s';

if A and B are principal expressions then A = B is a formula;

_ if A is a principal expression and s is a formula then A says s is a formula.

We use the usual abbreviations for boolean connectives, such as D, and we also treat equality between principals (=) as an abbreviation. In addition, A controls s stands for (A says s) D s.

Axioms. The basic axioms are those for normal modal logics [14]: _ if s is an instance of a propositional-logic tautology then I- s;

if I- s and I- (s D s') then I- s';

F- A says (s D s') D (A says s D A says s'); if F- s then F- A says s, for every A.

The calculus of principals is included:

if s is a valid formula of the calculus of principals then F- s.

Other axioms connect the calculus of principals to the modal logic:

F- (A A B) says s (A says s) A (B says s);

F- (BMA) says s B says A says s;

F- (A = B) D ((A says s) D (B says s)).

The last axiom is equivalent to (A = B) D ((A says s) (B says s)), a substitu­tivity property.

Other relations between principals. Two relations similar to = deserve mention at this point.

Let us write A — B if, for every s, if A says s then B says s. Although — is weaker than = , it suffices in many of the situations where we currently use = , and hence we have contemplated adding it to the formalism. It may also be convenient to have second-order quantification over formulas and over principals. Second-order quantification enables us to define A — B as Vx.((A says x) D (B says x)). We do not adopt any of these additional constructs, for the sake of minimality. However, there is no difficulty in giving a semantics for them, and the proof rules needed in examples would be simple.

Another important relation between principals is defined by the formula

(A says false) D (B says false)

which we abbreviate A i— B. Intuitively, A i— B means that there is something that A can do (say false) that yields an arbitrarily strong statement by B (in fact, false). Thus, A i— B means that A is at least as powerful as B in practice. Clearly,

A = B implies A i— B. We do not have the converse, and actually the converse does not seem attractive, as for example B i— (B A) is valid but we would not want

B = (BMA) (since B may wish to say s without this being taken as a quotation of A). Nevertheless, the relation i— serves as a point of reference in axiomatizing the algebra of principals; a careful study of i— may be of some interest.

3.3 Semantics

The simplest semantics is a Kripke semantics, based on accessibility relations [14]. A structure M is a tuple (W, w0, I, J), where

W is a set (as usual, a set of possible worlds); w0 is a distinguished element of W;

_ I is an interpretation function that maps each proposition symbol to a subset of W (the set of worlds where the proposition symbol is true);

J      is an interpretation function that maps each principal symbol to a binary relation over W (the accessibility relation for the principal symbol).

The meaning function 7?. extends J, mapping a principal expression to a relation: 7?.(A?) = J(A?)

7?.(AAB) = 7?.(A)u7?.(B)

7?.(BMA) = 7?.(A)p7?.(B)

There is no difficulty in giving a semantics to other operations on principals such as infinite conjunctions, disjunctions, 0, and 1.

This simple relational model provides some justification for the axioms for prin~ cipals. If 7?.(A) = 7?.(B), then it is natural to have A = B, and this holds in the semantics. For example, 7?.(CM(BMA)) =7?.((CMB)MA) provides a justification for the associativity of M.

The meaning function £ maps each formula to its extension, that is, to the set of worlds where it is true:

£(p?) = I(p?)

£(-is) = Wb£(s)

£(s A s') = £(s) n£(s')

£(A says s) = {w M 7?.(A)(w) t £(s)}

£(A = B) = W if 7?.(B) t 7?.(A) and 0 otherwise

where 7?.(C)(w) = {w' M w7?.(C)w'}.

A formula s holds in M at a world w if w E £(s), and it holds in M if it holds at w0. In the latter case, we write M M= s, and say that M satisfies s. Moreover, s is valid if it holds in all models; we write this M= s. The axioms are sound, in the sense that if C s then M= s. Although useful for our application, the axioms are not complete. For example, the formula

(C says (A = B)) s ((A = B) V (C says false))

is valid but not provable. A more interesting source of incompleteness is that the algebras of principals that underly the semantics are obviously representable, while some multiplicative semilattice semigroups are not.(We do obtain a completeness result for a sublanguage in Section 6.)

More abstract models. A more abstract model may be desirable in order to avoid the requirement of representability. A first step would be to modify the notion of structure.A structure would become a tuple (W, wo, I, J, 7, 2), where 7 is a multiplicative semilattice semigroup (the principals) and 2 is a homomorphism from 7 to W2. The functions J and 7?. map principal expressions not to binary relations but to principalsthe corresponding binary relations being still available via 2. The corresponding semantics is

7?.(A?) = J(A?)

7?.(A A B) = 7?.(A) A 7?.(B)

7?.(BMA) = 7?.(A)p7?.(B)

~ ~ ~

£(A says s) = {w M 2(7?.(A))(w) t £(s)}

£(A = B) = W if 7?.(A) = 7?.(B) and 0 otherwise

Now it is consistent to have two different principals with the same associated binary relation.

This semantics is imbalanced, as it gives an abstract interpretation of principals but not of propositions. A more balanced, abstract semantics is possible in terms of structures similar to dynamic algebras (see Pratt [21] for a recent discussion of dynamic algebras). The operator says is directly analogous to the usual partial correctness operator [] of dynamic logic. It connects the two sorts of the algebras, that of principals and that of propositions.

3.4 On Idempotence

Idempotence postulates are attractive. For example, when A is a user there seems to be little advantage in distinguishing A A and A; in fact, this distinction seems quite artificial. Therefore, we may postulate that A A = A, for all A, and hence that A says A says s and A says s are equivalent.The idempotence of implies the idempotence of for (see Section 5 for details). Here we discuss the idempotence of and for; most of the remarks below are written in terms of , but exactly the same arguments apply to for.

The idempotence axiom is rather convenient for handling chains of principals. For instance, suppose that C represents a collection of nodes, that B and C repre­sent members of C, and that an ACL includes C A. Thanks to idempotence, the principal C B A obtains access. This means that multiple "hops" within a collec­tion of nodes does not reduce rights and should not reduce security. In particular, there is no need to postulate that C C = C, or to make sure that C C A appears in the ACL explicitly.

In addition, idempotence yields (AAB) = (B A), since (AAB) = (AAB) (AAB) and is monotonic, and similarly (A A B) = (B for A). These implications are rather pleasing, but not necessarily intuitive. They complicate the problem of making access control decisions. When (A A B) makes a request, one must check whether either (B A) or (A B) is trusted and grant access if either is trusted.

Finally, the semantics of Section 3.3 does not validate idempotence. We have been unable to find a sensible condition on binary relations that would force idempotence and would be preserved by both union and composition. A related symptom is that idempotence seems less compelling for complex principals than for simple ones.

For all these reasons we prefer to do without idempotence; to compensate we often rely on assumptions of the form C C = C, or write less elegant but more explicit ACLs.

We give a similar treatment to other possible axioms related to idempotence. Although it is often reasonable to assume formulas of the forms A controls (B = A) and A controls (t D A says s), this does not seem well founded in general. In particular, when A is a group, if A controls (B = A) for all B then any member of A can add members to A. Therefore, we choose to adopt neither A controls (B = A) nor A controls (t D A says s) as general axioms.

4. ROLES

The formal system we have presented so far includes no exotic connectives for roles or delegation. We discuss roles in this section and delegation in the next one. We start with an informal argument on the nature of roles and then describe their logic.

4.1 What Roles Are For

There are many situations in which a principal may wish to reduce his powers. We now describe a few, as motivation for our treatment of roles. They are all examples of the principle of "least privilege," according to which a principal should have only the privileges it needs to accomplish its task.

An administrator may want to have the powers of a normal user most of the time, and exercise his extraordinary powers only when needed. For example, users of the UNIXTM operating system with system-manager privileges typically run with their own, normal identity when that suffices, in order to avoid costly mistakes.

When a principal wishes to run a piece of untrusted software, he should be able to invoke it with reduced powers. It is important that the untrusted code should not be able to increase its powers beyond those granted initially. This is done in capability systems by restricting capabilities before passing them across address spaces and by passing as few capabilities as possible. In timesharing systems it is common for untrusted software to be tested with unprivileged user accounts that are used for no other purpose.

Analogously, when a principal wishes to delegate his powers to a machine less trustworthy than his own, he should be able to limit the rights passed.

These situations can be handled by the use of roles. A principal A may adopt a role R and act with the identity A as R when he wants to diminish his powers. Thus, A can decide to become A as R and then later perhaps A as R as R'. Role adoption is not reversible, in the sense that A as R cannot, on his own, recover the full powers of A. This prevents untrusted software that has been granted only limited rights from obtaining the full rights of the user that invoked it. But this does not mean that a user who has once relied on roles can never again exercise his full powers: a process acting on behalf of the user may hold on to the credentials for the user's original identity, which it could use when instructed.

As a practical matter it may be best for users to have only restricted powers when they first log in. In this way users could be forced to authenticate themselves a second time when they want extraordinary powers. Our general treatment of roles does not require or preclude such implementation decisions, which are however important in building a usable system.

4.2 Roles, Groups, and Resources

A principal A may reduce his powers in different ways by adopting different roles, say R or R'. Some ACLs may grant permissions to A as R but not to A as R', and vice versa. There is however no intrinsic difference between R and R'; that is, if the uses of their names were swapped consistently in all ACLs, the effects of adopting the two roles would be swapped. Moreover, R and R' may be used differently at two independent sites. Thus, the meaning of roles could be a matter of local policy at each site; this policy is reflected in the writing of ACLs.

In practice, we expect many roles to be related to groups. If C is a group, there may be a role Crole associated with it, so that a member of a group C can act in the role of member of C. A member A of several groups F, C, H, ~~~ can select the privileges associated with one, say C, by adopting the corresponding C role. Without this role, A matches any ACL with an entry F, but A as C role need not.

TMUNIX is a registered trademark of UNIX System Laboratories, Inc.

However, A as Crote matches any ACL with an entry C as C rote, and if we accept the rule that C = C as C rote, then A as Crote also matches any ACL with an entry C.

It is tempting to establish a formal identification between the group C and a corresponding role C role. In what follows, for simplicity, we do not identify roles and groups. In fact, this identification would interact somewhat strangely with our encoding of roles, given below. We do allow roles related to groups (such as C role), but this relation is not formal; a formal operator for relating groups and roles may be a useful extension of our calculus.

It is reasonable to expect that not all roles make sense for all principals and that a principal can act only in certain roles. For example, a principal may be allowed to act as C role only if he is a member of C. The simplest implementation of this idea relies on the judicious writing of ACLs. Roles can be adopted freely, and any A can speak in the role C role, with the identity A as C role. However, it may be that no ACL in the system grants access to A as C role, and for example the ACL C as C role does not if A is not a member of C. It is this implementation that we choose.

Not all roles that arise naturally are related to groups. For example, there may be a role such that adopting it makes it possible to access only a certain directory in the file system; the role corresponds naturally to a set of resources (files) rather than to any group of principals.

4.3 The Encoding

Given the view that roles can be freely adopted, it is quite satisfactory to define A as R to equal AMR.

In many cases this encoding makes some intuitive sense. For example, let A be a machine and R a (possibly untrusted) piece of software that A is running.The requests that A makes while running this software should not emanate from A with full powers; rather, they should emanate from A in some restricted role. The role can be named after the piece of software or after its class (e.g., untrusted-software). In any case, when A makes a request s in this role, A says that R says s.This is precisely AMR says s. Similarly, if A is a user and R is one of his positions, we can think of R as a program that A is following and apply the analysis above.

Furthermore, this presentation of roles offers formal advantages, thanks to the monotonicity, multiplicativity, and associativity of M.

_ Since M is monotonic in both arguments, if R is a more trusted role than R' and A a more trusted principal than A', then A as R is more trusted than A' as R'; that is, if R = R' and A = A' then (A as R) = (A' as R'). Thus, it is possible to exploit a hierarchy of roles.

_ The multiplicativity of M yields that A A B in a role R is identical to the con­junction A and B both in role R:

(AAB) asR=(AasR)A(BasR) Similarly, we can exploit the conjunction operation for roles: A as (RAR') = (A as R)A(A as R')

Both of these properties seem reasonable for roles as we conceive them informally, and they are quite handy.

Associativity yields a satisfactory interaction between roles and delegation. In particular, the user A in role R on a machine B is identical to the user A on a machine B, with the compound in role R:

BM(A as R) = (BMA) as R

and then the encoding of for, given in the next section, yields B for (A as R) = (B for A) as R Some special properties for roles can be expected:

We sometimes rely on the postulates that all roles are idempotent (RMR = R) and commute with one another (R'MR = RMR'). This yields

A as R as R = A as R

and

A as R as R' = A as R' as R (We make it explicit when these properties are assumed.)

_ We assume A = (A as R) for all A. With a unit, this could just be written 1 = R. In the binary-relation model, 1 = R means that roles are subsets of the identity relation; note that the previous idempotence and commutativity properties follow from this.

5. DELEGATION

Delegation is a fairly ill-defined term. Here we explain our approach to delegation; some example schemes for delegation illustrate the use of the logic. Then we give an encoding of delegation.

5.1 The Forms of Delegation

Delegation is a basic primitive for secure distributed computing. It is the ability of a principal A to give to another principal B the authority to act on A's behalf. When B requests a service from a third principal, B might present credentials that are supposed to demonstrate that B is making the request and that A has delegated to B.

Naturally, access control decisions need to take delegations into account. A range of designs is possible.

In the simplest case, A delegates all of his rights to B. Upon B's request, a service will be granted if it would have been granted to A, had A requested it directly.

An obvious improvement is for A to delegate only some of his rights, such as the right to read certain files from a file server. Capability systems (e.g., [10, 18, 23]) embody this approach in the case where delegation certificates can be transferred; the containment of capabilities is a serious concern. If delegation certificates are not transferable, cascaded delegations are hampered, as A may have to prepare adequate certificates for any expected collaborators to B in advance. In all cases the provider of the service never checks that B is a reasonable delegate for A.

These considerations suggest more sophisticated designs, where access control decisions may depend on the identities of both A and B. For example, the file server may not let a known malicious workstation read a user's files, even if the

user was unlucky enough to log onto the workstation. The file server may also let a trusted node read files over which the user has execute-only rights, in the belief that these files will not be shown to the user, but just executed; here the node acts as a protected subsystem and offers guarantees that its clients cannot provide by themselves. These examples illustrate a desirable flexibility. It exists in some form in a few designs and systems [15, 24], and it is a prominent component of DSSA [12]. We believe that it should and will become widespread.

Different mechanisms embody the concept of delegation in different settings. A user might rely on a smart-card for delegating to a workstation, while delegation across the address spaces of a machine might benefit from operating system support. (The use of smart-cards is discussed in [2], with a simplistic view of delegation.) Similarly, credentials can be signed with either shared-key cryptography or with public-key cryptography, or they might not be signed at all when a secure physical channel is available. Recognizing and treating all these variants as mere instances of delegation makes possible a uniform view of access control throughout an entire distributed system.

Delegation relies on authentication, which is often achieved through authentica­tion protocols (see for example [4, 5, 15, 19, 20]). In fact, some of the messages for delegation can be combined with those for authentication. However, in our study, it is often convenient to view delegation as independent.

Delegation without certificates. The framework outlined so far enables us to de­scribe and compare various schemes for delegation. In what follows, A delegates to B, who makes requests to C. For instance, A may be a user with a sufficiently powerful smart-card, B a workstation, and C a file server. For simplicity, the au­thority delegated from A to B is not limited to any particular class of requests and A does not adopt a special role before the delegation.

We assume that synchronized clocks are available and that appropriate times-tamps, lifetimes, sequence numbers, and message type fields are included and checked for all messages. We also assume that all principals can perform digi­tal signatures, for example with the RSA algorithm [22]. We denote by KA and KB the public keys for A and B, and by Kb'

$ and Kb'

B the matching secret keys.

The formula K says X represents the certificate X encrypted under Kb', which is commonly written {X}K-1.

A certification authority S provides certificates for the principals' public keys as needed. The necessary certificates are Ks says KA = A and Ks says KB B, where Ks is S's public key.

We consider three instances of delegation. In each case we are led to ask whether composite principals, such as BMA, appear on C's ACL. The simplest instance of delegation is delegation without certificates:

(1)   When B wishes to make a request r on A's behalf, B sends the signed request along with A's name, for example in the format KB says A says r.

(2)   When C receives the request r, he has evidence that B has said that A requests r, but not that A has delegated to B; then C consults the ACL for request r and determines whether the request should be granted under these circumstances.

The logic serves in describing the reasoning of the service provider, C, who makes the access control decision. Some assumptions are needed. First, C must believe

that Ks is S's public key:

Ks = S

and C obtains a certificate encrypted under the inverse of Ks:

Ks says (KB = B)

These two formulas yield

S says (KB = B)

We should assume that C trusts S for such statements:

S controls (KB = B)

and we immediately obtain that C has B's key:

KB = B

In addition, C sees a message under the inverse of KB, requesting r on behalf of A; in other words,

KB says A says r

Immediately, C obtains

B says A says r

that is,

(BMA) says r

Now C consults an ACL for r. If BMA appears in this ACL, that is, if BMA is trusted on r, then C believes raccess is granted.

Delegation with certificates. The protocol just described can hardly be considered satisfactory in general. It is preferable for A to issue a delegation certificate that proves the delegation to B:

(1)   After mutual authentication, A issues a certificate to B under A's key. This certificate states that A has delegated some authority to B.

(2)   When B wishes to request r on A's behalf, no further interaction with A is

needed: B can present A's certificate to C, along with KB says A says r.

(3) At this point C has evidence that B has requested r on behalf of A; now C

consults the ACL for r and determines whether the request should be granted.

For the time being, let us use the notation B serves A to mean that B is a delegate for A. (But serves need not be primitive; see Section 5.2.) Then the delegation certificate from A for B can be expressed:

KA says (B serves A)

and the usual checking of public-key certificates from S yields

A says (B serves A)

If C trusts A on this statement, C gets

((BMA) says r) A (B serves A)

In our theories, this implies

(B for A) says r

Again C can consult the ACL for r, and r will be granted if the list includes B for A. In particular, r will be granted if the list mentions B A, a weaker principal, but may be granted even otherwise.

This scheme is illustrated in more detail by an example in Section 6.

Delegation without delegate authentication. Another variant consists in omitting the authentication between B and C, leaving the responsibility of authenticating B solely to A:

(1)       After mutual authentication, A issues a certificate to B under A's key. The certificate includes a key Kd and B's name. The inverse key Kb'

G remains a

secret known at most to A and B.

(2)   When B wishes to request r on A's behalf, B can present A's certificate to C along with the request under the delegation key Kd.

(3) At this point C has evidence that B has requested r on behalf of A; now C consults the ACL for r and determines whether the request should be granted.

The most obvious novelty in this scheme is the introduction of a delegation key Kd. One of the reasons why this is significant is that the delegate can simply forget the secret key Kb'

G in order to give up the power of acting on behalf of the delegator; Section 6 discusses this use of delegation keys. For efficiency, however, requests would be made under neither KB nor Kd, but rather under a shared session key, for example a DES key [8]. The use of a session key is a significant optimization because of the efficiency of DES encryption, and does not compromise security.

The final items in these descriptions are deceptively identical. In the previous schemes, C obtains direct evidence that B is making the request. In this scheme, on the other hand, this evidence is provided only by A's certificate, which includes B's name. Accordingly, we may want C to make different access control decisions in the two cases. This distinction is necessary, for example in the case in which B is a protected subsystem. It is a distinction that a theory of delegation should allow, and hopefully clarify.

Let us denote by A on B the compound principal that is obtained by this del­egation scheme. It is sensible to assume that A = (A on B) for A to be believed when he claims that Kd speaks for A on B. This property suggests the definition (A on B) = (A V (B for A)); the definition yields suitable properties for on.

The use of on is problematic in a world where some ACLs may allow B for A but not A on B. The interaction between on and for is unfortunate. In particular, a request from A on B may fail where one from B for A would succeed; this is unpleasant, since for could have appeared in the request instead of on. It poses the problem of how to choose when to use on and when to use for. It seems best to use for throughout. This choice can be made affordable, and it also offers the advantage of simplicity—the design requires fewer credential formats and fewer laws. Therefore, we do not discuss on further.

5.2 The Encoding

The delegation of all powers can be defined convincingly: A delegates to B when A says that B speaks for A (that is, when A says (B = A) holds). The concept of

delegation that interests us here is subtler. When A delegates to B, the powers of B on behalf of A depend on the contents of the ACLs in the distributed system; A may be more reckless with delegations if these powers are small.In turn, the contents of the ACLs depend on how their writers understand the meaning of delegation. There is a circularity here. The meaning of delegation results from the combination of the contents of the ACLs in the system and of the behavior of delegators and delegates. Hence, we conclude that the meaning of delegation is a matter of policy or convention.

These remarks suggest an approach where the notion of delegation is primitive; we now sketch this approach, assuming for a moment that disjunction is available. The operator serves is taken as primitive and axiomatized. Some straightforward axioms come to mind, and in particular that B serves A is antimonotonic in B and that if B? serves A for all i, then (V? B?) serves A. Let E(A) be the weakest principal to which A has delegated and let EB (A) be the weakest principal stronger than B to which A has delegated. Then B for A can be defined to be EB (A) A, and this equals (B A E(A)) A. Axioms for delegation yield properties of for; for example, the axioms given yield that for is multiplicative in its second argument. We have not found a satisfactory way to obtain associativity.

We prefer not having delegation as a logical primitive; the following thought experiment inspires an alternative approach. Imagine that there is a distinguished principal D in the distributed system who operates as a delegation server. The function of D is to certify delegations. When A wants to delegate to B, it suffices for A to tell D that if B says that A says s, then D should back B. Thus, if B A says s then D A says s. Intuitively, D says that A says s when a delegate of A's makes this assertion. Thus, we can take (B A D) A as a formal encoding for B for A. Notice that there is a striking similarity between this encoding of for and the previous formulation.

It is not actually necessary for D to be implemented, just as typical roles do not correspond to real users and machines. When A wishes to delegate to B, A says that for all s, if B says that A says s then D says that A says s; formally, it suffices to have A says (B A = D A). The statement A controls (B A = D A) then represents that A can delegate to B. These two assertions together immediately yield (B A = D A), and when (B A) says s, we obtain (D A) says s, and then ((B A D) A) says s. In this formal derivation it is irrelevant whether D is a real server or not. (It is perhaps even better if D is not a real server, for then it cannot be attacked.)

Thus, we can take B for A to mean (B A D) A, where D is a distinguished fictional principal. Similarly, (B A = D A) can represent B serves A; hence, if B serves A then (B A = B for A). This expresses the intuition that for is "plus a delegation." The logical framework also allows the possibility of weaker delegation statements, where A delegates only some of these rights; we prefer the use of roles for limiting the power of delegations.

Our encoding has sensible formal consequences:

for is monotonic in both arguments.

for is multiplicative in both arguments, in fact. This follows from the multi~ plicativity of and the definition of for:

(BAB')for(AAA') =(BAB'AD) (AAA')

= ((BAD)A(B' AD))M(AAA')

= ((BAD)MA) A ((BAD)MA')

A ((B' A D)MA) A ((B' A D)MA')

= (B for A) A (B for A') A (B' for A) A (B' for A')

B for A is always defined, even if A has not delegated to B. In fact, we have (BMA) A (C for A) = ((B A C) for A)

and hence also

(BMA)A(C forA) = (B for A)

This somewhat surprising theorem is the consequence of two desirable, basic properties: the monotonicity of for and the antimonotonicity of delegation (which means that if A delegates to C, then it also delegates to the stronger principal B A C).

Additional properties of D yield further consequences:

_ If DMD = D then for possesses a weak associativity property: Cfor (B for A) = (CforB)forA

which follows from the associativity and the multiplicativity of M: C for (B for A)=(CAD)M((BAD)MA) = (CMBMA) A (CMDMA) A (DMBMA) A (DMDMA) = (CMBMA) A (CMDMA) A (DMBMA) A (DMA) = (CMBMA) A (DMBMA) A (DMA)

= ((CforB)MA) A (DMA)

= (CforB)forA

The other direction of the implication is not valid. The essential reason for this is that C for (B for A) implies CMDMA, while (C for B) for A does not. Intuitively, this is because C's part in (C for B) for A need not involve checking evidence that B is a delegate for A, or even that A exists.

If A = DMA then (A A (BMA)) = (B for A), because M is multiplicative:

AA(BMA) = (DMA)A(BMA) = ((BAD)MA) = BforA

This property means that when A makes a statement himself, there is no need to find a corresponding statement by the delegation server.

_ If A = DMA and A = AMA then A = A for A, that is, the idempotence of M implies the idempotence of for:

AforA = ((AAD)MA) = (AMA)A(DMA) = AA(DMA)

The additional properties for D are reasonable, and we adopt them. These prop­erties are reminiscent of those for roles. In the binary-relation model, for example, these properties of D and those for roles all amount to saying the same thing, that the associated binary relations are subsets of the identity.

6. PROTOCOLS AND ALGORITHMS

In this section we consider some mechanisms for delegation and for access control decisions. The last subsection presents an example.

6.1 Delegation

While delegation has a single semantics, substantially different implementations are recommended for users and for nodes.

Delegation from users to nodes. The schemes for delegation discussed in Section 5 do not seem adequate for users. Delegation from users to nodes poses special problems. One difficulty is that it is inconvenient for users to refresh delegation certificates. Refreshing a delegation certificate may require reintroducing a smart-card, for example. Therefore, it seems desirable that delegation certificates be relatively long-lived (valid for many hours).

Long-lived delegation certificates pose a security threat because a delegation cer­tificate may be valid long after the user has stopped using the node. An attacker may subvert the node over a relatively long time period and abuse the user's delega­tion. To prevent this from happening, it is best to introduce an auxiliary delegation key that the node can forget deliberately when the user leaves. The delegation cer­tificate remains valid, but becomes useless.

In more detail, the protocol goes as follows. First the user A delegates to the node B and to a public key Kd provided by the node:

A says ((Kd A B) serves A)

The node has the inverse of the public key and it can set up a channel Ch for

(KdAB) for A:

Kd says A says (Ch = (Kd A B) for A)

and

B says Asays (Ch = (Kd AB)forA)

Hence

((Kd A B) for A) says (Ch = (Kd A B) for A) follows logically. When this statement is believed, it yields

Ch=(KdAB)forA

and then monotonicity leads to the desired result:

Ch =B for A

Hereafter B can make requests for A through the channel Ch. In practice, the channel may be obtained by multiplexing a longer-term secure channel from B; this longer-term channel may well be a DES channel.

The delegation from Kd to the channel has a relatively short lifetime and needs to be renewed frequently. When the node forgets Kd deliberately, it loses the ability to refresh the certificate for the channel Ch.

Delegation from nodes to nodes. For nodes the schemes of Section 5 are conve­nient enough. The one corresponding to the for operator is simple, reasonably secure, and can be made efficient enough for implementation.

The same ideas work for cascaded delegations. Suppose that user A has delegated to node B and that B can operate with the identity B for A. If a further delegation is needed to a node C, the precise delegation statement is

(BMA) says (C serves (B for A)) Since A has delegated to B, it follows logically that:

(B for A) says (C serves (B for A)) This statement is believed, and yields

C serves (B for A)

Now C can make a request r on behalf of B for A:

C says (B for A) says r and then the delegation from A yields

(C for (BforA)) says r

6.2 Access Control Decisions

Unfortunately, the set of valid formulas of the calculus of principals is not recursive for any useful definition of validity, but it is recursively enumerable. Undecidability can be proved by a reduction from the word problem for Thue systems, for example. On the other hand, the formulas that arise in access control are not arbitrary; the next two parts discuss decidable access control problems.

A general access control problem. The problem of making access control decisions is computationally complex. It is important therefore to understand the precise form of its instances. The parts of an instance are:

An expression P in the calculus of principals represents the principal that is making the request. In particular, all appropriate delegations are taken into account in constructing this expression. The various relevant certificates are presented for checking.

A statement s represents what is being requested or asserted; the statement is presented explicitly by the requester, and the service provider does not need to derive it logically from other statements. The precise nature of s is ignoredit is treated as an uninterpreted proposition symbol.

Assumptions state implications among principals; these typically represent as­sumptions about group memberships. They have the form PL = GL, where P. is an arbitrary expression in the calculus of principals and G an atom. Note that this syntax is liberal enough to write GMG = G for every appropriate G of interest, obtaining some of the benefit of the idempotence axiom.

Certain atomic symbols R0, ..., R , ... are known to denote roles. This may be obvious from their names.

An ACL is a list of expressions E0, ..., E , ... in the calculus of principals; these represent the principals that are trusted on s.

The basic problem of access control is deciding whether A (P = G ), derived from the assumptions, and A (E controls s), derived from the ACL, imply P controls s, given the special properties of roles and of the delegation server D. We simplify the problem, and ask instead whetherA (P = G ) implies P = E2 for some j.

In this simplification, ACL entries are considered one by one, and their possible interactions are ignored. ACL entries written by two different users cannot lead to results that neither of them could foresee. The simplification of the problem is both convenient and sound, but in some cases it is incomplete.For example, when the model is a monoid of binary relations, if R controls s and R' controls s and both R and R' are roles, then (R' R) controls s; on the other hand, the requester (R' R) is denied access when the entries R and R' are considered separately. We do not know under what general conditions one has completeness; however, we prove a completeness result in the next subsection.

Fixing a j and introducing an auxiliary atom A, the access control question becomes whether A (P = G ) and E2 = A imply P = A. After some renamings, this is: given expressions P, Q0, ..., Q , ..., and atoms A, B0, ..., B , ..., does A (Q = B ) imply P = A?

This problem has a few interesting, tractable cases. If we ignore roles and D for the time being and allow only the operator A, we have the problem of deriving a Horn clause from other Horn clauses. If instead the only operator is ,we have the problem of deciding membership of a word in a context-free language. The word corresponds to P, and the grammar for the context-free language comes from the implications (Q = B ); the atom A serves as initial symbol.

It is the combination of A and that makes the problem hard. More precisely, let us ignore roles and D, allow both and A, and assume the theory of multiplicative semilattice semigroups. Context-free grammars can still be encoded, but in addition the "universal branching" due to A alternates with the "existential branching" that comes from choosing between rules of the encoded grammars. Using these ideas, we have sketched a proof that the problem of making access control decisions is equivalent to the acceptance problem for alternating pushdown automata [6].

It follows that the fairly general access control problem that we posed requires exponential time. We believe that the inclusion of various reasonable properties for roles and for D does not worsen this complexity. (We have considered some of the cases.) Although all of the expressions involved seem likely to be small, we fear that our algorithms would not run fast enough in practice. Further restrictions are wanted.

A more tractable problem. A second version of the access control problem is based on some further simplifications:

The for operator takes a more prominent role. Since it is expected to be common, one would want an algorithm that does not treat it by expanding it in terms of A and , with an exponential blow-up.

In effect, for is treated as an associative operator. More precisely, we assume that all ACLs have the weakest parenthesization possible. This enables us to ignore the parenthesization of the requester.

_ The operator occurs only in the encoding of for and as, and D occurs only in the encoding of for.

_ Roles are differentiated from other principals (called proper principals) and occur in special positions. The set of atomic symbols for proper principals is 7'; the set of atomic symbols for roles is Q.

_ Assumptions (group memberships) are restricted to the form atom = atom, where both atoms are either in 3 or in Q. In particular, this forbids the assump­tions of the form C C = C, which would give us some benefits of idempotence where appropriate.

_ It is therefore necessary to include a construct for writing, in an ACL, that any positive number of iterations of a principal are allowed. We introduce a metalogical construct ()+ for this purpose; for example F for C+ is a shorthand for the list F for C, (F for C) for C,....

An ACL is a list of ACL entries. In turn, an ACL entry is a conjunction of ACL entries free of A, called for-lists. A for-list is a list connected by for's, that is, it has the form Po for ~~~ for Pm, where each P, is a principal in roles. A principal in roles is of the form Q as R1 as ~~~ Ri,,, where Q is a proper principal and each R2 is a role.

This definition is summarized by a grammar:

A CL =list of Entry

Requester =Entry

Entry =conjunction of for-list

for-list =Principal-in-Roles for-list for Principal-in-Roles Principal-in-Roles =Proper-Principal Principal-in-Roles as Role Membership =Proper-Principal = Proper-Principal Role = Role

The syntactic conditions can be loosened, as this normal form for ACL entries can be obtained by two syntactic transformations justified by the laws of the logic. Conjunctions can be pushed outwards, since both as and for distribute over A; this normalization is the only source of exponential behavior, and it can be expected to be unimportant in the common examples where conjunctions are rare. Roles can be pushed inwards, into the delegator argument of for's; this step is efficient.

With these syntactic restrictions, a more efficient access control algorithm is possible:

The request is granted if the requester implies one of the ACL entries.

_ Each ACL entry is a conjunction of for-lists, and so is the requester. For the requester to imply an ACL entry, it must be that for each conjunct of the ACL entry there exists some conjunct of the requester that implies it.

_ A for-list implies another if they are of the same length, and each principal in roles of the requester implies the corresponding one of the entry.

A principal in roles Q as R1 as ~~~ as R, implies another Q' as R'1 as ~~~ as R' Q~ if Q implies Q' and for each R2 there exists R'N such that R2 implies R' N.

An atomic symbol P implies another atomic symbol P'if there is a chain of assumptions P = Po = ... =PQ = P'.

This algorithm is simple to describe to users, and it is also simple to implement. The adequate speed of a prototype implementation suggests that the algorithm might well be practical. The metalogical construct ( )+ does not introduce any major algorithmic difficulty. Its treatment is well understood, as it is standard in the context of regular languages.

The algorithm is sound for the binary-relation model, where we take all roles to be subsets of the identity. The algorithm is also complete for the binary-relation model. Note in particular that the algorithm treats all roles as idempotent, and they all commute with one another.

THEOREM (SOUNDNESS AND COMPLETENESS).Let Eo,. .. ,E ,... be an ACL,

P  a requester, and 9 (B = B' ) a conjunction of assumptions. The algorithm grants the request if and only if

A (B =B' )A A (E controls p) D (P controls p)

 

is valid for all p over binary-relation models.

PROOF. The soundness proof is simple. The algorithm works by attempting to prove that P = E for some i from the assumptions, and does so soundly. Moreover, the truth of P =E implies that if 9 (E controls p) holds, then so does

P  controls p.

The completeness proof is clearest when there are no assumptions, and hence we first treat that case. We suppose that the algorithm does not grant a request and obtain that there is a binary-relation model where 9 (E controls p) holds but

P  controls p does not, for some p. This requires that p be false, that P says p be true, and that E says p be false for all i.

It suffices to find some binary-relation model where -i(woR(P)wo) and where R(E )(wo) ç~ 5(P)(wo) for all i. Then we can define an interpretation that makes the proposition symbol p true at all w such that woR(P)w, and false at all other worlds.

The binary relation model is constructed from strings in a fairly usual way. Let T = 7 x 2' and let S be the set of strings over T. The set S is our set of possible worlds; the empty string is wo.

If A E Q, then its interpretation J(A ) is defined by

I(A ) = {(x. (A2,B), x . (A2,B)) A2 E 7, A E B ç Q}

Hence roles are interpreted by subsets of the identity, as required. If A E 7 then, instead:

J(A ) = {(x, x. (A , B)) B ç Q}

with the exception of the special constant D:

J(D) = 0

Thus, in this model, for and are equivalent; this is merely a convenience.

The interpretation of a principal expression Q relates the empty string to all strings

(PQ, {R1 Q, . . . , RPQ

Q }) . . . . . (P1,{R1 1,...,RP1

1 })

such that

(P1 as R11 as ... as RP1

1 ) for ... for (P Q as R1 Q as ... as RPQ

Q )

is one of the for-lists in Q, and also to all strings obtained from the strings

(PQ, {R1 Q, . . . , RPQ

Q }) c . . . c (P1,{R1 1,...,RP1

1 })

by enlarging the role sets. Note that in any case the empty string is never related to itself, as the for-lists are not empty, so in particular -i(woR(P)wo) holds.

Suppose that, for some i, the algorithm does not manage to prove that P = E . Then there must be some conjunct in E that is not implied (according to the algorithm) by any of the conjuncts in P. Suppose this conjunct is

(P1 as R11 as ... as RP1

1 ) for ... for (P Q as R1 Q as ... as RPQ

Q )

This implies that the empty string is related to

(PQ, {R1 Q, . . . , RPQ

Q }) c . . . c (P1,{R1 1,...,RP1

1 })

by the interpretation of E . On the other hand, there is no conjunct in P that establishes this relation. Thus, the model satisfies R(E )(wo) t~ 5(P)(wo).

This proves our initial completeness claim. Next we deal with assumptions. Without loss of generality, we can take the assumptions to be transitive, that is, if both A = A1 and A1 = A are assumed, then so is A = Ak.

Let us replace each symbol A in P with the conjunction of all symbols A1 such that A = A1 is among the assumptions. Let P' be the expression obtained after this replacement and after normalization (after A's are moved outwards). The algorithm grants the request to P if and only if it grants the request to P'—the additional conjuncts in P' do not add strength in presence of the assumptions. Moreover, the algorithm grants the request to P' using the assumptions if and only if it grants the request without the assumptionsas the additional conjuncts in P' can be exploited to dispense with the assumptions. In short, P obtains access with the assumptions if and only if P' obtains access without them.

Now it suffices to show that a similar equivalence holds at the semantic level. Given a model M' where A (E controls p) does not imply P' controls p, we construct a model M where all of the assumptions hold and A (E controls p) does not imply P controls p. The models M and M' differ only in their interpretation functions, 3M and JM':

U

JM(A ) = {JM '(A1) M A = A1 is among the assumptions}

Note that all roles are still interpreted as roles.

The meaning of P'in M' is equal to the meaning of P'in M, and it is equal to the meaning of P in M. Moreover, all of the assumptions hold in M. The

meaning of the E 's in M is larger than in M', thus making weaker the assumption

A

(E controls p). This shows that M has the desired properties. ( 6.3 An Example

The most typical, complete example is that of a user logging into a workstation, and the workstation making requests on a server.

The user A authenticates and delegates in some role RA to a workstation B in role RB. The user may rely on a smart-card, and use the scheme for user delegation outlined in Section 6.1. The delegation certificate is

KA says RA says ((Kd A (B as RB)) serves (A as RA))

The workstation sets up a secure channel to a server. Logically, this requires two statements:

Kd says (A as RA) says (Ch = ((B as RB) for (A as RA))) under the delegation key, and

KB says RB says (A as RA) says (Ch = ((B as RB) for (A as RA)))

(For simplicity, the workstation acts in the role RB, but any stronger role would do just as well.)

The server needs to check that KA is the user's key and that KB is the work­station's key, that is, KA = A and KB = B. Typically this requires looking at certificates from a certification authority; it is possible that a chain of certi­fication authorities needs to be involved, as there may be no single universally trusted certification authority.

_ With these properties of the keys, it follows from the delegation certificate that

(A as RA) says ((Kd A (B as RB)) serves (A as RA))

and this statement is believed. The channel set-up certificates yield

((Kd A (B as RB))M(A as RA)) says

(Ch = ((B as RB) for (A as RA)))

and this leads to

((B as RB) for (A as RA)) says (Ch = ((B as RB) for (A as RA))) and then

Ch = ((B as RB) for (A as RA))

as (B as RB) for (A as RA) is trusted in this matter.

The user may indicate to the workstation that he wishes to reduce his privileges and adopt a further role R' A, in order to make a request r; or the workstation may do this on behalf of the user, on its own initiative:

(Ch as R' A) says r

The requester here is ((B as RB) for (A as RA)) as R' A, which is equivalent to

(B as RB) for (A as RA as R' A).

_ The ACL at the server may contain (C' as RB) for (C as R'' A). The server may have, or the workstation may present, certificates that prove that A = C,

RA = R'' A, R'A = R'' A, and B = C'.

_ Actually, the group membership certificates come signed with someone's public key. In each case it must be possible to resolve this public key into a name and then to discover that the name is that of someone who is trusted to certify membership in the group.

At this point the algorithm for access control can easily determine that access should be granted.

7. EXTENSIONS

Our main goal in this paper has been to isolate some useful and mathematically tractable concepts. We have only touched on many practical and theoretical mat­ters that deserve more detailed treatments. In addition, the basic logic could be extended in many interesting ways. To conclude, we briefly describe three exten­sions.

7.1 Intersection

An intersection operation fl permits the construction of groups from groups. It is not a logical connective in the sense that conjunction is, as it can only be applied to atomic symbols (so for example (A2 AL) fl A is not a legal expression).

Conjunction is strictly weaker than intersection: (A fl B) = (A A B) is valid but (A A B) = (A fl B) is not. A weaker property than (A A B) = (A fl B) holds: if C = A and C = B then C = (A fl B) provided C is in some sense atomic. Atomicity is not a logically defined notion; intuitively, only simple principals such as users and machines are atomic, while the conjunction of two such principals is not.

An application of intersection concerns restricting access to only a particular member of a group. The ACL entry A A C grants access to A if A is a member of C, but it also grants access to A A B if B is a member of C. In contrast, A fl C grants access to A if A is a member of C, but not necessarily to A A B even if B is a member of C.

7.2 Subtraction

Another important operation on groups is subtraction (-). It provides the ability to specify that certain named individuals or subgroups within a supergroup should be denied access, even when such access is granted to the supergroup. Subtraction is the only negative construct for ACLs in this paper.

Subtraction has a simple semantics in centralized systems, where it is easy to decide group membership. There, subtraction is simply set subtraction. The situ­ation is different in distributed systems, because in general it is possible to prove only membership in groups, but not nonmembership.

Consider, for example, a situation in which C'' - C appears in an ACL, with A = C, A = C', C = C'', and C' = C''. Should access be granted to A? The facts A = C and C = C'' may not be available to the procedure making the access control decision. Moreover, we cannot expect A to provide proofs for themas this is probably of no benefit to A. Therefore, the access control decision cannot depend on A = C and C = C'', and hence access should be granted in this case. In short, C'' - C means "all members of C'', except for those that are members of C'' only via C."

This definition of subtraction is somewhat operational. Nevertheless, it is the best possible, and it has even been suggested that it provides an intuitive semantics for subtraction.

Even in distributed systems, there are groups for which it is possible to prove both membership and nonmembership. Typically, these groups are those managed by fairly centralized subsystems of the distributed system. The traditional set subtraction operation can be made available for these groups.

7.3 Variables

So far, we have provided for only the most basic form of joint signatures, and a more general form would be useful. One would like to be able to express that access should be granted to any two different members of a given group when they sign jointly, without listing all allowed combinations. Moreover, one may require that the two signers bear a certain relation to one another.

The introduction of variables provides the desired expressiveness, and more. Vari~ ables can be included in ACLs. When a requester matches an ACL entry, we identify the parts of the requester that match against each of the variables in the ACL en~ try, and bind the variables to these parts.It is then possible to evaluate arbitrary predicates on these variables.

For example, the entry yMx is equivalent to CMF when we require that x = F and y = C. Other requirements on x and y can be added, for instance that x and y be different, or that y be a machine owned by x. (Intuitively, it becomes possible to generalize from unary relations to arbitrary ones.) The entry has an implicit universal quantifier: it means that, for all x and y, if x and y satisfy all requirements then (yMx) controls s, where s is the statement under consideration. Trivially, B A matches y x; access is granted if the requirements hold when x is replaced with A and y with B.

The manipulation of variables can be added to the algorithm of Section 6.2. There are some complications, however. In particular, some metalogical construct to handle lists of principal expressions is needed if variables are to be legal in the scope of the iteration construct ( )+.

The use of variables may not be the only or best way to provide the desired expressiveness. It seems to deserve further study.

GLOSSARY

A says s: A makes the statement s.

A controls s: A is trusted on s: if A says s then s. This is the meaning of A appearing in the ACL for s.

A = B: A is a stronger principal than B. (For example, when B represents a group, A may represent a member or a subgroup of B.) If A says s then B says s, and if B controls s then A controls s.

A = B: A = B and B = A.

B serves A: B is a delegate for A. This can be defined as (BMA = B for A).

A A B: A and B in conjunction; (AAB) says s if and only if A says s and B says s. BMA: B quoting A; (BMA) says s if and only if B says A says s.

B for A: B on behalf of A. This can be defined in terms of a fictional delegation server D, as (BAD) A. If B says A says s and B serves A then (B for A) says s. A as R: A in role R. This can be encoded as AMR.

A fl B: the intersection of A and B, if A and B are atomic symbols. A b B: A minus B, if A and B are atomic symbols.

ACKNOWLEDGMENTS

Morrie Gasser, Andy Goldstein, and Charlie Kaufman were at the origin of many of the ideas discussed here. Tim Mann, Garret Swart, and Ted Wobber partici~ pated in fruitful discussions about implementations and examples. Bill Shockley convinced us of the practical importance of the extension described in Section 7.3. Greg Nelson and Vaughan Pratt helped in understanding the algebra of principals. Roger Maddux told us about Andréka's work. Luca Cardelli and Cynthia Hibbard provided editorial suggestions.

REFERENCES

1. ABADI, M., AND PLOTKIN, G. A logical view of composition. Theor. Comput. Sci. 11 , 1

(June 1993), 3-30.

2. ABADI, M. ,BURROwS, M., KAUFMAN, C., AND LAMPSON, B. Authentication and delega~ tion with smart-cards. In Theoretical Aspects of Computer Software, Springer-Verlag Lecture Notes in Computer Science 526, Sept. 1991, 326345.

3.     ANDR EKA, H. Representations of distributive lattice~ordered semigroups with binary rela~ u

tions. Manuscript, Aug. 1989.

4.    BURROWS, M., ABADI, M., AND NEEDHAM, B..M. A logic of authentication. Proceedings of the Royal Society of London A 26 (1989), 233271.

5. CCITT. CCITT Blue Book, Recommendation X.509 and ISO 9594~8: The directory~ authentication framework. Geneva, March 1988.

6. CHANDRA, A., KOzEN, D., AND STOCKMEYER, L. Alternation. .1. ACM 28, 1 (Jan. 1981),

114133.

7. DAM, M. Relevance logic and concurrent computation. In Proceedings of the Third IEEE Symposium on Logic in Computer Science (July 1988), 178185.

8. NATIONAL BUREAU OF STANDARDS. Data Encryption Standard. Fed. Inform. Processing Standards Pub. 46. Washington D.C., Jan. 1977.

9.    DIFFIE, W., AND HELLMAN, M. New directions in cryptography. IEEE Trans. Inf. Theor. IT-22, 6 (Nov. 1976), 644654.

10.  FABRY, B.. Capability~based addressing. Commun. ACM 17, 7 (July 1974), 403412.

11.  GASSER, M., GOLDSTEIN, A., KAUFMAN, C., AND LAMPSON, B. The Digital Distributed Sys~ tem Security Architecture. In Proceedings of the 1989 National Computer Security Conference

(Oct. 1989), 305319.

12.  GASSER, M., AND MCDERMOTT, E. An architecture for practical delegation in a distributed system. In Proceedings of the 1990 IEEE Symposium on Security and Privacy (May 1990),

20-30.

13.  GIRARD, J.-Y. Linear logic. Theor. Comput. Sci. 50 (1987), 1-102.

14.  HUGHES, G.E., AND CRESSWELL, M.J. An Introduction to Modal Logic. Methuen, New York,

1968.

15.  KOHL, J., NEUMAN, C., AND STEINER, J. The Kerberos network authentication ser~ vice (version 5, draft 3). Available by anonymous FTP from athena-dist.mit.edu, as /pub/doc/kerberos/V5DRAFT3~RFC. {PS ,TXT}, Oct. 1990.

16.  KOZEN, D. A completeness theorem for Kleene algebras and the algebra of regular events. Cornell TR90-1123, May 1990.

17.  LAMPSON, B., ABADI, M., BURROWS, M., AND WOBBER, E. Authentication in distributed systems: theory and practice. ACM Trans. Comput. Syst. 10, 4 (November 1992), 265-310.

18.  LEVY, H. Capability-based Computer Systems. Digital Press, 1983.

19.  MILLER, S.P., NEUMAN, C., SCHILLER, J.I., AND SALTZER, J.H. Kerberos authentication and authorization system. In Project Athena Technical Plan, Section E.2.1, MIT, July 1987.

20.  NEEDHAM, R.M., AND SCHROEDER, M.D. IJsing encryption for authentication in large net~ works of computers. Commun. ACM 21, 12 (Dec. 1978), 993-999.

21. PRATT, V. Dynamic algebras as a well-behaved fragment of relation algebras. In Algebraic Logic and Universal Algebra in Computer Science, Springer-Verlag Lecture Notes in Com­puter Science 425, 1990, 77110.

22. RIVEST, E. L., SHA1IR, A., AND ADLEMAN, L. A method for obtaining digital signatures and public-key cryptosystems. Commun. ACM 21, 2 (Feb. 1978), 120 126.

23. SALTZER, J., AND SCHR0EDER, M. The protection of information in computer systems. Proc. IEEE 63, 9 (Sept. 1975), 1278 1308.

24. S0LLINS, K. Cascaded authentication. In Proceedings of the 1988 IEEE Symposium on Se­curity and Privacy (April 1988), 156 163.

25. VICKERS, S. Samson Abramsky on linear process logics. Foundation Workshop Notes, Oct.- Nov. 1988.

26. YETTER, D.N. Quantales and (noncommutative) linear logic. .1. Symb. Logic 55, 1 (March 1990), 41 64.

Heceived August 1991; revised September 1992; accepted November 1992.