Information Technology Reference
In-Depth Information
if
ϕ
is an instance of a propositional-logic tautology
ϕ
ϕ ⊃ ϕ
ϕ
ϕ
ϕ
P
says
ϕ
(for all
P
)
(
P
says
(
ϕ ⊃ ϕ
))
⊃
(
P
says
ϕ ⊃ P
says
ϕ
)
if
ϕ
a valid formula of the calculus of principals
ϕ
P
says
(
ϕ
1
∧ ϕ
2
)
≡
(
P
says
ϕ
)
∧
(
P
says
ϕ
)
(
P
| Q
)
says
ϕ ≡ P
says
Q
says
ϕ
(for all
ϕ
)
(
P
⇒ Q
)
⊃
((
P
says
ϕ
)
⊃
(
Q
says
ϕ
))
(for all
ϕ ∈ T
)
(
P
T
Q
)
⊃
((
P
says
ϕ
)
⊃
(
Q
says
ϕ
))
Fig. 3.
Logical rules for the derivability predicate
(
Trans)
(
P
T
Q
)
∧
(
Q
T
R
)
⊃
(
P
T
R
)
(for all
T
2
⊆ T
1
)
(
Sub)
(
P
T
1
Q
)
⊃
(
P
T
2
Q
)
(
Mon)
(
P
T
Q
)
⊃
(
R|P
T
R|Q
)
(for every
s ∈ T
)
(Role Del)
(
P
serves
T
Q
)
∧
(
P |Q
says
s
)
⊃
(
P
for
A
Q
says
s
)
(
Ref)
P
T
P
(
Trans)
(
P
T
1
Q
)
∧
(
Q
T
2
R
)
⊃
(
P
T
1
∩T
2
R
)
(for all
T
2
⊆ T
1
)
(Role Sub)
(
Q
1
T
2
Q
2
)
∧
(
P
serves
T
1
Q
1
)
⊃
(
P
serves
T
2
Q
2
)
Fig. 4.
Logical rules related to
T
,
serves
T
,and
T
model role-permission associations, which relate roles (principals) with sets of
permissions (sets of statements).
We can model these RBAC notions in our logic using our three extensions: the
restricted mimicked by
relation, the
restricted serves
relation, and the
restricted
inherits
relation. We explain how to do so in the next section. For now, we
introduce to our logical system some additional rules related to these relations.
These rules (see Figure 4) are all sound with respect to the Kripke semantics.
4
Describing RBAC Policies in the Access-Control Logic
When a user
U
acts in a role
R
and makes a request
q
, a reference monitor makes
an access-control decision based on
UA
and
PA
. The request will be granted if
the user has the right to act in role
R
(i.e.,
U
∈
authorized users
(
R
)) and
q
is a
permission associated with role
R
(i.e.,
q
∈
authorized permissions
(
R
)).
