Trust Domain Model. We have constructed a model, M = {C, Cnew, P, X, α}, for a Trust Domain. This model allows us to reason about the correctness of the Distributed Trust Manager (DTM). One potential side benefit of the model is that it will allow us to identify holes in our design validation and testing of the DTM. The basic components of our model, C, P, X, and α are defined below. C = {c1, c2, c3, ..., cn}, for some finite integer n, is the set of nodes in the Trust Domain. While n could be very large, for practical purposes associated with the implementation of DTM, we will limit n to 16. Cnew = cj | cj C, which is a node that is trying to join a Trust Domain. The state, w, of Cnew is unknown at the time that Xxxx declares its intention to join a Trust Domain. That is, Cnew may be a node whose behavior is in accordance with the Trust Domain admission and security policies (“uncompromised node”) or it may be compromised. α = {α1, α2, α3, ..., αm} is the set of actions that a node may perform. A node is essentially a deterministic finite automaton. Thus, it has a finite set of states, a finite set of input symbols, and a transition function that causes the node to move from some state si to some state sj (si may be sj) based on the input it receives [HM 00]. The transition function is analogous to the set of actions a node may take based on the input the node receives. Since the input alphabet is finite and the number of states is finite, the set of actions, α, which a node may take, is finite. P = {p1, p2, p3, ..., pk} is a security policy, which describes the acceptable behaviors of a computer in the Trust Domain. Each pi is a rule composed of a subject, an object, and an action that the subject may perform on the object. We note that security policies are rarely defined completely, as it is difficult to list every possible rule that is acceptable. Thus, we accept that we will have to add new rules to the policy as new acceptable actions that a computer may perform on an object are discovered. It should be clear that P ⊆ α. We also note that ⌐P U P = α. X is a capability matrix, which indicates what actions the subjects can perform on the objects and/or on each other. The subjects here are the nodes. The objects are the data and the services running on the nodes. X[i][j] = {(n, {αi Є α | ci can perform actions αi to object n on computer cj})}. In other words, for each object n on computer cj, X[i][j] gives the set of actions that computer ci can do to object n on computer...
