Information Technology Reference
In-Depth Information
channel
holds the information the intruder operates on (it can be either
initial, intercept
e
d, or forged). They are defined as follows:
P
I
1
=
π
(
x
)
.I
(
x
)
.
0
P
I
3
=
N
o
(
x
)
.I
(
x
)
.
0
P
I
5
=
I
(
x
1
,x
2
)
.
I
(
x
1
)
.
0
P
I
5
I
P
I
2
=
νn.I
(
n
)
.
0
P
I
4
=
I
(
x
)
.N
i
(
x
)
.
0
P
I
6
=
I
(
x
1
)
.I
(
x
2
)
.I
(
x
1
,x
2
)
.
0
P
I
8
=
I
(
x
)
.
I
(
k
)
.
I
(
{x}
k
)
.
0
P
I
10
=
I
(
x
)
.I
(
x
)
.I
(
x
)
.
0
Notice that, in our simple calculus, the decomposition of pairs shall be
treated as two projection rules (
=
I
(
x
1
,x
2
)
.I
(
x
2
)
.
0
P
I
7
=
I
(
{y}
k
)
.
I
(
k
)
.
Kp
(
k, k
)
.
I
(
y
)
.
0
P
I
9
=
I
(
x
)
.
0
P
I
5
P
I
5
and
). See [4] for a detailed dis-
cussio
n.
Q
!
π
=
!
0 represents what we called “persistent information” in the case
of MSR
P
. We can assume the same predicate (here channel) names with
the same meaning. This information is made available to client processes on
each channel
π
(
t
)
.
π
(
e.g.,
). It is assumed that no other process performs an
Kp
outp
ut
on
π
.
Q
I
0
=
I
(
t
)
.
0 for some terms
t
.
Q
I
0
represents the initial knowledge of the
intruder.
Q
net
ρ
P
ρ
Q
I
In PA
P
,a
state
is a process of the form
Q
!
where
P
!
net
ρ
Q
!
=(
Q
I
are ground, un-
replicated (
i.e.,
without a ban
g as
a prefix) instances of sequential su
xe
s of
pr
oc
ess
es
!
P
ρ
Q
!
I
Q
!
π
) while
Q
net
,
P
ρ
and
0),
ρ
P
!
ρ
, and
P
!
net
(more precisely
N
o
(
t
)
.
P
!
I
(more precisely
I
(
t
)
.
0
or
I
(
t
)
.
I
(
t
)
.
0).
4 Encodings for Protocol Specifications
This section describes the encodings from MSR
P
to PA
P
and vice versa. As
above, we assume the same underlying signature
Σ
P
. In particular, the predi-
cate symbols and terms in MSR
P
find their counterpart in channel names and
messages in PA
P
, respectively.
The first mapping, from MSR
P
to PA
P
, is based on the observation that
role state predicates force MSR
P
rules to be applied sequentially within a role
(this is not true for general MSR theories [4]). Minor technicalities are involved in
dealing with the presence of multiple instances of a same role (they are addressed
through replicated processes). At its core, the inverse encoding, from PA
P
to
MSR
P
, maps sequential agents to a set of MSR
P
rules corresponding to roles: we
generate appropriate role state predicates in correspondence of the intermediate
stages of each sequential process. The bang operator is not directly involved in
this mapping as it finds its counterpart in the way rewriting rules are applied.
The transformation of the intruder, whose behavior is fixed a priori, is treated
off-line in both directions.
4.1 From MSR
P
to PA
P
=(
˜
˜
˜
Given an MSR
P
configuration (˜
r
:˜
s
), with ˜
r
=(
∪
ρ
(˜
r
ρ
)
,
˜
r
I
) and ˜
s
A,
N,
I,
π
˜
),
Q
net
A
P
A
Q
I
(with
Q
!
=(
P
!
net
ρ
P
!
ρ
we return a PA
P
state
Q
!
