Elements of system: s_{i} ∈ S subjects,
o_{i} ∈ O objects
State space V = B × M × F ×
H where: B set of current accesses (i.e., access modes each subject has
currently to each object); M access permission matrix; F consists of 3 functions: f_{s} is security level
associated with each subject, f_{o} security level
associated with each object, and f_{c} current security
level for each subject; H hierarchy of system objects, functions h:
O→P(O) with two properties:
If o_{i} ≠ o_{j}, then
h(o_{i}) ∩
h(o_{i}) = ∅
There is no set
{ o_{1}, …, o_{k} } ⊆ O
such that for each i, o_{i+1}
∈ h(o_{i}) and
o_{k+1} = o_{1}
Set of requests is R
Set of decisions is D
W = R × D × V ×
V is motion from one state to another
System Σ(R, D, W, z_{0})
⊆ X × Y × Z such that
(x, y, z) ∈ Σ(R,
D, W, z_{0}) iff
(x_{t}, y_{t},
z_{t}, z_{t−1})
∈ W for each t ∈ T; latter is an
action of system
Theorem: Σ(R, D, W, z_{0})
satisfies the simple security condition for any initial state
z_{0} that satisfies the simple security
condition iff W satisfies the following conditions for
each action (r, d,
(b′, m′, f′,
h′), (b, m, f, h)):
each (s, o, x) ∈
b′ − b satisfies the simple
security condition relative to f′ (i.e.,
x is not read, or x is read and
f_{s}(s) domf_{o}(o)); and
if (s, o, x) ∈ b does not
satisfy the simple security condition relative to
f′, then (s, o, x) ∉
b′
Theorem: Σ(R, D, W, z_{0})
satisfies the *-property relative to S′ ⊆
S for any initial state z_{0} that
satisfies the *-property relative to S′ iff
W satisfies the following conditions for each
(r, d, (b′,
m′, f′, h′), (b,
m, f, h)):
for each s ∈ S′, any (s,
o, x) ∈ b′ − b
satisfies the *-property with respect to f′;
and
for each s ∈ S′, if (s,
o, x) ∈ b does not satisfy the
*-property with respect to f′, then
(s, o, x) ∉ b′
Theorem: Σ(R, D, W, z_{0})
satisfies the ds-property iff the initial state
z_{0} satisfies the ds-property and W
satisfies the following conditions for each
(r, d, (b′,
m′, f′, h′), (b,
m, f, h)):
if (s, o, x) ∈ b′
− b, then x ∈
m′[s, o]; and
if (s, o, x) ∈ b and
x ∈ m′[s, o], then
(s, o, x) ∉ b′
Basic Security Theorem: A system Σ(R, D,
W, z_{0}) is secure iff z_{0}
is a secure state and W satisfies the conditions of the above
three theorems for each action.