Information Technology Reference
In-Depth Information
P
net
is fixed a priori (see Section 3.2); (b)
ρ
P
!
ρ
Q
!
I
Q
!
π
)). In particular (a)
and
Q
!
I
, result from the transformation of respectively
∪
ρ
(˜
r
ρ
) and ˜
r
I
; (c)
Q
!
π
, and (d)
A
P
A
results from the transformation of ˜
π
,
Q
net
, and
Q
I
result from
transformation of
˜
,
˜
and
˜
A
N
I
, respectively.
Processes
P
!
ρ
, for each role
ρ
, are obtained via the transformation function
ranging over the set of role rules
∪
ρ
(˜
r
ρ
). We define it depending on the
structure of the role rule
r
ρ
i
∈
r
ρ
involved. Formally for
˜
i
=0:
r
ρ
0
=
˜
π
(
x
)
.ν
n
.r
ρ
1
if
r
ρ
0
:˜
π
(
x
)
→∃
n
.A
ρ
0
(
x
)
,
π
˜
(
x
)
Informally role generation rules are mapped onto a process which first receives,
in sequence, permanent terms via the channels
π
π
in ˜
and then generates all the
n
new names
used along the execution of the protocol.
For 0
<i≤ l
ρ
−
1:
=
N
i
(
t
(
x
))
.r
ρ
i
+2
,
if
r
ρ
i
+1
=
A
ρ
i
(
x
)
→ A
ρ
i
+1
(
x
)
,N
(
t
(
x
))
r
ρ
i
+1
N
o
(
t
(
x
,
y
))
r
ρ
i
+2
,
if
r
ρ
i
+1
=
A
ρ
i
(
x
)
,N
(
t
(
x
,
y
))
→ A
ρ
i
+1
(
x
,
y
)
Finally we have, with a little abuse of notation,
r
ρ
l
ρ
+1
= 0. The final process
de
=
defining the role
ρ
behavior is the following:
P
ρ
r
ρ
0
The intruder is handled by simply mapping ˜
r
I
to
Q
!
I
. More precisely, we
I
define the transformation function
that relates the intruder rewriting rule
r
I
j
P
I
j
r
I
5
with the sequential agents
defined in Section 3.2 (
is mapped to the
pair
). Being the intruder behavior fixed
a priori
, this transformation
is effectively performed off-line once and for all.
At this point the transformation is complete as soon as the state
s
=(
˜
P
I
5
and
P
I
5
˜
˜
A,
N,
I,
˜
π
˜
) is treated. For each
A
ρ
i
(
t
)
∈
A
, we define
P
A
ρ
i
(
t
)
=
r
ρ
i
+1
[
x
/
t
], where
x
are
the variables appearing as argument of
A
i
in
r
ρ
i
+1
.
de
=
N
(
t
)
∈ N
˜
N
Q
net
, that is
Q
net
t
.
The multiset
guides the definition of
N
(
)
0.
de
=
I
(
t
)
∈ I
de
=
π
(
t
)
∈π
Similarly,
Q
I
I
(
t
)
.
0. On the other hand,
Q
!
π
!
π
(
t
)
.
0.
Writing, with a little abuse of notation,
for the generic function that, given
a multiset rewriting MSR
P
configuration returns a PA
P
state, the encoding can
be summarized as:
r
I
:(
˜
˜
˜
(
∪
ρ
(˜
r
ρ
)
,
˜
A,
N,
I,
π
˜
))
=(
P
!
net
P
!
ρ
Q
!
I
Q
!
π
)
(
Q
net
P
A
Q
I
)
ρ
˜
A
4.2 From PA
P
to MSR
P
P
!
net
ρ
P
!
ρ
Q
!
I
Q
!
π
), we show how to construct a configuration in MSR
P
. The basic translation
involves the transformation function
Q
net
ρ
P
ρ
Q
I
Given a PA
P
state
Q
!
with
Q
!
=(
#
(
i
;
)
for the
P
!
ρ
's (called as a subroutine
by the top level transformation
) which, given a sequential agent representing
a role
ρ
, returns the multiset of rules ˜
r
ρ
. Here
i
is an non-negative integer.
Formally:
