Beyond Proof-of-compliance: Security Analysis in Trust Management

Beyond Proof-of-compliance: Security Analysis in
Trust Management
NINGHUI LI
Purdue University
JOHN C. MITCHELL
Stanford University
and
WILLIAM H. WINSBOROUGH
George Mason University
Trust management is a form of distributed access control that allows one principal to delegate
some access decisions to other principals. While this makes trust management more flexible than
the access matrix model, it makes safety and security analysis more important. We show that in
contrast to the undecidability of classical HRU safety properties, our primary security properties
are decidable. In particular, most safety properties we study are decidable in polynomial time.
The computational complexity of containment analysis, the most complicated security property
we study, forms a complexity hierarchy based on the expressive power of the trust management
language.
Categories and Subject Descriptors: K.6.5 [Management of Computing and Information Systems]: Secu-
rity and Protection; D.4.6 [Operating Systems]: Security and Protection — Access Controls; F.2.2 [Analysis
of Algorithms and Problem Complexity]: Nonnumerical Algorithms and Problems — Complexity of proof
procedures
General Terms: Security, Theory, Languages
Additional Key Words and Phrases: access control, trust management, distributed system security,
logic programs
1.
INTRODUCTION
Access control techniques, which govern whether one party can access resources and ob-
jects controlled by another party, are useful in protecting the confidentiality, integrity, and
availability of information. Traditional access control schemes make authorization deci-
sions based on the identity of the requester. However, in decentralized or multicentric
environments, the resource owner and the requester often are unknown to one another,
making access control based on identity ineffective. For example, although a certificate
authority may assert that the requester’s name is John Q. Smith, if this name is unknown to
A preliminary version of this paper appeared in Proceedings of 2003 IEEE Symposium on Security and Privacy
under the title “Beyond proof-of-compliance: Safety and availability analysis in trust management”. Most of this
work was performed while the first author was at the Department of Computer Science, Stanford University in
Stanford, CA 94305, and the third author was at Network Associates Laboratories in Rockville, MD 20850.
Authors’ addresses: Ninghui Li, Department of Computer Sciences, Purdue University, 656 Oval Drive, West
Lafayette, IN 47907-2086, USA; email: ninghui@cs.purdue.edu. John C. Mitchell, Department of Com-
puter Science, Gates 4B, Stanford, CA 94305-9045, USA; email: mitchell@cs.stanford.edu. William
H. Winsborough, Center for Secure Information Systems, George Mason University, Fairfax, VA 22030-4444,
USA; email: wwinsborough@acm.org.

---

2
·
the access mediator, the name itself does not aid in making an authorization decision. What
is needed is information about the rights, qualifications, responsibilities and other charac-
teristics assigned to John Q. Smith by one or more authorities, as well as trust information
about the authorities themselves.
Trust management [Blaze et al. 1996; Blaze et al. 1999a; 1999b; Rivest and Lampson
1996; Ellison et al. 1999; Clarke et al. 2001; Gunter and Jim 2000; Jim 2001; Li et al. 2003;
Li et al. 2003; Li et al. 2002; Li and Mitchell 2003; Weeks 2001] is an approach to access
control in decentralized distributed systems with access control decisions based on policy
statements made by multiple principals. In trust management systems, statements that are
maintained in a distributed manner are often digitally signed to ensure their authenticity
and integrity; such statements are called credentials or certificates. A key aspect of trust
management is delegation: a principal may transfer limited authority over one or more
resources to other principals. While the use of delegation greatly enhances flexibility and
scalability, it may also reduce the control that a principal has over the resources it owns.
Since delegation gives a certain degree of control to a principal that may be only partially
trusted, a natural security concern is whether a resource owner nonetheless has some guar-
antees about who can access their resources. If we think of the union of all policies of all
principals as the state of a TM system, then a state may change as the result of a single step
that adds or removes a policy statement, or as the result of a finite sequence of such steps.
A resource owner generally has control over some part of the state, but cannot control all
possible changes. In this paper, we consider the security analysis problem, which asks
what accesses may be allowed or prevented by prospective changes in the state of a TM
system.
A few definitions are useful for stating the security analysis problem more precisely. In
general, a TM language has a syntax for specifying policy statements and queries, together
with an entailment relation . We call a set P of policy statements a state of a TM system.
Given a state P and a query Q, the relation P
Q means that Q is true in P. When
Q arises from an access request, P
Q means that access Q is allowed in P; a proof
demonstrating P
Q is then called a proof-of-compliance.
Recognizing that a principal or a coalition of cooperating principals may control only
a part of the global state, we assume there is a restriction rule, R, that defines how states
may be changed. For example, the principal in question may consider the part of the state
controlled by fully trusted principals to be fixed, while considering that other principals
may remove some policy statements and/or add new ones. Given a state P and a restriction
∗
rule R, we write P →R P if the change from P to P is allowed by R, and P →R P
∗
if a sequence of zero or more allowed changes leads from P to P . If P →R P , we say
that P is R-reachable from P , or simply P is reachable, when P and R are clear from
context.
DEFINITION 1. Let P be a state, R a restriction rule, and Q a query. Existential se-
∗
curity analysis takes the form: Does there exist P such that P →R P and P
Q?
When the answer is affirmative, we say Q is possible given P and R. Universal security
∗
analysis takes the form: For every P such that P →R P , does P
Q? If so, we say Q
is necessary given P and R.
Here are some motivating examples of security analysis problems.
Simple Safety. (Existential) Does there exist a reachable state in which a specific (pre-

---

·
3
sumably untrusted) principal has access to a given resource?
Simple Availability. (Universal) In every reachable state, does a specific (presumably
trusted) principal have access to a given resource?
Bounded Safety. (Universal) In every reachable state, is the set of all principals that have
access to a given resource bounded by a given set of principals?
Liveness. (Existential) Does there exist a reachable state in which no principal has ac-
cess to a given resource?
Mutual Exclusion. (Universal) In every reachable state, are two given properties (or two
given resources) mutually exclusive, i.e., no principal has both properties (or access to both
resources) at the same time?
Containment. (Universal) In every reachable state, does every principal that has one
property (e.g., has access to a resource) also have another property (e.g., is an employee)?
Containment can express safety or availability (e.g., by interchanging the two example
properties in the previous sentence).
Simple safety analysis was first formalized by Harrison et al. [Harrison et al. 1976] in
the context of the well-known access matrix model [Lampson 1971; Graham and Den-
ning 1972]. Simple safety analysis was referred to as safety analysis since other analysis
problems were not considered. The model in [Harrison et al. 1976] is commonly known
as the HRU model. In the general HRU model, safety analysis is undecidable [Harrison
et al. 1976]. A number of protection models were developed to make safety analysis more
tractable. Lipton and Snyder introduced the take-grant model [Lipton and Snyder 1977],
in which simple safety can be decided in linear time. Sandhu introduced the Schematic
Protection Model [Sandhu 1988], and the Typed Access Matrix model [Sandhu 1992]. In
these previous works, only simple safety analysis are considered; the other kinds of analy-
sis listed above were not. Since some of the analysis problems are about properties other
than safety (e.g., availability), we use the term security analysis rather than safety analysis.
To the best of our knowledge, security analysis for TM systems has not been investigated
previously as such. In this paper, we define a precise model for security analysis in trust
management. The policy languages we consider are languages in the RT family of Role-
based Trust-management languages [Li et al. 2003; Li et al. 2002; Li and Mitchell 2003].
The RT family combines the strengths of Role-Based Access Control (RBAC) [Sandhu
et al. 1996] and previous trust-management (TM) systems. Semantics for the RT family
is defined by translating each statement into a logic programming clause. In this paper,
we consider four languages in the RT family; they are denoted by RT[ ], RT[∩], RT[
],
and RT[
, ∩]. RT[ ] is the most basic language in the family; it has two types of state-
ments: simple member and simple inclusion. RT[∩] adds to RT[ ] intersection inclusion
statements. RT[
] adds to RT[ ] linking inclusion statements, which can be used to express
attribute-based delegation. RT[
, ∩] has both intersection inclusion and linking inclusion;
RT[
, ∩] is a slightly simplified (yet expressively equivalent) version of the RT0 language
described in [Li et al. 2003].
All the security analysis problems listed above are considered. While the TM language
we are studying supports delegation and is more expressive than the access matrix model
in certain ways, and the kinds of analysis problems we consider are more general, some-
what surprisingly, they are decidable. Simple safety, simple availability, bounded safety,
liveness, and mutual exclusion analysis for RT[
, ∩] (and hence for the other three sub-

---

4
·
languages of RT[
, ∩]) can all be answered in time polynomial in the size of the state
P. These analysis problems are answered by evaluating queries against logic programs
derived from the state P and the restriction rule R.
Containment analysis is the most interesting case, both in terms of usefulness and in
terms of technical challenge. The computational complexity of containment analysis de-
pends on the language features. In RT[ ], the most basic language, containment analysis is
in P. Containment analysis become more complex when additional policy language fea-
tures are used. Containment analysis is coNP-complete for RT[∩], PSPACE-complete
for RT[
], and decidable in coNEXP for RT[ , ∩]. These complexity properties are
proved using techniques and results from logic programming, formal languages, and au-
tomata theory. For RT[ ], we use logic programs derived from P and R to do containment
analysis. These logic programs use negation-as-failure in a stratified manner [Apt et al.
1988]. For RT[∩], we show that containment analysis is essentially equivalent to determin-
ing validity of propositional logic formulas. The RT[
] language is expressively equiv-
alent to SDSI (Simple Distributed Security Infrastructure) [Rivest and Lampson 1996;
Clarke et al. 2001], and is related to a class of string rewriting systems modelled using
pushdown systems [Bouajjani et al. 1997]. We show that containment analysis in RT[
]
can be reduced to determining containment among reachable configurations of pushdown
systems, which is again reduced to determining containment of languages accepted by
Nondeterministic Finite Automata (NFAs). For the case of RT[
, ∩], we show that if a
containment does not hold, then there must exist a counter-example state (i.e., a reachable
state in which the containment does not hold) of size at most exponential in the size of the
input.
The rest of this paper is organized as follows. In Section 2, we define the model we use
to study security analysis in TM. In Section 3, we handle simple safety, simple availability,
liveness, and mutual exclusion. In Section 4, we present results about containment analy-
sis. We discuss related work in Section 5, and conclude in Section 6. An appendix contains
proofs that are not included in the main body.
2.
A CONCRETE SECURITY ANALYSIS PROBLEM
The abstract definition of security analysis in Definition 1 has three parameters: the lan-
guage used to express the state P, and the form of query Q and the form of restriction
rule R. In this section, we define concrete security analysis problems by supplying these
parameters, discuss our choices, give an example that will be used throughout the paper,
and discuss how security analysis can be used in practical situations to achieve security
objectives.
2.1
Syntax of The TM Language
The policy languages we consider are in the RT family of Role-based Trust-management
languages. More specifically, we consider RT[
, ∩] and its three sub-languages: RT[ ],
RT[
], and RT[∩]. The basic constructs of RT[ , ∩] include principals and role names.
In this paper, we use A, B, D, E, F , X, Y , and Z, sometimes with subscripts, to denote
principals. A role name is a word over some given standard alphabet. We use r, u, and
w, sometimes with subscripts, to denote role names. A role takes the form of a principal
followed by a role name, separated by a dot, e.g., A.r and X.u. A role defines a set of
principals that are members of this role. Each principal A has the authority to designate
the members of each role of the form A.r. An access control permission is represented as

---

·
5
a role as well; for example, that B is a member of the role of A.r may represent that B has
the permission to do action r on the object A.
There are four types of policy statements in RT[
, ∩], each corresponding to a different
way of defining role membership:
—
Simple Member:
A.r ←− D
This statement means that A asserts that D is a member of A’s r role. We read “←−” as
“includes”.
—
Simple Inclusion:
A.r ←− B.r1
This statement means that A asserts that its r role includes (all members of) B’s r1 role.
This represents a delegation from A to B, since B may affect who is a member of the
role A.r by issuing statements about B.r1.
—
Linking Inclusion:
A.r ←− A.r1.r2
We call A.r1.r2 a linked role. This statement means that A asserts that A.r includes
B.r2 for every B that is a member of A.r1. This represents a delegation from A to all
the members of the role A.r1.
—
Intersection Inclusion:
A.r ←− B1.r1 ∩ B2.r2
We call B1.r1 ∩ B2.r2 an intersection. This statement means that A asserts that A.r
includes every principal who is a member of both B1.r1 and B2.r2. This represents
partial delegations from A to B1 and to B2.
A role expression is a principal, a role, a linked role, or an intersection. We say that each
policy statement defines the role A.r. Given a set P of policy statements, we define the
following: Principals(P) is the set of principals in P, Names(P) is the set of role names
in P, and Roles(P) = {A.r | A ∈ Principals(P), r ∈ Names(P)}. RT[
, ∩] is a slightly
simplified (yet expressively equivalent) version of RT0 [Li et al. 2003]. 1 In this paper,
we also consider the following sub-languages of RT[
, ∩]: RT[ ] has only simple member
and simple inclusion statements, RT[
] adds to RT[ ] linking inclusion statements, and
RT[∩] adds to RT[ ] intersection inclusion statements.
The four types of statements in RT[
, ∩] cover the most common delegation relation-
ships in other TM languages such as SPKI/SDSI [Ellison et al. 1999; Clarke et al. 2001]
and KeyNote [Blaze et al. 1999a]. The sub-language RT[
] can be viewed as a simpli-
fied yet expressively equivalent version of SDSI. SDSI allows long linked names, which,
as observed in [Li et al. 2003], can be broken up by introducing new role names and
statements. With the exception of thresholds, the delegation relationships (though, not the
s-expression-based representation of permission) in SPKI’s 5-tuples, can be captured by
using simple member statements and a restricted form of simple inclusion statements. A
SPKI 5-tuple in which A delegates a permission r to B can be represented as A.r ←− B.
A SPKI 5-tuple in which A delegates r to B and allows B to further delegate r can be
represented as two RT[
, ∩] statements: A.r ←− B and A.r ←− B.r. Similar analogies
can be drawn for KeyNote.
Although RT[
, ∩] is limited in that role names are constants, extending role names in
RT[
, ∩] to have internal structures does not change the nature of security analysis. As we
1 RT[ , ∩] simplifies RT0 in that intersection inclusion statements in RT[ , ∩] allow the intersection of only
two roles; in RT0, the intersection may contain k components, each can be a principal, a role, or a linked
role. RT0 statements using such intersections can be equivalently expressed in RT[
, ∩] by introducing new
intermediate roles and additional statements. This simplification helps simplify the proofs in this paper.

---

6
·
will see, security analysis is mostly affected by the structure of the delegation relationships.
We believe that many results and techniques developed for RT[
, ∩] can be carried over
to more expressive languages, e.g., RT1 [Li et al. 2002], which adds to RT0 the ability to
have parameterized roles, RT C
1 [Li and Mitchell 2003], which further adds constraints to
RT1, and, to a certain extent, SPKI/SDSI and KeyNote.
The security analysis problem for RT[
, ∩] involves new concepts and techniques. Se-
mantics and inference for SDSI, which is essentially the sub-language RT[
], has been
extensively studied [Abadi 1998; Clarke et al. 2001; Halpern and van der Meyden 2001;
Jha and Reps 2002; Li 2000; Li et al. 2003]. Some of these studies only consider answering
queries in a fixed state. Some consider universal analysis where no restriction is placed on
how the state may grow [Abadi 1998; Halpern and van der Meyden 2001]. However, the
most interesting aspect of security analysis, answering queries when restrictions are placed
on state changes, has not been addressed in the previous studies.
2.2
Semantics of the TM Language
We give a formal characterization of the meaning of a set P of policy statements by trans-
lating each policy statement into a datalog clause. (Datalog is a restricted form of logic
programming (LP) with variables, predicates, and constants, but without function sym-
bols.) We call the resulting program the semantic program of P. We use the LP-based
approach to define semantics because we will formulate safety computation rules by using
a similar approach, and the LP-based approach generalizes easily to the case in which role
names contain parameters (see [Li et al. 2002]).
DEFINITION 2 SEMANTIC PROGRAM. Given a set P of policy statements, the seman-
tic program, SP (P), of P, has one ternary predicate m. Intuitively, m(A, r, D) means that
D is a member of the role A.r. The program SP (P) is the set of all datalog clauses pro-
duced from policy statements in P as follows, where symbols that start with “?” represent
logical variables:
For each A.r ←− D in P, add
m(A, r, D)
(m1)
For each A.r ←− B.r1 in P, add
m(A, r, ?Z) : − m(B, r1, ?Z)
(m2)
For each A.r ←− A.r1.r2 in P, add
m(A, r, ?Z) : − m(A, r1, ?Y ), m(?Y, r2, ?Z) (m3)
For each A.r ←− B1.r1 ∩ B2.r2 in P, add
m(A, r, ?Z) : − m(B1, r1, ?Z), m(B2, r2, ?Z) (m4)
In general, a datalog program is a set of datalog clauses. Given a datalog program, DP,
its semantics can be defined through several equivalent approaches. The model-theoretic
approach views DP as a set of first-order sentences and uses the minimal Herbrand model
as the semantics. We write SP (P) |= m(X, u, Z) when m(X, u, Z) is in the minimal Her-
brand model of SP (P). This semantics corresponds exactly to the set-theoretic semantics
of RT0 in [Li et al. 2003].
We now summarize a standard fixpoint characterization of the minimal Herbrand model,
which we will use in the proofs in this paper. Given a datalog program DP, let DPinst
be the ground instantiation of DP using constants in DP; the immediate consequence
operator, TDP , is defined as follows. Given a set K of ground logical atoms, TDP (K)

---

·
7
consists of all logical atoms, a, such that a : − b1, . . . , bn ∈ DPinst, where n ≥ 0, and
either n = 0 or bj ∈ K for 1 ≤ j ≤ n. The least fixpoint of TDP is given by
∞
TDP↑ω=
TDP↑i, where TDP↑0= ∅ and TDP↑i+1= TDP (TDP↑i), i ≥ 0
i=0
The sequence TDP ↑i is an increasing sequence of subsets of a finite set. Thus there
exists an N such that TDP (TDP ↑N ) = TDP ↑N. TDP ↑ω is identical to the minimal
Herbrand model of DP [Lloyd 1987]; therefore, SP (P) |= m(X, u, Z) if and only if
m(X, u, Z) ∈ TSP(P)↑ω.
It has been shown that the minimal Herbrand model of DP can be computed in time
linear in the size of DPinst [Dowling and Gallier 1984]. If the total size of DP is M , then
there are O(M ) constants in DP. Assuming that the number of variables in each clause is
bounded by a constant, v, the number of instances of each clause is therefore O(M v), so
the size of DPinst is O(M v+1). Thus, the worst-case complexity of evaluating SP (P) is
O(|P|3), since |SP (P)| = O(|P|) and each rule in SP (P) has at most two variables.
2.3
Restriction Rules on State Changes
Before discussing how we model restrictions on changes in policy state, we consider one
motivating scenario. Additional discussion of ways that security analysis can be used in
practical situations appears in Section 2.6. Suppose that the users within an organization
control certain principals, and that these principals delegate partial control to principals
outside the organization. In this situation, roles defined by principals within the organi-
zation can be viewed as unchanging, since the analysis will be repeated before any future
candidate change is made to those roles. Roles defined by principals outside the organi-
zation, however, may change in arbitrary ways, since they are beyond the organization’s
control. By using security analysis, the organization can ensure that delegations to princi-
pals outside the organization do not violate desired security properties, which are specified
by a collection of security analysis problem instances and the correct answers to them.
To model control over roles, we use restriction rules of the form R = (GR, SR), which
consist of a pair of finite sets of roles. (In the rest of the paper we drop the subscripts from
G and S, as R is clear from context.)
—Roles in G are called growth-restricted (or g-restricted); no policy statements defin-
ing these roles can be added. Roles not in G are called growth-unrestricted (or g-
unrestricted).
—Roles in S are called shrink-restricted (or s-restricted); policy statements defining these
roles cannot be removed. Roles not in S are called shrink-unrestricted (or s-unrestricted).
One example of R is (∅, ∅), under which every role is g/s-unrestricted, i.e., both g-
unrestricted and s-unrestricted. Another example is R = (∅, Roles(P)), i.e., every role
may grow without restriction, and no statement defining roles in Roles(P) can be removed.
This models the case of having incomplete knowledge of a fixed policy state. A third
example, corresponding to the scenario discussed above, is R = (G, S), where G = S =
{X.u | X ∈ {X1, . . . , Xk}, u ∈ Names(P)}, i.e., X1, . . . , Xk are trusted (controlled);
therefore, every role X.u such that X ∈ {X1, . . . , Xk} is restricted, all other roles are
unrestricted. If a principal X does not appear in R, then for every role name r, by definition

---

8
·
X.r is g/s-unrestricted. This models the fact that the roles of unknown principals may be
defined arbitrarily.
We allow some roles controlled by one principal to be g-restricted while other roles
controlled by the same principal may be g-unrestricted. This provides more flexibility
than simply identifying principals as trusted and untrusted, and permits one in practice to
perform security analysis only when changing certain roles. Similarly, we allow a role
to be both g-restricted and s-unrestricted, which has the effect of making a safety check
necessary when modifying the definition of the role only if adding a new statement.
These restrictions are static in the sense that whether or not a state-change step is allowed
by R does not depend on the current state. A dynamic restriction could, for instance, have
B.r2 be g-restricted if B is a member of A.r1, which depends on the current state. Security
analysis with dynamic restrictions is potentially interesting future work.
2.4
Queries
In this paper, we consider the following three forms of query Q:
—
Membership:
A.r
{D1, . . . , Dn}
Intuitively, this means that all the principals D1, . . . , Dn are members of A.r. Formally,
P
A.r
{D1, . . . , Dn} if and only if {Z | SP(P) |= m(A, r, Z)} ⊇ {D1, . . . , Dn}.
—
Boundedness:
{D1, . . . , Dn}
A.r
Intuitively, this means that the member set of A.r is bounded by the given set of prin-
cipals. Formally, P
A.r
{D1, . . . , Dn} if and only if {D1, . . . , Dn} ⊇ {Z |
SP (P) |= m(A, r, Z)}.
—
Inclusion:
X.u
A.r
Intuitively, this means that all the members of A.r are also members of X.u. Formally,
P
X.u
A.r if and only if {Z | SP (P) |= m(X, u, Z)} ⊇ {Z | SP (P) |=
m(A, r, Z)}.
A membership query A.r
{D1, . . . , Dn} can be translated to an inclusion query
A.r
B.u, in which B.u is a new role, by adding B.u ←− D1, . . . , B.u ←− Dn to
P and making B.u g/s-restricted. Similarly, boundedness queries can be translated to
inclusion queries as well. We include membership and bounded queries because they can
be answered more efficiently.
Each form of query can be generalized to allow compound role expressions that use
linking and intersection. However, these generalized queries can be reduced to the forms
above by adding new roles and statements to the policy. For instance, {}
A.r ∩ A1.r1.r2
can be answered by adding B.u1 ←− A.r ∩ B.u2, B.u2 ←− B.u3.r2, and B.u3 ←− A1.r1
to P, in which B.u1, B.u2, and B.u3 are new g/s-restricted roles, and by posing the query
{}
B.u1.
The three forms of queries can be varied to consider cardinality of roles rather than exact
memberships. A cardinality variant of membership queries has the form “|A.r| ≥ n”,
which means that the number of principals who are members of A.r is no less than n. A
cardinality variant of boundedness queries has the form “n ≥ |A.r|”. Cardinality variants
of membership and boundedness queries can be answered similarly to the base queries. We
do not consider a cardinality variant of inclusion queries in this paper.

---

·
9
2.5
An Example
EXAMPLE 1. The system administrator of a company, SA, controls access to some
resource, which we abstractly denote by SA.access. The company policy is the following:
managers always have access to the resource, managers can delegate the access to other
principals, but only to employees of the company. HRU is trusted for defining employees
and managers. The state P consists of the following statements:
SA.access ←− SA.manager
SA.access ←− SA.delegatedAccess ∩ HR.employee
SA.manager ←− HR.manager
SA.delegatedAccess ←− SA.manager.access
HR.employee ←− HR.manager
HR.employee ←− HR.programmer
HR.manager ←− Alice
HR.programmer ←− Bob
HR.programmer ←− Carl
Alice.access ←− Bob
Given the state P above, Alice and Bob have access, Carl does not. One possible restric-
tion rule has G = { SA.access, SA.manager, SA.delegatedAccess, HR.employee } and S
= { SA.access, SA.manager, SA.delegatedAccess, HR.employee, HR.manager }. We now
list some example analysis problem instances, together with the answers:
Simply safety analysis:
Is “SA.access
{Eve}” possible?
(Yes.)
Simple availability analysis:
Is “SA.access
{Alice}” necessary?
(Yes.)
Bounded safety analysis:
Is “{Alice, Bob}
SA.access” necessary.
(No.)
Containment analysis:
Is “HR.employee
SA.access” necessary?
(Yes.)
2.6
Usage of Security Analysis
Security analysis provides a means to ensure that safety and availability requirements are
met and will continue to be met after policy changes are made by autonomous authorities.
Security analysis is also useful when the global state of a TM system is fixed, but only
partially known. For instance, previously unknown statements may be presented along
with new access requests. Thus, although the global state does not change, one’s view
of that state is changing. Thus there are many reasons why an individual or organization
using a TM system may be unable to determine a fixed state of that system. Whatever that
reason, security analysis techniques can be used to ensure that basic safety and availability
requirements are not violated by prospective changes one is considering making, before
putting those changes into effect. Let us make this more concrete.
A security analysis problem instance is given by a state P, a query Q, a quantifier for the
query (universal or existential), and a restriction rule R. Basic security requirements can
be formalized as security analysis problem instances, together with answers to them that
are acceptable for secure operation. For instance, one safety requirement might be formal-
ized as asking whether anyone outside the organization can access a particular confidential
resource, in which case the acceptable answer would be “no.” Once a policy state has
been established that leads the analysis to produce no unacceptable answers, if prospective
changes to g/s-restricted roles result in any unacceptable answers, the changes are con-
sidered to be in violation of the corresponding requirement, and should not be applied.

---

10
·
By definition of the analysis, changes to g/s-unrestricted roles cannot cause unacceptable
answers when starting from a policy state that gives none.
One possible usage scenario for this approach is as follows. An organization’s Sys-
tem Security Officer (SSO) writes a restriction rule restricting change of some of the roles
that are under the control of principals in the organization, as well as a set of analysis-
instance/acceptable-answer pairs. The SSO then uses these pairs and obtains the assistance
of principals within the organization to bring the current policy into compliance. This is
done by changing the policy as needed to make the analysis yield acceptable answers for
all the analysis instances. If this cannot be done, the requirements are inconsistent or out-
side the organization’s control, and must be revised. Once the policy has been brought into
compliance, principals that control restricted roles are trusted to ensure that subsequent
changes to such roles do not lead to unacceptable answers. By restricting only roles con-
trolled within the organization, the SSO may be able to rely on software enforcement and
other means to ensure that this trust is justified.
In the above usage, the SSO determines an analysis configuration consisting of a set
of analysis-instance/acceptable-answer pairs and a restriction rule. In general, many such
configurations can be used, each specified by a different interested party having a differ-
ent set of principals it is willing to trust to run the analysis and to enforce the analysis-
instance/acceptable-answer pairs, and hence having a different restriction rule.
It is significant to note that the usage pattern we are suggesting enables the enforce-
ment of requirements that cannot be enforced by constructs in RT[
, ∩], or most other
trust management languages. This is because those languages are monotonic in the sense
that policies with more statements derive more role membership facts. By contrast, many
of the requirements expressible using analysis-instance/acceptable-answer pairs are anti-
monotonic, in the sense that adding statements to a policy that satisfies such a requirement
can yield a policy that does not. Thus there is no way to enforce such a requirement within
the language itself. This is illustrated by the example of mutual exclusion of two roles.
Monotonicity makes it impossible to express within RT[
, ∩] that a principal cannot be
added to both roles. However this is easily prevented through the usage pattern described
above.
3.
ANSWERING MEMBERSHIP AND BOUNDEDNESS QUERIES
Monotonicity properties of logic programming allow us to derive efficient algorithms for
membership and boundedness queries. First, RT[
, ∩] and its sub-languages are mono-
tonic in the sense that more statements will derive more role membership facts. This fol-
lows from the fact that the semantic program is a positive logic program. Second, mem-
bership queries are monotonic; given a membership query Q, if P
Q, then for every
P such that P ⊆ P , P
Q. Third, boundedness queries are anti-monotonic; given a
boundedness query Q, if P
Q, then for every P such that P ⊆ P, P
Q.
Intuitively, universal membership (simple availability) analysis and existential bound-
edness (liveness) analysis can be answered by considering the set of principals that are
members of a role in every reachable state. We call this set the lower bound of a role.
Because the restriction R is static, there exists a minimal state that is reachable from P
and R. This is obtained from P by removing all statements defining s-unrestricted roles.
We denote this state by P|R. Clearly, P|R is reachable; furthermore, P|R ⊆ P for ev-
ery reachable P . Since RT[
, ∩] is monotonic, one can compute the lower bound by

---