Citation: B. Lampson, M. Abadi, M. Burrows, and E. Wobber. Authentication in distributed systems: Theory and practice. ACM Trans. Computer Systems 10, 4 (Nov. 1992), pp 265-310. A preliminary version is in the Proc. 13th ACM Symposium on Operating Systems Principles.

Links: Abstract, Postscript, Acrobat, Word.

Email: blampson@microsoft.com. This paper is at http://www.research.microsoft.com.

Different kinds of channels make statements in different ways. A channel’s statement may arrive on a wire from a terminal to serial port 14 of a computer. It may be obtained by successfully decrypting with des key #574897, or by verifying a digital signature on a file stored two weeks ago. It may be delivered by a network with a certain source address, or as the result of a kernel call to the local operating system. Most of these channels are real-time, but some are not.

Often several channels are produced by multiplexing a single one. For instance, a network channel to the node with ip address 16.4.0.32 may carry udp channels to ports 2, 75, and 443, or a channel implemented by a kernel call trap from a user process may carry interprocess communication channels to several other processes. Different kinds of multiplexing have much in common, and we handle them all uniformly. The subchannels are no more trustworthy than the main channel. Multiplexing can be repeated indefinitely; for example, an interprocess channel may carry many subchannels to various remote procedures.

Hierarchical names are closely connected to multiplexed channels: a single name like /com/dec/src can give rise to many others (/com/dec/src/burrows, /com/dec/src/abadi, ...). Section 5.2 explores this connection.

Finally, we use caching to make frequent operations fast. A cache usually needs a way of removing entries that become invalid. For example, when caching the fact that key #574897 speaks for Burrows we must know what to do if the key is compromised. We might remember every cache that may hold this information and notify them all when we discover the compromise. This means extra work whenever a cache entry is made, and it fails if we can’t talk to the cache.

To help readers who dislike formulas, we highlight the main results by boxing them. These readers do need to learn the meanings of two symbols:
A Þ B (A speaks for B) and A|B (A quoting B); both are explained below.

Throughout the paper we write statements in a form intended to make their meaning clear. When processed by a program or transmitted on a channel they are encoded to save space or make it easier to manipulate them. It has been customary to write them in a style closer to the encoded form than the meaningful one. For example, a Needham-Schroeder authentication ticket [19] is usually written {Kab, A}Kbs. We write Kbs says Kab Þ A instead, viewing this as the abstract syntax of the statement and the various encodings as different concrete syntaxes. The choice of encoding does not affect the meaning as long as it can be parsed unambiguously.

It follows from (S1)–(S4) that says distributes over Ù:

In our theory there is a set of principals; we gave many examples in Section 2. The symbols A and B denote arbitrary principals, and usually C denotes a channel. There are two basic operators on principals, Ù (and) and | (quoting). The set of principals is closed under these operators. We can grasp their meaning from the axioms that relate them to statements:

The Ù and | operators satisfy certain equations:

Now we can define Þ, the ‘speaks for’ relation between principals, in terms of Ù and =:

Equation (P7) is a strong definition of ‘speaks for’. It’s possible to have a weaker, qualified version in which (P8) holds only for certain statements s. For instance, we could have “speaks for reads” which applies only to statements that request reading from a file, or “speaks for file foo" which applies only to statements about file foo. Neuman discusses various applications of this idea [20]. Or we can use roles (see Section 6) to compensate for the strength of Þ, for instance by saying A Þ (B as reader) instead of A Þ B.

The operators Ù and Þ satisfy the usual laws of the propositional calculus. In particular, Ù is monotonic with respect to Þ. This means that if A Þ B then A Ù C Þ B Ù C. It is also easy to show that | is monotonic in both arguments and that Þ is transitive. These properties are critical because C Þ A is what authenticates that a channel C speaks for a principal A or that C is a member of the group A. If we have requests Kabadi says “read from foo" and Kburrows says "read from foo", and file foo has the acl SRC Ù Manager, we must get from Kabadi Þ Abadi Þ src and Kburrows Þ Burrows Þ Manager to Kabadi Ù Kburrows Þ SRC Ù Manager. Only then can we reason from the two requests to SRC Ù Manager says "read from foo", a request that the acl obviously grants.

The following handoff axiom makes it possible for a principal to introduce new facts about Þ:

In other words, A has the right to allow any other principal B to speak for it. There is a simple rule for applying (P10): when you see A says s you can conclude s if it has the form B Þ A. The same A must do the saying and appear on the right of the Þ, but B can be any principal.

What is the intuitive justification for (P10)? Since A can make A says (B Þ A) whenever it likes, (P10) gives A the power to make us conclude that A says s whenever B says s. But B could just ask A to say s directly, which has the same effect provided A is competent and accessible.

From (P10) we can derive a theorem asserting that it is enough for the principal doing the saying to speak for the one on the right of the Þ, rather than being the same:

Proof: the premise implies A says B Þ A by (P8), and this implies the conclusion by (P10). This theorem, called the handoff rule, is the basis of our methods for authentication. When we use it we say that A´ hands off A to B.

From this and (P10) we can deduce B Þ A given A says (A´ Ù B Þ A) and A´ says B Þ A´. Thus A can let A´ and B speak for it jointly, and A´ can let B exercise this authority alone. One situation in which we might want both A and A´ is when A is usually off line and therefore makes its statement with a much longer lifetime than A´ does. We can think of the statement made by A´ as a countersignature for A’s statement. (P12) is the basis for revoking authentication certificates (Section 5) and ending a login session (Section 7).

The last two theorems illustrate how we can prove B Þ A from our axioms together with some premises of the form A´ says (B´ Þ A´ ). Such a proof together with the premises is called B’s credentials for A. Each premise has a lifetime, and the lifetime of the conclusion, and therefore of the credentials, is the lifetime of the shortest-lived premise. We could add lifetimes to our formalism by introducing a statement form s until t and modifying (S2)–(S3) to apply the smallest t in the premises to the conclusion, but here we content ourselves with an informal treatment.

As we have seen, the essential property of a channel is that its statements can be taken as assumptions: formulas like C says s are the raw material from which everything else must be derived. On the other hand, the channel by itself doesn’t usually mean much—seeing a message from terminal port 14 or key #574897 isn’t very interesting unless we can deduce something about who must have sent it. If we know the possible senders on C, we say that C has integrity. Similarly, if we know the possible receivers we say that C has secrecy, though we have little to say about secrecy in this paper.

Knowing the possible senders on C means finding a meaningful A such that C Þ A; we call this authenticating the channel. Why should we believe that C Þ A? Only because A, or someone who speaks for A, tells us so. Then the handoff rule (P11) lets us conclude C Þ A. In the next section we study the most common way of authenticating C. Here we investigate why A might trust C enough to make A says C Þ A, or in other words, why A should believe that only A can send messages on C.

Our treatment is informal. We give some methods of using encryption and some reasons to believe that these methods justify statements of the form “a channel implemented by des encryption and decryption using key #8340923 speaks for lampson". We do not, however, try to state precise assumptions about secrecy of keys and properties of algorithms, or to derive such facts about ‘speaks for’ from them. These are topics for another paper.

The first thing to notice is that for A to assert C Þ A it must be able to name C. A circumlocution like “the channel that carries this message speaks for A” won’t do, because it can be subverted by copying the message to another channel. As we consider various channels, we discuss how to name them.

We are mainly interested in channels that depend on encryption for their security; as we shall see, they add less to the tcb than any others. We begin by summarizing the essential facts about such channels. An encryption channel consists of two functions Encrypt and Decrypt and two keys K and K–1. By convention, we normally use K to receive (decrypt) and K–1 to send (encrypt). Another common notation for Encrypt(K–1, x) is {x}K–1.

An encryption algorithm that is useful for computers provides a channel: for any message x, Decrypt(K, Encrypt(K–1, x)) = x. The algorithm keeps the keys secret: if you know only x and Encrypt(K–1, x) you can’t compute K or K–1, and likewise for Decrypt. Of course “can’t compute” really means that the computation is too hard to be feasible.

The usual way to get both properties at once is to add a suitable checksum to the cleartext and check it in Decrypt, as shown in Figure 3. The checksum should provide enough redundancy to make it very unlikely that decrypting with K will succeed on a message not produced by encrypting with K–1. Achieving this property requires some care [10, 28].

In shared key encryption K = K–1. Since anyone who can receive can also send under K, this is only useful for pairwise communication between groups of principals that trust each other completely, at least as far as messages on K are concerned. The most popular shared key encryption scheme is the Data Encryption Standard or des [18]. We denote an encryption channel with the des key K by des(K), or simply by K when the meaning is clear; the channel speaks for the set of principals that know K.

In public key encryption K ¹ K–1, and in fact you can’t compute one from the other. Usually K is made public and K–1 kept private, so that the holder of K–1 can broadcast messages with integrity; of course they won’t be secret. Together, K and K–1 are called a key pair. The most popular public key encryption scheme is Rivest-Shamir-Adleman or rsa [21]. In this scheme (K–1)–1 = K, so anyone can send a secret message to the holder of K–1 by encrypting it with K. We denote an encryption channel with the rsa public key K by rsa(K), or simply by K when the meaning is clear; the channel speaks for the principal that knows K–1.

With this background we can discuss how to make a practical channel from an encryption algorithm. From the existence of the bits Encrypt(K–1, s) anyone who knows K can infer K says s, so we tend to identify the bits and the statement; of course for the purposes of reasoning we use only the latter. We often call such a statement a certificate, because it is simply a sequence of bits that can be stored away and brought out when needed like a paper certificate. We say that K signs the certificate.

To describe our methods precisely we need some notation for keys and key identifiers. Subscripts and primes on K denote different keys; the choice of subscript may be suggestive, but it has no formal meaning. A superscripted key does have a meaning: it denotes a key identifier for that key, and the superscripts indicate who can extract the key from the identifier. Thus Kr denotes R’s key identifier for K, and if Ka and Kb are key identifiers for the two parties to the shared key K, then Kab denotes the pair (Ka, Kb). The formula Kr says s denotes a pair: the statement K says s together with a hint Kr to R about the key that R should use to check the signature. Concretely, Kr says s is the pair (Encrypt(K–1, s), Kr). Thus the r doesn’t affect the meaning of the statement at all; it simply helps the receiver to decrypt it. This help is sometimes essential to the functioning of a practical protocol.

A key identifier Kr for a receiver R might be any one of:

In the second case R can extract the key from the identifier without any state except its master key Krm, and in the third case without any state except what it needs for K´r. An encrypted key may be weaker cryptographically than a table index, but we believe that it is safe to use it as a key identifier, since it is established practice to distribute session keys encrypted by master keys [19, 26, 28].

Since R simulates public key encryption, we assume that any principal A can get a channel to R. This channel is a key shared by R and A along with key identifiers for both parties. To set it up, A goes to a trusted agent, which may be off line, and talks to it on some physically secure channel such as a hard-wired keyboard and display or a dedicated RS-232 line. The agent makes up a key K and tells A both K and Kr, R’s key identifier for K; to make Kr the agent must know R’s master key. Finally, A constructs Ka, its own key identifier for K. Now A has Kar, its two-way channel to R.

Given both Kar says s (a message encrypted by a shared key Ka together with R’s key identifier for Ka) and Kbbr (the pair (Kbb, Kbr), which constitutes a two-way shared-key channel between R and some B with the shared key Kb), the relay R will make Kbb|Kar says s on demand. The relay thus multiplexes all the channels it has onto its channel to B, indicating the source of each message by the key identifier. The relay is not vouching for the source A of s, but only for the key Ka that was used to encrypt s. In other words, it is simply identifying the source by labelling s with Kar and telling anyone who is interested the content of s. Thus it makes the channel Kar into a broadcast channel, and this is just what public key encryption can do. Like public key encryption, the relay provides no secrecy; of course it could be made fancier, but we don’t need that for authentication. B’s name for the channel from A is Kbb|Kar.

There is an added complication for authenticating a channel. With public keys, a certificate like Kca says Ka Þ A authenticates the key Ka. In the simulation this becomes Kcar says Kax Þ A for some X, and relaying this to B is not useful because B cannot extract Ka from Kax unless X happens to be B. But given Kcar says Kaar Þ A and Kbbr as before, R can invent a new key K and splice the channels Kaar and Kbbr to make a two-way channel Kab = (Ka, Kb) between A and B. Here Ka and Kb are defined in the lower right corner of Table II; they are the third kind of key identifier mentioned earlier. Observe that A can decrypt Ka to get hold of K, and likewise for B and Kb. Now R can translate the original message into Kbb|Kcar says Kab Þ A, just what B needs for authenticated communication with A. For two-way authentication, R needs Kcar says Kbbr Þ B instead of just Kbbr; from this it can make the symmetric certificate Kaa|Kcar says Kab Þ B.

Table II summarizes the construction, which uses an essentially stateless relay to give shared key encryption the properties of public key encryption. The only state the relay needs is its master key; the client supplies the channels Kar and Kbbr. Because of its minimal state, it is practical to make such a relay highly available as well as highly secure.

Even with this simulation, shared key encryption is not as secure as public key: if the relay is compromised then existing shared keys are compromised too. With public key encryption a certificate like Kca says Ka Þ A which authenticates the key Ka can be both issued and used without disclosing Ka–1 to anyone. Public key also has a potential performance advantage: there is no common on-line agent that must provide service in order for authenticated communication to be established between A and B. The simulation requires the relay to be working and not overloaded, and all other schemes that use shared keys share this property as well.

We set up a node-to-node channel between nodes A and B in three phases; see Table III. In the first phase each node sends its public rsa key to the other node. It knows the corresponding private key, having made its key pair when it was booted (see Section 6). In phase two each node chooses a random des key, encrypts it with the other node’s public key, and sends the result to the other node, which decrypts with its own private key. For example, B chooses Jb and sends Encrypt(Ka, Jb) to A, which decrypts with Ka–1 to recover Jb. In the third phase each node computes K = Hash(Ja, Jb), makes a key identifier for K, and sends it to the other node. Now each node has Kab (the key identifiers of A and B for the shared key K); this is just what they need to communicate. Each node can make its own key identifier however it likes; for concreteness, Table III shows it being done by encrypting K with the node’s master key.

A believes that only someone who can decrypt Encrypt(Kb, Ja) could share its knowledge of K. In other words, A believes that K Þ Kb. This means that A takes K Þ Kb as an assumption of the theory; we can’t prove it because it depends both on the secrecy of rsa encryption and on prudent behavior by A and B, who must keep the J’s and K secret. We have used the secrecy of an rsa channel to avoid the need for the certificate Kb says “The key with digest D Þ Kb”, where D = Digest(K).

Now whenever A sees K says s, it can immediately conclude Kb says s. Thus when A receives a message on channel K, which changes whenever there is rekeying, it also receives the message on channel Kb, which does not change as long as B is not rebooted. Of course B is in a symmetric state. Finally, if either node forgets K, running the protocol again makes a new des channel that speaks for the same public key on each node. Thus the des channel behaves like a cache entry; it can be discarded at any time and later re-established transparently.

The only property of the key pair (Ka, Ka–1) that channel setup cares about is that Ka–1 is A’s secret. Indeed, channel setup can make up the key pair. But Ka is not useful without credentials. The node A has a node key Kn and its credentials Kn Þ A´ for some more meaningful principal A´, for instance VaxSN5437 as VMS5.4 (see Section 6). If Ka comes out of the blue, the node has to sign another certificate, Kn says Ka Þ Kn, to complete Ka’s credentials, and everyone authenticating the node has to check this added certificate. That is why in our system the node tells channel setup to use (Kn, Kn–1) as its key pair, rather than allowing it to choose a key pair.

There are two general methods, push and pull. Both produce the same credentials for A, a set of certificates and a proof that they establish C Þ A, but the two methods collect the certificates differently.

So everyone can deduce Kca Þ A for every named A. At first this may seem too strong, but trusting CA to authenticate channels from A means that CA can speak for A, because it can authenticate as coming from A some channel that CA controls.

For each A that it speaks for, CA issues a certificate of the form Kca says Ka Þ A in which A is a name. The certificates are stored in a database and indexed by A. This database is usually called a name service; it is not part of the tcb because the certificates are digitally signed by Kca. To get A’s credentials you go to the database, look up A, get the certificate Kca says Ka Þ A, verify that it is signed by the Kca that you believe speaks for CA, and use the handoff rule to conclude Ka Þ A, just what you wanted to know. The right side of Figure 5 shows what B does, and the symmetric left side shows what A does to establish two-way authentication.

The figure shows only the logical flow of secure messages. An actual implementation has extra insecure messages, and the bits of the secure ones may travel by circuitous paths. To push, the sender A calls the database to get Kca says Ka Þ A and sends it along with a message signed by Ka. To pull, the receiver B calls the database to get the same certificate when B gets a message that claims to be from A or finds A on an acl. The Needham-Schroeder protocol [19] combines push and pull: when A wants to talk to B it gets two certificates from CA, the familiar Kca says Ka Þ A which it pushes along to B, and Kca says Kb Þ B for A’s channel from B.

As we have seen, with public key certificates it’s not necessary to talk to CA directly; it suffices to talk to a database that stores CA’s certificates. Thus CA itself can be normally off line, and hence much easier to make highly secure. Certificates from an off line CA, however, must have fairly long lifetimes. For rapid revocation we add an on line agent O and use the joint authority rule (P12). CA makes a weaker certificate Kca says (O|Ka Ù Ka) Þ A, and O countersigns this by making O|Ka says Ka Þ O|Ka. From these two, Kca Þ A, and (P12) we again get Ka Þ A, but now the lifetime is the minimum of those on CA’s certificate and O’s certificate. Since O is on line, its certificate can time out quickly and be refreshed often. Note that CA makes a separate certificate for each Ka it authenticates, and each such certificate makes it possible for O to convince a third party that Ka Þ A only for specific values of Ka and A. Thus the tcb for granting access is just CA, because O acting on its own can’t do anything, but CA speaks for A; the tcb for revocation is CA and O, since either one can prevent access from being revoked.

Our system uses the pull method throughout; we discuss the implications in Sections 8 and 9. Hence we can use a cheap version of the joint authority scheme for revocation; in this version a certificate from CA is believed only if it comes from the server O that stores the database of certificates. To authenticate A we first authenticate a channel Co from O. Then we interpret the presence of the certificate Kca says (O|Ka Ù Ka) Þ A on the channel Co as an encoding of the statement Co |Ka says Ka Þ O|Ka. Because Co Þ O, this implies O|Ka says Ka Þ O|Ka, which is the same statement as before, so we get the same conclusion. Note that O doesn’t sign a public-key certificate for A, but we must authenticate the channel from O, presumably using the basic method. Or replace O by Ko everywhere. Either way, we can’t revoke O’s authority quickly; it’s not turtles all the way down.

A straightforward alternative to an on line agent that asserts O|Ka says Ka Þ O|Ka is a ‘black-list’ agent or recent certificate that asserts “all of CA’s certificates are valid except the ones for the following keys: K1, K2, ...” [5]. For obvious reasons this must be said in a single mouthful. Such revocation lists are used with Internet privacy-enhanced mail.

The formalization of Figure 5 also describes the Kerberos protocol [15, 26]. Kerberos uses shared rather than public key encryption. Although its designers didn’t know about the relay simulation described in Section 4.3, the protocol can be explained as an application of that idea to public key certificates. Here are the steps; they correspond to the union of Figure 5 and Table II. First A gets from CA a certificate Kcar says Kaar Þ A. Kerberos calls CA the ‘authentication server’, the certificate a ‘ticket granting ticket’, and the relay R the ‘ticket granting server’. The relay also has a channel to every principal that A might talk to; in particular R knows Kbbr Þ B. To authenticate a channel from A to B, A sends the certificate to R, which splices Kaar and Kbbr to turn it into Kbb says Kab Þ A. This is called a ‘ticket’, and A sends it on to B, which believes Kb Þ Anybody because Kb is B’s channel to CA. As a bonus, R also sends A a certificate for B: Kaa says Kab Þ B.

In practice, application programs normally use Kerberos to authenticate network connections, which the applications then rather unrealistically treat as secure channels. To do this, A makes Kb says cia Þ A, where cia is A’s network address and connection identifier; this is called an ‘authenticator’. A sends both the ticket and the authenticator to B, which can then deduce cia Þ A in the usual way. The ticket has a fairly long lifetime so that A doesn’t have to talk to R very often; the authenticator has a very short lifetime in case the connection is closed and cia then reused for another connection not controlled by A. Kerberos has other features that we lack space to analyze.

If the name space is a tree, so that names are path names, it is natural to arrange the certification authorities in a corresponding tree. The lack of global trust means that a parent cannot unconditionally speak for its children; if it did, the root would speak for everyone. Instead when you want to authenticate a channel from A = /A1 /A2 /.../An you start from an authority that you believe has the name B = /B1 /B2 /.../Bm and traverse the authority tree along the shortest path from B to A, which runs up to the least common ancestor of B and A and back down to A. Figure 6 shows the path from /dec/burrows to /mit/clark; the numbers stand for public keys. The basic idea is described in Birrell et al. [3]; it is also implemented in spx [27].

We can formalize this idea with a new kind of compound principal, written P except N, and some axioms that define its meaning. Here M or N is any simple name and P is any path name, that is, any sequence of simple names. We follow the usual convention and separate the simple names by ‘/ ’ symbols. Informally, P except N is a principal that speaks for any path name that is an extension of P as long as the first name after P isn’t N, and for any prefix of P as long as N isn’t ‘..’. The purpose of except is to force a traversal of the authority tree to keep going outward, away from its starting point. If instead the traversal could retrace its steps, then a more distant authority would be authenticating a nearer one, contrary to our idea that trust should be as local as possible. The axioms for except are:

The quoting principals on the left side of Þ prevent something asserted by P except M from automatically being asserted by all the longer path names. Note that usually both (N2) and (N3) apply. For instance, /dec except burrows speaks for /dec/abadi except ‘..’ by (N2) and for / except dec by (N3).

Now we can describe the credentials that establish C Þ A in our system. Suppose A is /mit/clark. To use the (N) rules we must start with a channel from some principal B that can authenticate path names; that is, we need to believe Cb Þ B except N. This could be anyone, but it’s simplest to let B be the authenticating party. In Figure 6 this is /dec/burrows, so initially we believe Cburrows Þ /dec/burrows except nil, and this channel is trusted to authenticate both up and down. In other words, Burrows knows his name and his public key and trusts himself. Then each principal on the path from B to A must provide a certificate for the next one. Thus we need

The certificates quoting ‘..’ can be thought of as ‘parent’ certificates pointing upward in the tree, those quoting mit and clark as ‘child’ certificates pointing downward. They are similar to the certificates specified by ccitt X.509 [5].

From this and the assumption Cburrows Þ /dec/burrows except nil, we deduce in turn the body of each certificate, because for each A´ says C´ Þ B´ we have A´ Þ B´ by reasoning from the initial belief and the (N2-3) rules, and thus we can apply (P11) to get C´ Þ B´ . Then (N1) yields Cclark Þ /mit/clark, which authenticates the channel Cclark from /mit/clark. In the most secure implementation each line represents a certificate signed by the public key of an off line certifier plus a message on some channel from an on line revocation agent; see Section 5.1. But any kind of channel will do.

If we start with a different assumption, we may not accept the bodies of all these certificates. Thus if /mit/clark is authenticating /dec/abadi, we start with Cclark Þ /mit/clark except nil and believe the bodies of the certificates

Since this path is the reverse of the one we traversed before except for the last step, each principal that supplies a parent certificate on one path supplies a child certificate on the other. Note that clark would not accept the bodies of any of the certificates on the path from burrows. Also, the intermediate results of this authentication differ from those we saw before. For example, when B was /dec/burrows we got Cdec Þ /dec except burrows, but if B is /mit/clark we get Cdec Þ /dec except ‘..’. From either we can deduce Cdec Þ /dec, but Cdec’s authority to authenticate other path names is different, because burrows and clark have different ideas about how much to trust dec.

In other words, the mit certification authority is willing to authenticate Cclark as speaking for clark relative to Cmit or to any name that Cmit might speak for; the authority takes responsibility only for names relative to itself. The corresponding assertion in a parent certificate, on the other hand, is a mistake. It would be

Since mit’s parent can change as a result of renaming higher in the tree, this certificate, which does not distinguish one parent from another, is too strong.

Our method for authenticating path names using the (N) axioms requires B to trust each certification authority on the path from B up to the least common ancestor and back down to A. If the least common ancestor is lower in the tree then B needs to trust fewer authorities. We can make it lower by adding a ‘cross-link’ named mit from node 56 to node 37: Cdec says Cmit Þ /dec/mit except ‘..’. Now /dec/mit/clark names A, and node 21 is no longer involved in the authentication. The price is more system management: the cross-link has to be installed, and it also has to be changed when mit’s key changes. Note that although the tree of authorities has become a directed acyclic graph, the least-common-ancestor rule still applies, so it’s still easy to explain who is being trusted.

A principal doing a lookup might have channels from several other principals instead of the single channel Cb from itself that we described. Then it could start with the channel from the principal that is closest to the target A and thus reduce the number of intermediaries that must be trusted. This is essential if the entire name space is not connected, for instance if it is a forest with more than one root, since with only one starting point it is only possible to reach the names in one connected component of the name space. Each starting point means another built-in key, however, and maintaining these keys obviously makes it more complicated to manage the system. This is why our system doesn’t use such sets of initially trusted principals.

When we use path names the names of principals are more likely to change, because they change when the directory tree is reorganized. This is a familiar phenomenon in file systems, where it is dealt with by adding either extra links or symbolic links to the renamed objects (usually directories) that allow old names to keep working. Our system works the same way; a link is a certificate asserting that some channel C Þ P, and a symbolic link is a certificate asserting P´ Þ P. This makes pulling more attractive, because pushing requires the sender to guess which name the receiver is using for the principal so that the sender can provide the right certificates.

We can push without guessing if we add a level of indirection by giving each principal a unique identifier that remains the same in spite of name changes. Instead of C Þ P we have C Þ id and id Þ P. The sender pushes C Þ id and the receiver pulls id Þ P. In general the receiver can’t just use id, on an acl for example, because it has to have a name so that people can understand the acl. Of course it can cache id Þ P; this corresponds to storing both the name and the identifier on the acl. There is one tricky point about this method: id can’t simply be an integer, because there would be no way of knowing who can speak for it and therefore no way to establish C Þ id. Instead, it must have the form A/integer for some other principal A, and we need a rule A Þ A/integer so that A can speak for id. Now the problem has been lifted from arbitrary names like P to authorities like A, and maybe it is easier to handle. Our system avoids these complications by using the pull model throughout.

A group is a principal that has no public key or other channel of its own. Instead, other principals speak for the group; they are its members. Looking up a group name G yields one or more group membership certificates Kca says P1 Þ G, Kca says P2 Þ G, ..., where Kca Þ G, just as the result of looking up an ordinary principal name P is a certificate for its channel Kca says C Þ P, where Kca Þ P. A symbolic link can be viewed as a special case of a group.

A quite different way to express group membership when the channels are public keys is to give G a key Kg and a corresponding certificate Kca says Kg Þ G, and to store Encrypt(Kp, Kg–1) for each member P in G’s database entry. This means that each member will be able to get Kg–1 and therefore to speak for the group, while no other principals can do so.

The advantage is that to speak for G, P simply makes Kg says s, and to verify this a third party only needs Kg Þ G. In the other scheme, P makes Kp says s, and a third party needs both Kp Þ P and P Þ G. So one certificate and one level of indirection are saved. One drawback is that to remove anyone from the group requires choosing a new Kg and encrypting it with each remaining member’s Kp. Another is that P must explicitly assert its membership in every group G needed to satisfy the acl, either by signing s with every Kg or by handing off from every Kg to the channel that carries s. A third is that the method doesn’t work for principals that don’t have permanent secret keys, such as roles or programs. Our system doesn’t use this method.

We capture the fact that A as R is weaker than A by assuming that A speaks for A as R. Because adopting a role implies behaving appropriately for that role, A must be careful that what it says on its own is appropriate for any role it may adopt. Note that we are not assuming A Þ A|B in general, but only when B is a role. Formally, we introduce a subset Roles of the simple principals and the axioms:

If the principal is a person, it can just decide to do so; in this case we can’t give any formal rule for when the principal should be willing to assume the role. Consider the example of a user acting as system manager for her workstation. Traditionally (in Unix) she does this by issuing a su command, which expresses her intention to issue further commands that are appropriate for the manager. In our system she assumes the role "user as manager". There is much more to be said about roles for users, enough to fill another paper.

Digests are to roles in general much as encryption keys are to principals in general: they are unintelligible to people, and the same program specification may apply to several program texts (perhaps successive versions) and hence to several digests. In general we want the role to have a name, and we say that the digest speaks for the role. Now we can express the fact that digest D speaks for the program named P by writing D Þ P. There are two ways to use this fact. The receiver of A as D says s can use D Þ P to conclude that A as P says s because as is monotonic. Alternatively, A can use D Þ P to justify making A as P says s whenever program D asserts s.

So far we have been discussing how a principal can decide what role to assume. The principal must also be able to convince others. Since we are encoding A as P as A|P, however, this is easy. To make A as P says s, A just makes A says P says s as we saw earlier, and to hand off A as P to some other channel C it makes A as P says (C Þ A as P).

If A trusts the file system to speak for P, it hands off to pr the right to speak for A as P, using the mechanisms described in Section 8 or in the treatment of booting below; this is much like running a Unix setuid program. Now pr is a protected subsystem; it has an independent existence and authority consistent with the program it is running. Because pr can speak for A as P, it can issue requests to an object with A as P on its acl, and the requests will be granted. Such an acl entry should exist only if the owner of the object trusts A to run P. In some cases B might hand off to pr some of the principals it can speak for. For instance, if B is a shell it might hand off its right to speak for the user that is logged in to that shell.

If A doesn’t trust the file system, it computes the digest D of the program text and looks up the name P to get credentials for D Þ P. Having checked these credentials it proceeds as before. There’s no need for A to record the credentials, since no one else needs to see them; if you trust A to run P, you have to trust A not to lie to you when it says it is running P.

It is often useful to form a group of programs, for instance, /com/dec/src/trustedSW. A principal speaking for this name, for example, the key Kca of its certification authority, can issue a certificate Kca says P Þ /com/dec/src/trustedSW for a trusted program P. If A as /com/dec/src/trustedSW appears on an acl, any program P with such a certificate will get access when it runs on A because as is monotonic. Note that it’s explicit in the name that /com/dec/src is certifying this particular set of trusted software.

Virus control is one obvious application. To certify a program as virus-free we compute its digest D and issue a membership certificate Kca says D Þ trustedSW (from now on we elide /com/dec/src/). There are two ways to use these certificates:

There can also be groups of nodes. An acl might contain DBServers as Ingres; then if A Þ DBServers (A is a member of the group DBServers), A as Ingres gets access because as is monotonic. If we extend these ideas, DBSystems can be a principal that stands for a group of systems, with membership certificates such as DBServers as Ingres Þ DBSystems, Mainframes as DB2 Þ DBSystems, and so on.

One is that the machine is the base case for authenticating a system, and it authenticates its messages by knowing a private key Km–1 which is stored in nonvolatile memory. Making and authenticating this key is part of the process of installing M, that is, putting it into service when it arrives. In this process M constructs a public key pair (Km, Km–1) and outputs the public key Km. Then someone who can speak for the name M, presumably an administrator, makes a certificate Kca says Km Þ M. Alternatively, a certification authority constructs (Km, Km–1), makes the certificate Kca says Km Þ M, and delivers Km–1 to M in some suitably secure way. It is an interesting problem to devise a practical installation procedure.

The machine M also needs to know the name and public key of some principal that it can use to start the path name authentication described in Section 5; this principal can be M itself or its local certification authority. This information can be stored in M during installation, or it can be recorded in a certificate signed by Km and supplied to M during booting along with P.

You might think that all this is too much to put into a boot rom. Fortunately, it’s enough if the boot rom can compute the digest function and knows one digest (set at installation time) that it trusts completely. Then it can just load the program Pboot with that digest, and Pboot can act as part of M. In this case, of course, M gives Km–1 to Pboot to express its complete trust.

We have seen how a principal can hand off all of its authority to another, and how a principal can limit its authority using roles. We now consider a combination of these two methods that allows one principal to delegate some of its authority to another one. For example, a user on a workstation may wish to delegate to a compute server, much as she might rlogin to it in vanilla Unix. The server can then access files on her behalf as long as their acls allow this access. Or a user may delegate to a database system, which combines its authority with the delegation to access the files that store the database.

A minor variation of the basic scheme handles delegation from the user U to the workstation W on which she logs in. The one difference arises from the assumption that the user’s key Ku is available only while she is logging in. This seems reasonable, since getting access to the user’s key will require her to type her password or insert her smart card and type a pin; the details of login protocols are discussed elsewhere [1, 26, 27]. Hence the user’s delegation to the workstation at login must have a rather long lifetime, so that it doesn’t need to be refreshed very often. We therefore use the joint authority rule (P12) to make this delegation require a countersignature by a temporary public key Kl. This key is made at login time and called the login session key. When the user logs out, the workstation forgets Kl–1 so that it can no longer refresh any credentials that depend on the login delegation, and hence can no longer act for the user after the 30-minute lifetime of the delegation has expired. This protects the user in case the workstation is compromised after she logs out. If the workstation might be compromised within 30 minutes after a logout, then it should also discard its master key and node key at logout.

The credentials for login start with a long-term delegation from the user to Kw Ù Kl (here Kw is the workstation’s node key), using Ku for A and Kw for the second B in (1):

Kw accepts the delegation in the usual way, so we know that

and because | distributes over Ù we get

Next Kl signs a short-term certificate

This lets us conclude that Kw|Ku Þ Kl|Ku by the handoff rule and the monotonicity of |. Now we can apply (P12) and reach the usual conclusion for delegation, but with a short lifetime:

Figure 7 is an expanded version of the example in Figure 1. For each component it indicates the principals that the component speaks for and the channel it can send on (usually an encryption key). Thus the Taos node speaks for WS as Taos and has the key Kn–1 so it can send on channel Kn. The accounting application speaks for WS as Taos as Accounting for bwl; it runs as process pr, which means that the node will let it send on Kn | pr or C | pr. Consider a request from the accounting application to read file foo. It has the form C | pr says "read foo"; in other words, C | pr is the channel carrying the request. This channel speaks for Kws as Taos as Accounting for Kbwl. The credentials of C | pr are:

The server gets certificates for the first three premises in the credentials. The last premise does not have a certificate. Instead, it follows directly from a message on the shared key channel C between the Taos node and the server, because this channel speaks for Kn as described in Section 4.

To turn these into credentials of C | pr for WS as Taos as Accounting for bwl, the server must obtain the certificates that authenticate channels for the names bwl and WS from the certification database as described in Section 5. Finally, to complete the access check, the server must obtain the group membership certificate WS as Taos Þ SRC-node. A system using the push model would substitute names for one or both of the keys Kws and Kbwl. It would also get the name certificates for WS and bwl from the database and add them to the credentials.

Most messages use a channel between a sending process on the sending node and a receiving process on the receiving node. As we saw in the example, this channel is made by multiplexing a channel Csr between the two nodes, using the two process identifiers prs and prr as the multiplexing address, so it is Csr|prs–prr; see Figure 8. A shared key Ksr defines the node-to-node channel Csr = des(Ksr).

Henceforth we concentrate on the integrity of the channels, so we care only that the message comes from the sender, not that it goes to the receiver. Section 4 explains how to establish des(Ksr) Þ rsa(Ks), where Ks is the sending node’s public key. So we can say that the message goes over Cs|prs from the sending process, where Cs = rsa(Ks). Some messages don’t use des(Ksr) but instead are certificates encrypted with Ks because they must be passed on to a third party that doesn’t know Ksr; we indicate this informally by writing Ks says s instead of Cs says s.

The sender wants to communicate one or more statements A says s to the receiver, where A is some principal that the sender can speak for. A single process may speak for several principals, and we express this by multiplexing the channel from the process. Our strategy is to encode A as a number called an authentication identifier or aid, and to pass the aid as an ordinary integer. By convention, the receiver interprets a call like Read(aid, file, ...) as one or more statements Caid says s, where Caid = Cs|prs|aid; this is the channel Cs|prs from the process multiplexed with aid as the subchannel address. The receiving node supplies Cs|prs to the receiver on demand. Recall that Cs is obtained directly from the key used to decrypt the message and prs is supplied by the sending node. The aid is supplied by the sending process. An aid is chosen from a large enough space that it is never reused during the lifetime of the sending node (until the node is rebooted and its Cs changes); this ensures that a channel Caid is never reused.

This design is good because the sending process doesn’t need to tell the operating system about aid in order to send Caid says s to the receiver, since aid is just an integer. The only role of the operating system is to implement the channel Cs|prs securely by labelling each message with the process prs that sends it. Thus a principal is passed as cheaply as an integer, except for a one-time cost that we now consider.

The receiver doesn’t actually care much about Caid ; it wants to interpret the message as A says s for some more meaningful principal A such as a user’s name or public key. To do this, it needs to know Caid Þ A; we call A the meaning of Caid. There are two parts to this: finding out what A is, and getting a proof that Caid Þ A (that is, credentials for A). The receiver gets A and the credentials from the sender. Recall that the credentials consist of some premises C says A´ Þ B´ plus the reasoning that derives Caid Þ A from the premises and the axioms. The channel C on which the sender transmits a premise to the receiver could be either a public key channel or a shared key channel with the receiver as one party, as in the Needham-Schroeder protocol [19]. We treat the former case in detail here. The latter case can arise in two ways. One is that shared key encryption is being used to simulate public key encryption, as described in Section 4. The other is as an optimization when there is already a shared-key channel that speaks for the public key, such as the channel des(Ksr) described just above. This optimization works only for premises that the receiver does not need to forward to a third party.

The meaning A of Caid is an expression whose operands are names or channels; in either case the credentials must prove that the sending system Cs can speak for A. In our system all the operands of A are either roles or the public keys of nodes or of users; in the example of Figure 7 the keys are Kws and Kbwl, and all the names are roles. Sections 6 and 7 explain how the sending system gets credentials for these keys as a result of booting or login. Section 5 explains how the receiving system pulls credentials that authenticate these keys as speaking for named principals.

Thus the credentials are a collection of certificates and statements from the sender, together with the connective tissue that assembles them into a proof of Caid Þ A. The receiver gets them from the sender, checks the proof, and caches the result. In our system a component of the receiver’s operating system called the authentication agent does this work for the receiver.

The process doesn’t need to see the credentials, since it trusts its agent to check them just as it trusts its operating system for virtual memory and the other necessities of life. The process does need to know their lifetime, since the information Caid Þ A that it may want to cache must be refreshed after that time. Figure 9 shows communication through the agent.

Its first job, acting for the receiver, is to maintain a cache of Caid Þ A facts and lifetimes like the cache maintained by its client processes. The agent answers queries out of the cache if it can. Because this is a cache, the agent can discard entries whenever it likes. If the information it needs isn’t in the cache, the receiver’s agent asks the sender’s agent for the meaning and credentials of Caid, checks the credentials it gets back, and caches the meaning.

An authority is an aid that a process speaks for. For a process to have an authority, its agent must have credentials to prove that some channel controlled by the agent speaks for the authority’s meaning, and the agent must agree that the process speaks for the authority. Each process pr starts out with one authority, which it obtains by virtue of a user login or of the program P running in pr. In the latter case, for example, the node N loading P makes a new authority a, tells pr what it is, and records a Þ N as P and pr|a Þ a.

The process can get its initial authority by calling Self(). If it has authorities a and b, it can get the authorities a Ù b by calling And(a, b) and a as r by calling As(a, r). It can give up a by calling Discard(a). What the agent knows about an authority is original information, unlike the cached facts Caid Þ A. Hence the agent must keep it until all the processes that speak for the authority discard it or disappear.

The agent’s third job is to hand off authorities from one process to another, as shown in Figure 10. A sending process can hand off the authority a to another principal b by calling Handoff(a, Cb). This is a statement to its local agent: a says Cb Þ a, where Cb = Cr|prr|b. The agent believes it because of (P10). The process can then pass a to the receiving process by sending it a message in the usual way, say by calling Take(a). If prr has the authority b, it can obtain the authority a by calling Claim(Ca,b). This causes the receiving agent to call the sending agent requesting its credentials for the meaning A of a (proof that Ks|a Þ A) plus the certificate Ks|a says Kr|a Þ A. These are credentials that allow the receiving agent to speak for A. The certificate lets Kr|a speak for A rather than a because the receiver needs to be able to prove its right to speak for the meaningful principal A, not the authentication identifier a. The certificate is directly signed by Ks (the sender’s public key), rather than simply sent on des(Ksr) (the shared key channel between sender and receiver) because the receiver needs something that it can pass on to a third party.

Our system has two procedures for dealing with delegation, one for each of the certificates (1) and (2) in Section 7. A process calls For(a, Cb) to delegate the meaning A of a to the meaning B of the principal Cb; this corresponds to making (1), which in this context is a says Cb|a Þ B for A. Before it calls For, the process normally checks Cb against some acl that expresses the principals to which it is willing to delegate.

Now the process can pass a to a receiver that has an authority b corresponding to Cb, and the receiver calls Accept(a, b) to obtain an authority result that speaks for B for A. This call corresponds to claiming B for A, making (2), which in this context is Cb|a says b|a Þ B for A, and making b|a says result Þ B for A. The sending agent supplies a certificate signed by its public key, Ks|a says Kr|a Þ B for A, along with a’s credentials that prove Ks|a Þ A, just as in an ordinary handoff. The receiving agent can construct credentials for B for A based on the credentials it has for B, the claimed certificate and credentials, and the reasoning in Section 7. So the receiver can prove to others its right to speak for B for A.

Even a seemingly endless chain of remote calls will eventually result in an attempt to actually access an object. For instance, a call Read(file f, authority a) will be interpreted by the receiver as Ca says "read file f ". The receiver obtains the acl for f and wants to know whether Ca speaks for a principal that can have read access. To find this out the receiver calls CheckAccess(f’s acl, Ca, read), which returns true or false. Section 9 explains how this works.

The performance of our interprocess authentication mechanism depends on the cache hit rates and the cost of loading the caches. Each time a receiving node sees Ca for the first time, there is a miss in its cache and a fairly expensive call to the sender for the meaning and credentials. This call takes one rpc time (2.5 ms on our 2 mips processors) plus the time to check any certificates the receiver hasn’t seen before (15 ms per certificate with 512-bit rsa keys). Each time a receiving process sees Ca for the first time, there is one operating system call time and a fast lookup in the agent’s cache. Later the process finds Ca in its own cache, which it can access in a few dozen instructions.

When lifetimes expire, it’s as though the cache was flushed. We typically use 30-minute lifetimes, so we pay less than 0.001% to refresh one certificate. If a node has 50 Ca’s in constant use with two different certificates each, this is 0.1%. With the faster processors coming it will soon be much less.

We take an acl to be a set of principals, each with some rights to the acl’s object. The acl grants a request A says s if A speaks for B and B is a principal on the acl that has all the rights the request needs. So the reference monitor needs an algorithm that will generate a proof of A Þ B (then it grants access), or determine that no such proof exists (then it denies access). This is harder than constructing the credentials for a request, because there we are building up a principal one step at a time and building the proof at the same time. And it is much harder than checking credentials, because theorem proving is much harder than proof checking. So it’s not surprising that we have to restrict the form of acls to get an algorithm that is complete (that is, always finds a proof if there is one) and also runs reasonably fast.

In addition to A and a set of B’s we also have as input a set of premises P Þ Q, where P and Q are properPrincipals or roles. The premises arise from group membership certificates or from path name lookup; they are just like the premises in credentials.

Now there is an efficient algorithm to test A Þ B:

The natural form of denial for us is an acl modifier which means that the access checker should disbelieve a certificate for any principal that satisfies some property. For example, we can disbelieve certificates for a principal with a given name, or one with a given key, or one whose name starts with ‘A’, or one with a given tag (in which case the tags should be unique or we will sometimes deny access improperly). The idea behind this approach is that the system should be fail-secure: in case of doubt it should deny access. This means that it views positive premises like A Þ B skeptically, negative ones like “deny Jim access” trustingly.

Our theory yields a formal proof for every access control decision. The premises in the proof are statements made on channels or assumptions made by the reference monitor (for instance the premise that starts off a name lookup). Every step in the proof is justified by one of a small number of rules, all listed in the appendix. The proof can be written into the audit trail, and it gives a complete account of what access was granted and why. The theory thus provides a formal basis for auditing. Furthermore, we can treat intermediate results of the form A Þ B as lemmas to be proved once and then referenced in other proofs. Thus the audit trail can use storage efficiently.