Information Technology Reference
In-Depth Information
#
(1;(
x
,
n
))
.ν
n
.P
ρ
}∪P
ρ
˜
π
(
x
)
=
{
˜
π
(
x
)
→∃
n
.A
ρ
0
(
n
,
x
)
#
(
i
;
x
)
#
(
i
+1;(
x
,
y
))
.P
ρ
}∪P
ρ
N
o
(
t
(
y
))
=
{A
ρi−
1
(
x
)
,N
(
t
(
x
,
y
))
→ A
ρi
(
x
,
y
)
#
(
#
(
.P
ρ
}∪P
ρ
N
i
(
t
)
=
{A
ρi−
1
(
x
)
→ A
ρi
(
x
)
,N
(
t
)
i
;
x
)
i
+1;
x
)
#
(
i
;
x
)
0
=
·
in
ρ
P
ρ
Let
P
!
ρ
be the role specification of which an object
P
ρ
is an instanti-
ated sux and
θ
=[
x
/
t
] the witnessing substitution. If
P
ρ
starts with either a
persistent input
π
(
x
)orthe
ν
operator, we set
P
ρ
=
·
. Otherwise, let
i
be the
index at which
P
ρ
occurs in
P
!
ρ
as for the above definition. Then
P
ρ
=
A
ρi
(
t
).
The intruder process
Q
!
I
is roughly handled by the inverse of the transforma-
tion
I
, wh
ic
h we call
I
(s
e
e [4
]
for a more detailed and rigorous treatment).
Each object
I
(
t
)
.
0 (resp., the
I
(
t
)
.
I
(
t
)
.
0) in
Q
I
is rendered as the state element
I
t
I
t
,I
t
(
) (resp., pair of elements
(
)
(
)).
P
!
net
t
.
P
net
disappears. Instead, each occurrence of a process
N
o
(
)
0in
is
mapped to a state element
N
(
t
). Similarly, each process !
π
(
x
)in
P
!
π
is translated
into the state object
π
(
x
).
It is easy to prove that
and
are inverse of each other:
Lemma 1.
1. For any
MSR
P
C
C
C
configuration
, we have that
=
.
2. For any
PA
P
stat
e
Q
,
w
e have
t
hat
Q
=
Q
modulo the extension of
≡
with the equation a
(
t
)
.
a
(
t
)
.
0=
a
(
t
)
.
0
a
(
t
)
.
0
.
A detailed proof of this result, including the treatment of details that have been
omitted here for space reasons, can be found in [4].
5 Correspondence
In this section, we will call an MSR
P
configuration and a PA
P
state
correspond-
ing
when they manifest the same network and intruder behavior, step by step.
This will allow us to prove that the translations presented in this paper are
reachability-preserving in a very strong sense. We invite the reader to consult [4]
for a more comprehensive and detailed discussion of this matter.
We first formalize the notion of transition step and observation in each for-
malism.
α
→
Definition 1.
Given a process
Q
, the notation
Q
indicates that
α
is the
multiset of communication events that the process
Q
may perform in a next step
of execution. Formally:
α
→
α
→
Q
P
0
·
·
→
)
α,α
a
(
t
)
→
a
(
t
)
→
→
νn.P
(
Q P
→
t
.P
t
.P
a
(
)
a
(
)
α
→}
.
We write
α ∈ P
if
α ∈{α
:
P
