Information Technology Reference
In-Depth Information
In this case, properties we are interested in are called relativized properties
and are defined as subsets of (
φ
(
H
L
))
ω
,where
φ
is the abstraction
function. The first component represents the past, and the second one the future.
A property
P
is a
past property
(resp.
future property
)if
P
=
R
L
))
∗
×
∪
(
φ
(
H
∪
L
)
ω
)
×
φ
((
H
∪
L
)
ω
)).
We state the definition of information flow in this relativized situation.
Let
u
L
)
∗
)
L
)
∗
)(resp.
R
(resp.
P
=
φ
((
H
∪
×
R
)where
R
⊂
φ
((
H
∪
⊂
φ
((
H
∪
∈
L
+
with
B
(
u
)
∅
. For a relativized property
P
we define
Pr
S
(
P, u
)=
=
Pr
S
(
)
/Pr
S
(
B
(
u
)).
The event
{γ ∈ Tr | γ
=
γ
1
γ
2
,γ
1
|
L
=
u, last
(
γ
1
)=
last
(
u
)
,
(
γ
1
,γ
2
)
∈ P }
corresponds to the situation when the low-level user observes
u
and the last
action which occurred is a low-level action. We assume that
P
is well-behaved
such that this event is a measurable set for every
u
{
γ
∈
Tr
|
γ
=
γ
1
γ
2
,γ
1
|
L
=
u, last
(
γ
1
)=
last
(
u
)
,
(
γ
1
,γ
2
)
∈
P
}
L
+
.
We can give now a definition of relativized information flow:
Definition 5.
AsystemS is without relativized information flow for a rela-
tivized property P of abstraction level φ if for every u, v
∈
L
+
such that B
S
(
u
)
∈
and B
S
(
v
)
are nonempty, Pr
S
(
P, u
)=
Pr
S
(
P, v
)
.
Definition 6.
A system is without relativized information flow for a given ab-
straction level if it is without relativized information flow for all relativized prop-
erties of this level.
Again, one can use different levels of abstraction depending on the type of the
events whose occurrence is of interest. For instance, consider the high-level event
sequence
xy
, and assume one wishes to express that it occurs without any low-
level event intervening after the last event of the low-level observation
u
.Thiscan
be expressed by the sequential relative property (
H
)
ω
.(A
sequential property is needed to express the fact that
x
and
y
are not separated
by low-level events). If now one of the interesting events (say
y
) is low-level, we
need a general relative property so the identity of
y
is not abstracted away. For
instance, (
H
)
∗
×
H
∗
xy
(
H
∪{
l
}
∪{
l
}
L
)
ω
expresses that
xy
will occur with two
intervening events after the last low-level event of the given observation.
Theorem 3.
The only systems such that Tr
L
)
∗
×
L
)
2
xy
(
H
∪
(
H
∪
∪
H
ω
which are without relativized
general information flow are those which have a projection on L equal to τ
ω
.
Proof.
Suppose that the projection of
Tr
on
L
is equal to
τ
ω
, then the only
finite sequences
u
⊂
=
such that
B
(
u
) is non-empty are
τ
n
,n>
0, and in that
case
Pr
S
(
P, τ
n
)=
Pr
S
(
P, τ
m
) for all positive integers
m, n
for every relativized
general property
P
. We conclude that the system
S
has no relativized general
information flow.
Conversely, suppose that the projection of
Tr
on
L
contains a trace
w
=
τ
ω
.
Then the first action
a
of
w
is different from
τ
,otherwise
w
would be equal
to
τ
ω
. Consider the property
P
=
E
∗
×
E
ω
.
We have
Pr
S
(
P, a
)
>
0and
Pr
S
(
P, τ
) = 0. Therefore
S
has a relativized general infor-
mation flow.
{
(
γ
1
a, γ
2
)
∈
|
γ
1
|L
=
}
The next theorem characterizes the systems without relativized sequential
information flow. Recall that in this case the abstraction function
φ
collapses all
the low-level actions into a single one, the action
l
.
