Information Technology Reference
In-Depth Information
) or the complement of a channel name (a), we
define the
observations
of process
Let
c
be a channel name (
a
Q
along
c
as the multiset Obs
c
(
Q
)=
{
t
:
c
(
t
)
∈ Q}
.
Definition 2.
Given a multiset of ground atoms
˜
s
and a predicate name
a
,we
define the
projection
of
˜
s
along
a
as the multiset Prj
a
(˜
s
)=
{
t
:
a
(
t
)
∈
s}
˜
.
)
is a configuration, we set Prj
a
(
˜
C
r
s
C
s
If
=(˜
;˜
)=
Prj
a
(˜
)
.
Using Definitions 1 and 2, we make precise what we intend for an MSR
P
configuration and a PA
P
state to be corresponding.
Definition 3.
Given an
MSR
P
configuration
C
and a
PA
P
state
Q
. We say that
C
and
Q
are
corresponding
, written as
CQ
, if and only if the two conditions
hold:
1
.
Prj
N
(
C
)=
Obs
N
o
(
Q
)
2
.
Prj
I
(
C
)=
Obs
I
(
Q
)
Informally
means that the messages that are lying on the net and the
intruder knowledge are the same in configuration
CQ
C
Q
.
On the basis of these concepts, we can now define a correspondence between
MSR
P
configurations and PA
P
states such that, if in MSR
P
is possible to per-
form an action (by applying a rule) that will lead to a new configuration, then
in PA
P
is possible to follow some transitions that will lead in a corresponding
state, and vice versa.
and state
C
Q
Definition 4.
Let
and
be the set of all
MSR
P
configurations and
PA
P
states, respectively. A binary relation
∼⊆C×Q
is a
correspondence
if
(˜
r
:˜
s
)
∼
Q
implies that:
1
.
(˜
r
:˜
s
)
Q
;
s
, then
Q ⇒
∗
Q
and
(˜
s
)
∼ Q
;
2
.
if
˜
r
:˜
s −→
˜
r
:˜
Q ⇒ Q
, then
˜
s −→
∗
˜
s
and
(˜
s
)
∼ Q
.
3
.
if
r
:˜
r
:˜
The following theorems, whose proof can be found in [4], arm that security
protocol specifications written in MSR
P
and PA
P
, and related via the encod-
ings here presented, are corresponding. The treatment of the intruder requires
some care, that, for space reasons, we have partially hidden from the reader by
presenting a slightly simplified translation of
Q
!
I
into ˜
r
I
. Again, all details can
be found in [4].
Theorem 1.
Given an
MSR
P
security protocol theory
C
. Then
C ∼C
.
Theorem 2.
Given an
PA
P
security protocol process
Q
. Then
Q∼Q
.
This means that any step in MSR
P
can be faithfully simulated by zero or more
steps in PA
P
through the mediation of the encoding
, and vice-versa, the
reverse translation
will map steps in PA
P
into corresponding steps in MSR
P
.
