Authentication in Distributed Systems: Theory and Practice 
--- (Butler Lampson, Martín Abadi, Michael Burrows, Edward Wobber)

[68] This is an extremely dense paper describing a detailed theory for
authentication and its practical applications.

Principals are the main acting entities in this authentication theory.
Principals can request actions. Actions are performed on objects (resources
such as files, devices, processes, etc.). The objective of this work is to
provide a language in which rules may be defined, according to which
requests by a principal on an object are granted or not. Rules are attached
to the objects they govern. A reference monitor decides whether to allow a
specific action, taking under consideration the involved objects with their
associated access rules, principals and requests.

The job of the reference monitor is non-trivial, especially in distributed
systems, since it must make logical inferences leading it to a decision. For
example, principals almost never directly attempt an action on an object
themselves, since principals are humans and objects are bits; most usually,
a principal utilizes a channel, such as a network connection, a pipe or a
function call (e.g., to access object X, Alice, a principal, types on a
keyboard, which is attached to a system K, connected through a TCP pipe P to
another system L, where object X lives. The reference monitor on system L
sees an action attempted by a process Z on object X.) Channels are
principals, too; however, they're more than that, because they can request
things directly inside a computer, whereas human principals can't.

The reference monitor must decide whether the immediate channel attempting
an action is trusted at least as much as the principal mentioned in the
access rule for an object. In the example above, if X specifies in a rule
that it will accept all actions from Alice, then the reference monitor must
decide whether process Z is at least as trustworthy as principal Alice. To
do that, it has to reason about Z, L, P, K and Alice.

Trust can be bestowed or transfered by a principal on another principal. For
example, I may trust my brother to do anything that I can do. To prove my
trust, I give my brother a legally binding document, such as a power of
attorney. This provable trust is represented in the authentication theory
described in this paper by the ``speaks for'' relation. When A speaks for B,
A can do at least as much as B can do (i.e., if a request should be granted
for B, then it should also be granted for A). Since only channels can say
things directly inside a computer, invariably human principals must have
channels that speak for them, so that they can communicate their requests
through a computer system.

In a distributed system, where many components from different devices
conspire to see a request through to its destination, it is inevitable to
place different levels of trust in the reliability or the loyalty of every
single component. A well-designed authentication system relies for its
security only on few trusted components, its Trusted Computing Base, or TCB;
in other words, no component outside the TCB should be allowed to affect the
security of the system by misbehaving. Furthermore, the system is
fail-secure when it is conservative in the face of failure: when it gives
the wrong answer, it always denies a request it should have granted, never
the other way around.

2.73.1 Theory and Concepts

To connect principals to other principals, define statements, etc., the
following constructs are possible:

Speaks for
     [$A\Rightarrow B$] means that if A does something, it is exactly as if
     B had done the same thing. [$A\Rightarrow B$] is a statement.

Quoting
     A|B means that A says that B does something. A is quoting B as doing or
     saying something. Keep in mind that A might be lying (so B might not in
     fact do what A quotes B as doing). A|B is a compound principal.

Says
     (A:s) is a statement, representing the fact that A says statement s, or
     A is entitled to claim s. A may or may not have uttered s, but we can
     proceed as though A actually has. In other words, as far as A is
     concerned, given his knowledge and capabilities, s holds true.

Aggregation
     [$s\wedge t$] is a compound sentence, consisting of both s and t.
     Similarly [$A\wedge B$] is a compound principal, consisting of both A
     and B.

Some basic, intuitive axioms or inference rules using the above constructs
are defined in the paper, including modus ponens, distribution and
monotonicity over [$\Rightarrow$] of ``says'' over [$\wedge$] and so on.

2.73.2 Handoff

One of the primary tools in this theory is the ability to express delegation
of authority. A principal can utter a statement that allows another
principal (most commonly, a channel) to speak for it. The main handoff rule
is

[\begin{displaymath}(A:(B\Rightarrow A)) implies (B\Rightarrow A)\end{displaymath}]

The handoff rule can be expressed even more powerfully (without asserting
more), by making the initiator of the handoff be a principal who just speaks
for the owner of the handed off authority, i.e.,

[\begin{displaymath}((A\RightarrowB)\wedge(A:(C\Rightarrow B))) implies (C\Rightarrow B)\end{displaymath}]

2.73.3 Encrypted Channels

Encrypted channels are very powerful. They allow the untrusted, arbitrary
handling of messages, without compromizing the contents' secrecy or
integrity, through public key cryptography. Even if existing public-key
cryptographic algorithms turn out to be insecure or too expensive,
shared-key cryptography can be used to simulate public-key functionality.
Therefore, even with a small TCB, a sane authentication model can be built
using encryption.

Given that a computer node is trusted as a whole (including its operating
system and administration), the first step to building secure end-to-end
channels, for use in the authentication scheme described, is to build secure
channels from node to node. A single node-to-node secure channel between any
two nodes is sufficient, since the theory allows multiplexing over a single
channel. The node-to-node scheme must allow rekeying (since encryption keys
must change regularly).

The authors present the following mechanism to establish secure node-to-node
channels (from A's view point; B does the symmetric). It is assumed that
both A and B have their own node key-pair, which has been assigned to the
node by a certification authority, and their own boot key pair, computed
when the node boots up.

   * A sends its own public boot key to B (Ka).

   * A computes a random symmetric key (Ja) and sends it to B encrypted with
     B's public key Kb, i.e securely ( [$\{J_a\}^{K_b}$]).

   * A puts together the two symmetric keys (Ja, which it just made up, and
     Jb, which it received from B) and creates a new symmetric key K to use
     in its secure node-to-node channel with B. Instead of concatenating the
     two, it uses a one-way hash function on the concatenation, to avoid
     known-plaintext attacks. The new key is K = h(Ja, Jb).

     Up to this point, A and B can communicate using K, up until they have
     to change keys, or one of them dies. However, to be able to talk about
     this channel, they have to name the key they're using (so that, for
     example, innocent or malicious replays may be identified). To create an
     identifier for this newly created key, they take the next step.

   * A encrypts K with a secret, private master key KaM and sends it to B.
     This is A's identifier for K. Together A's and B's identifiers for K
     define this secure channel between A and B completely. Note that any
     arbitrary way of creating an identifier for K (with minimal conflicts)
     would also do.

After this exchange, A knows that [$K\Rightarrow K_b$], i.e., everything
that arrives encrypted by K can be safely trusted as much as anything that
could arrive encrypted by Kb-1. Since Ka and Kb are not used by the actual
channel, they can remain in use for much longer (as long as the system stay
up in this case) and still, the channel bears their trust.

To extend the chain of trust a little bit further, we need to show that
someone ``meaningful'' sits behind Ka. That can be done by connecting the
A's node key to Ka. Remember that Kan bears a certificate that
[$K_{an}\Rightarrow A$], for the ``meaningful principal'' A. Now, if node A
can present something like [$K_a\Rightarrow K_{an}$] (for example, sign Ka
with Kan-1), then Ka can be trusted as much as Kan, or transitively, A.