Authentication in Distributed Systems: Theory and Practice Butler Lampson, Martin Abadi, Michael Burrows, and Edward Wobber Summary ------- This paper describes a theoretical model for authentication, based on the notion of principals, and "speaks for" relationships between principals. The authors then use this theory to explain existing and proposed security mechanisms, including a system they developed themselves. Overall System -------------- Assume a security model based on access control as the basis for security policies. This means we have to reason about objects (resources), requests to perform operators on resources, and the entities making requests (principals). A monitor examines requests and decides whether or not to grant it based on who is making the request, and what access controls are placed on the object. Theory of Authentication ------------------------ Based on a few simple concepts: * Principal: A primitive principal can be a person, a computer, a role, or a communication channel. Channels are the only primitives that can speak directly. Principals might also represent groups of other principals. * Compound Principals: A compound principal is one that is built out of principals and operators (relationships between the principals). For example, a principal might assume a particular role (Abadi _as_ Manager), a channel might speak for someone else (C speaks for Lampson), and principals might speak together (Lampson and Wobber). * "Speaks for" relation: The "speaks for" relation formalizes the concept of a level of indirection. When one principal is authorized to represent another principal, it is said that it "speaks for" that other principal. For example, a login shell is authorized to "speak for" its user, and a secure communication channel is authorized to "speak for" the process on the other end of the channel. * Statements: Principals make statements (they "say" things) in order to communicate. When one principal forwards another's statement, we write that "A says B says X". We then use our database of "speaks for" relationships to determine if we believe that B really did "say X". There are a number of axioms in this theory of authentication: (A and B) says s == (A says s) and (B says s) [P1] (A quotes B) says s == A says B says s [P2] (A speaks for B) implies ((A says s) implies (B says s)) [P8] - the definition of "speaks for" relationship Details ------- Channels and encryption: * Essential property of channels is that it's statements can be taken as assumptions in our formal model. * A channel has integrity if we know all possible senders. A channel has secrecy if we know all possible receivers. * Channels must have names, in order for other principals to delegate "speaks for" authority to them. * In their system, use encrypted channels between machines, using public/private key system to ensure secrecy and integrity. Advantage of using public/private keys (as opposed to shared keys) is the ability to generate messages without knowing who is going to receive them. We can simulate this functionality in a shared key system using a trusted relay. Principals and Names: * Principals must be referred to by name, since users can't understand alternatives. But system has to identify based on channels that speak for principals (that speak for principals that ...) Problem is how to identify a channel that speaks for a human-identifiable principal. * Solution is based on a trusted certificate authority (CA) that generates certificates saying a particular principal speaks for some human-named principal. * Problem of naming: We have to scale to many entities, so we use a hierarchical naming scheme. To find a named entity in the hierarchy, we must trust the entities up to the least common ancestor between us and the target. Roles and Programs: * Principals use roles to limit their own authority. When a principal uses a role to do say something, we say "A as R says X", and formally denote 'as' as 'quotes' or 'says'. Two axioms relate to roles: A as R = A|R for all R in A's roles A speaks for A as R for all R in A's roles * We can securely load programs... - A is the OS loading a program P, on behalf of a principal B. - A loads P from the file system, and places it into a process pr. - if a trusts the file system, it just states that "pr speaks for A as P". If it doesn't trust the file system, it can generate a digest D of the program, and use it together with a certificate asserting that a digest D speaks for a program P. * Booting a machine is like securely loading a program. The Delegation: * A principal can delegate only some authority to another principal by first assuming a role, and then handing off it's authority within that role to another. Delegations are revoked using timeouts. * On Login, a user delegates his authority to the workstation W using a similar timeout mechanism. For long-running/batch computations an agent that has power to speak for a user can continue to delegate authority to the batch job as previous delegations expire. Mechanics of authenticating inter-process communication: * The mechanics of identifying and securing channels are handled through agents within the OS. * An agent's job is to cache authentication identifiers of channels, receive data and send data securely, and to hand off authority from one process to another. * There is one agent per machine since the OS/machine is trusted anyway, there is no advantage to having one agent per process. Advantages to having only one agent include: no duplication of code across many programs, agents can optimize common case of communication within a single machine, and key handling is localized to within a single piece of code. Access Control: * An ACL is a set of principals with some rights to an object. The goal is to take a request, a principal making a request, a set of "speaks for" relationships between principles and the ACL to determine whether the request is granted or not. * It is not always possible to reliably deny access to a principal, because principles may have more than one name or key, and certificates are stored in many locations--we may not have found the one certificate granting appropriate authority to a principal. * the formal model presented here generates an audit trail for each access grant. We can follow the theorems, certificates, etc. to determine why a particular request was granted.