Information Technology Reference
In-Depth Information
In
SBAC
(
ψ
), variables are denoted by using upper case symbols, and con-
stants will be denoted by lower case symbols. We use
U
,
O
,
P
,
A
,
L
,
E
, and
T
as variables that range over the sets of values in the domains
U
,
O
,
P
,
A
,
L
,
E
,
and
T
, respectively. To distinguish between variables that range over a domain
V
,weuse
V
1,
V
2,
...
As
SBAC
(
ψ
) is a locally stratified logic program, it follows that the
well-
founded semantics
[12] may be used for the declarative semantics for
SBAC
(
ψ
).
, where
V
is one of
U
,
O
,
P
,
A
,
L
,
E
,
T
Proposition 1.
Every locally stratified program has a unique, 2-valued well-
founded model [12].
Corollary 1.
SBAC
(
ψ
)
has a unique, 2-valued well-founded model [12].
Proof.
Follows immediately from Proposition 1 and the fact that every
SBAC
program is locally stratified.
Remark 1.
Having a categorical semantics for
SBAC
policies is important be-
cause it implies that authorizations are unambiguously defined.
Remark 2.
Henceforth, we use
WFM
(
SBAC
(
ψ
)) to denote the well-founded
model of
SBAC
(
ψ
).
In addition to the fixed set of terms that we admit in
SBAC
(
ψ
), we allow a
small number of fixed predicates too (see below). Despite the restrictions imposed
on our policy specification language, the language permits a range of access
control policies to be specified for protecting network systems.
3 The Status-Based Access Control (SBAC) Model
In this section, we describe the key components of our
SBAC
model. The
SBAC
model includes means for specifying that:
1. a requesting agent is assigned to a status level
l
(
l
∈L
).
2. a permission is associated with a status level
l
.
3. a denial is associated with a status level
l
.
A specification of 1 is a
status-level assignment
, a specification of 2 is a
permission-level association
, and a specification of 3 is a
denial-level association
.
The
SBAC
model includes a number of hierarchies for implicitly defining
authorizations. Due to space restrictions we only consider status level hierarchies
in this paper. A status level hierarchy is a partial order on status levels.
An
SBAC
status level hierarchy is represented by using an
SBAC
pro-
gram
ψ
that defines a
SUBSUMES
L
relation (
SUBSUMES
L
⊆L×L
). The
SUBSUMES
L
l
i
,l
j
relation comprises all pairs of status levels
such that
l
i
SUBSUMES
L
l
j
,SUBSUMES
L
).
The
SUBSUMES
L
relation is represented in
SBAC
(
ψ
) by using a 2-place
predicate
subsumes
L
with the intended meaning:
holds in the partial order (
L
