Information Technology Reference
In-Depth Information
(1)
∀
n>
0
Tr
n
=
H
n
(
Tr
)
⊗
L
n
(
Tr
)
.
(2)
n>
0
, all nodes of red depth n with outgoing red edges are equivalent
(3) For every H-equivalent nodes x, x
of T
(
S
)
, the probabilistic trees T
x
and T
x
are isomorphic.
∀
The proof of this theorem is based on the lemma given below which links
sequential relativized information flow at each fixed step with sequential rela-
tivized information flow. Then we can reuse the proof of Theorem 1.
E
be a sequential property on traces where R
l
)
∗
and
Lemma 1.
Let R
⊂
(
H
∪
E
=(
H
l
)
ω
l
)
∗
τ
ω
∪
∪
(
H
∪
.Then,forP
R
=
{
(
γ
1
,γ
2
)
||
γ
1
|
L
|
=
n, last
(
γ
1
)=
E
}
E
|
l, γ
1
γ
2
∈
R
, for every u of length n we have Pr
S
(
P
R
,u
)=
Pr
S
(
R
B
(
u
))
.
5
Comparison with Some Classical Security Properties
L
)
∗
τ
ω
,
In this section we restrict ourselves to finite systems, for which
Tr
⊆
(
H
∪
and we suppose that
τ
.
We identify an element of
Tr
with its shortest prefix ending with the action
τ
.
Given a trace
λ
and a system
S
, the low-level user observing
λ
|L
0
τ
can construct
the set of system traces which correspond to the same observation, the
low-level
equivalent set
[18] of
λ
:
For
λ
∈
L
.Denoteby
E
0
the set
H
∪
L
0
,where
L
0
=
L
\{
τ
}
E
0
{
.
We will show that
separability
,
noninterference
and
noninference
can be ex-
pressed in our framework and correspond to the absence of information flow for
some classes of properties.
∈
τ
}
,
LLES
(
λ, S
)=
{
β
∈
Tr
|
λ
|L
0
=
β
|L
0
}
1. Noninference
Noninference
is a security property which was introduced by O'Halloran [14].
It requires that every trace
λ
of the system admits in its low-level equivalent set
its projection
λ
|L
0
. As a consequence a low-level user cannot deduce from an
observation the existence of any occurrence of a high-level action:
Noninference
(
S
)
L
0
τ
.
≡∀
λ
∈
Tr
∃
u
∈
LLES
(
λ, S
)
u
∈
L
0
)
∗
τ
. A trace satisfies this
property iff it does not contain high-level actions. Thus this property exactly
focuses on the (non) existence of a high-level activity. It turns out that
nonin-
ference
canbeexpressedintermsofinformationflowfortheproperty
NonInf
.
Consider the property
NonInf
=
L
0
τ
⊂
(
H
∪
Theorem 6.
For
a
probabilistic
system
S,
Noninference
(
S
)
holds
iff
Pr
S
(
NonInf
)
=0
and there is no qualitative general information flow for the
property NonInf .
Proof.
= 0 and there is no qualitative general in-
formation flow for the property
NonInf
.Let
λ
be a trace
Suppose
Pr
S
(
NonInf
)
∈
Tr
. Consider the
projection
u
=
λ
|L
.Since
B
(
u
)isnon-empty,
Pr
S
(
NonInf
)
=0andthereis
no qualitative general information flow for the property
NonInf
.Sowehave
Pr
S
(
NonInf ,u
)
=0.Itprovesthat
u
∈
Tr
because
B
(
u
)
∩
NonInf
=
{
u
}
.Thus,
Noninference
(
S
)istrue.
