*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

MART^{u}IN
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;
authentication; 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 communication
cannot be taken for granted. Since it is hard to provide physically secure communication lines, some form of encryption is
typically required. In what follows, 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. Therefore,
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 describing 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 semantics. The laws for as and for appear in Sections 4 and 5.

This section includes
discussions of alternative approaches and of relevant mathematical 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 membership 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 multiplicative 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 manipulate 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 structures 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 relations 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 operators on principals beyond A and . Here we
consider a few operators with a mathematical origin. These operators are used
very seldom elsewhere in this paper.

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 lattice. 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 quantale. 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 substitutivity 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 W^{2}. 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 represent 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 collection 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 UNIX^{TM} 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.

^{TM}UNIX 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 conjunction 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 authentication 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 describe
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 authority 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 digital
signatures, for example with the RSA algorithm [22]. We denote by KA and KB the public keys for A and B, and by _{K}^{b}'_{}

$ and _{K}^{b}'_{}

B the matching secret keys.

The formula K says X represents the certificate X encrypted under K^{b}', 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 _{K}^{b}'_{}

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 _{K}^{b}'_{}

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 delegation 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 properties 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 certificate 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 delegation. 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 certificate
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 convenient 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 assumptions 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 assumptions 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, {R^{1} _{Q},_{ }._{
}._{ }._{ },_{ R}^{P}Q^{}

Q }) . . . . . (P1,{R^{1}
1,...,R^{P1}

1 })

such that

(P1 as R^{1}1 as ... as _{R}^{P}1^{}

1 ) for ... for (P _{Q }as R1 Q as ... as _{R}^{P}Q^{}

Q )

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

(PQ, {R^{1} _{Q},_{ }._{ }._{ }._{ },_{ R}^{P}Q^{}

Q }) c . . . c (P1,{R^{1} 1,...,R^{P1}

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 R^{1}1 as ... as _{R}^{P}1^{}

1 ) for ... for (P _{Q }as R1 Q as ... as _{R}^{P}Q^{}

Q )

This
implies that the empty string is related to

(PQ, {R^{1} _{Q},_{ }._{ }._{ }._{ },_{ R}^{P}Q^{}

Q }) c . . . c (P1,{R^{1} 1,...,R^{P1}

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 workstation'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
certification 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 matters
that deserve more detailed treatments. In addition, the basic logic could be extended in many interesting ways. To conclude,
we briefly describe three extensions.

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 situation 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 Computer 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 Security 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.