Information Technology Reference
In-Depth Information
Table 1.
Mapping from RBAC to Access-Control Logic
RBAC
Access-Control Logic
A permission
q
is associated with role
R
p ∈ ap
(
R
)
U
serves
RA
User
U
is authorized to act in role
R
.
ap
(
R
)
R
Role
R
1
inherits role
R
2
(
R
1
R
2
)
R
1
ap
(
R
2
)
R
2
User
U
asserting role
R
makes a request
q
.
U|R
says
q
User
U
, acting in authorized role
R
, makes a request
q
.
U
for
RA
R
says
q
From above, we know that (
Chair
{rsg,rt}
Ten
)
∧
(
Ten
{rsg}
Fac
). Role
transitivity allows us to conclude
Chair
{rsg}
Fac
. Taken together with
Alice
serves
RA
{rsg,rt}
Chair,
Figure 4's role-subsumption rule (Role Sub) lets us deduce
Alice
serves
RA
{rsg}
Fac
.
Fac
says
rsg
and
Alice
serves
RA
{
Fac
, we can use the Figure 4's
role-delegation rule (Role Del) to deduce (
Alice
for
RA
Fac
)
says
rsg
as needed. As
aresult,
Alice
's request can be granted.
From
Alice
|
rsg
}
4.5 Summary
Table 1 summarizes how RBAC concepts are translated into formulas of the
access-control logic, providing a guideline for describing RBAC policies in the
logic. The logical rules in Figure 4 provide the basis for reasoning about access-
control decisions. Specifically, to determine whether a request
U
R
says
q
should
be granted, it suces to determine whether the statement (
U
for
RA
R
)
says
q
can
be deduced from the logical rules.
|
5
Formal Specifications of RBAC Constraints
RBAC's separation-of-duty constraints do not directly affect access-control de-
cisions, in that they are not checked at the time a decision is made. Rather, they
impose additional restrictions on the initial specification of an RBAC policy.
Therefore, we have not incorporated them into our access-control logic. However,
it is desirable to be able to verify that a given policy is consistent: its user-role
assignment and role hierarchy should not conflict with the stated separation-of-
duty constraints.
For this reason, we have formalized RBAC constraints in the Higher-Order
Logic (HOL) theorem prover. The result is a tool which one can verify the con-
sistency of RBAC policies. Because the access-control logic has also been imple-
mented and proved sound in HOL, we can easily convert RBAC policies which
has been proved consistent in HOL into the access-control logic for reasoning
about access-control decisions.
5.1 Static Separation of Duty
The role-inheritance relationship between roles
R
1
and
R
2
(
R
1
R
2
)isapar-
tial order and thus reflexive, transitive, and antisymmetric. In RBAC, the role
