Information Technology Reference
In-Depth Information
hierarchy is generally represented pictorially by a Hasse diagram. We implement
Hasse diagrams in HOL as a set
HSD
of pairs, with (
R
1
,R
2
)
HSD
precisely
when there's an explicit edge between
R
1
and
R
2
in the Hasse diagram. It is then
straightforward to define
∈
as the reflexive, transitive closure of
HSD
,relative
to the set
ROLES
of roles:
rhRel HSD ROLES
=
{
(
R
1
,R
2
)
|
(
R
1
∈
ROLES
)
∧
(
R
2
∈
ROLES
)
∧
(
RTC
(
CURRY HSD
)
R
1
R
2
)
}
,
where (
CURRY HSD
)
R
1
R
2
is equivalent to (
R
1
,R
2
)
HSD
and the predicate
RTC
(defined in HOL's
Relation
theory) identifies the elements in the reflexive,
transitive closure of a relation.
For example, the Hasse diagram from Figure 1 can be represented by a set
HSD
as follows:
∈
HSD
=
{
(
Chair, Ten
)
,
(
P&T VM, Ten
)
,
(
Ten, Fac
)
,
(
CS Fac, Fac
)
,
(
CE Fac, Fac
)
,
(
UnTen, Fac
)
}
Letting
ROLES
be the set
{
Chair, P&T VM, Ten, UnTen, CS Fac, CE Fac, Fac
}
,
the inheritance relation
is given by:
rhRel HSD ROLES
=
HSD ∪{
(
R, R
)
| R ∈ ROLES}∪{
(
Chair, Fac
)
,
(
P&T VM, Fac
)
}.
The set of users authorized for a role
R
depends on both the user-role as-
signments (
UA
) and the inheritance relation
; likewise, the set of permissions
associated with a role depends on the permission assignments (
PA
)and
.Thus,
we define predicates
authorized users
and
authorized permissions
as follows:
authorized users R UA HSD ROLES
=
{
R
.
(
R
((
R
,R
)
(
U, R
)
U
|∃
∈
ROLES
)
∧
∈
rhRel HSD ROLES
)
∧
∈
UA
}
,
authorized permissions R PA HSD ROLES
=
{
R
.
(
R
∈
((
R, R
)
(
p, R
)
p
|∃
ROLES
)
∧
∈
rhRel HSD ROLES
)
∧
∈
PA
}
.
It is straightforward to prove that, whenever
R
1
R
2
—that is, when (
R
1
,R
2
)
is in
rhRel HSD ROLES
—the following two properties hold:
(
authorized users R
1
UA HSD ROLES
)
⊆
(
authorized users R
2
UA HSD ROLES
)
(
authorized permissions R
2
PA HSD ROLES
)
⊆
(
authorized permissions R
1
PA HSD ROLES
)
.
As described in Section 2, static separation-of-duty constraints are given by
aset
SSD
: each pair (
rs, n
)
SSD
represents a constraint to prevent users from
being authorized for
n
or more roles in
rs
. Because the set of authorized users
for a given role depends on both the user assignment
and
the role hierarchy,
∈
