Information Technology Reference
In-Depth Information
◦
α
φ
◦
α
ANI
◦
α
φ
Theorem 1.
α
ρη
ATT
α
ρη
ATT
(
P
)=
(
P
)
iff
(
η
)
P
(
φ
[]
ρ
)
.
α
φ
◦
α
D
.
As far as the narrow case is concerned, we have to check if the possible
executions with the high variable ranging on the whole concrete domain
Note here that the observation abstraction is the composition
V
H
and
the low variables ranging on the set of values with the same property
are equal
to the interference abstraction obtained by setting the high variable to
η
H
)
and the low one to any fixed value in the given property of low variables. This
means that we have to change the interference abstraction given above as follows,
where
C
H
(
V
L
)
L
is a function that uniquely selects an element from sets
C
L
:
℘
(
V
−→
V
of values:
α
NANI
:
℘
(
℘
(
Σ
)
× ℘
(
Σ
))
−→ ℘
(
℘
(
Σ
)
× ℘
(
Σ
))
)=
,l
,S
∈F
∃l ∈
V
L
.f
=
C
H
(
V
H
)
,η
(
l
)
,S
C
H
(
V
H
)
L
η
C
L
(
y ∈
V
)
)
α
NANI
(
F
f
l
=
(
y
)=
η
(
l
Therefore, we can rewrite also narrow abstract non-interference (NANI).
Theorem 2.
α
ρη
ATT
α
ρη
ATT
◦
α
id
(
P
)=
◦
α
NANI
◦
α
id
(
P
)
iff
[
η
]
P
(
ρ
)
.
id
id
3.2
GANI in Concurrency
In [10], the authors introduced a classification of security properties for
security
process algebras
. Since process algebras can be modeled by computational trees,
we show how different security properties defined in [10] can be re-interpreted
as instances of the generalized abstract non-interference. In the following we
consider the process algebra
Spa
introduced in [10]. We only remind the reader
that, if
L ⊆ Act
,then
P \L
can execute all the actions
P
is able to do, provided
that they do not belong to
L
,
P \
I
L
can execute all the actions
P
is able to do,
provided that they do not belong to
L ∩ I
,and
P/L
hides the actions in
L
.
.Westartby
considering NNI (non-deterministic non-interference) which is defined by using
the trace equivalence
Consider a process
P ∈
Spa
, whose computational tree is
{| P |}
P/
H
means that all the action in
H
(high) are hidden, i.e., they are substituted by
the internal action
ε
, while
P \
I
H
means that all the actions in
H
which are
input actions cannot be executed by
P
. Then, we can translate this definition as
GANI. It is clear that the definition of NNI considers the concrete system
P
,this
means that
≈
T
P \
I
H
)
/
H
≈
T
P/
H
,where
in the following way: (
α
OBS
de
=
id
. On the other hand, we have that what an external user
can observe is the system having the high actions hidden. Therefore, we have
to define the attacker abstraction that hides high-level actions. In the following
let
T
Act
be the set of all the semantic trees on the set of actions
Act
, while let
T
L
be the set of all the semantic trees where the private actions are hidden.
Let
τ ∈
T
Act
and consider the following function:
low
:
T
Act
−→
T
L
such that
low
(
τ
) is the tree where any label
σ ∈
H
in
τ
is substituted by
ε
.Let
{| P |}
the semantics of
P
specified as a computational tree. We define the function
)
τ ∈{|P |}
)=
low
(
. This specifies the attacker
α
low
as follows:
α
low
(
{| P |}
τ
abstractioninGANIanditissuchthat:
). Moreover, we
can note that NNI is defined by using trace equivalence, this means that the
{| P/
H
|}
=
α
low
(
{| P |}
