Information Technology Reference
In-Depth Information
protocols (see for example [2,17]). Narrowing our investigation to a specific do-
main will allow us to directly compare these restricted versions of MSR and PA.
The two specifications will rely on a common first-order signature
Σ
P
that in-
cludes at least concatenation (
,
) and encryption (
{ }
). In both formalisms
terms in
Σ
P
stand for messages. Predicate symbols are interpreted as such in
MSR
P
, and as channel names in PA
P
. Variables will also be allowed in rules and
processes.
3.1 Protocols as Multiset Rewriting
MSR
P
relies on the following predicate symbols [8]:
Network Messages (
˜
N
):
are the predicates used to model the network, where
N
(
t
) means that the term
t
is lying on the network.
Role States (
˜
A
):
are the predicates used to model roles. Assuming a set of
role identifiers
R
{A
ρ
i
(
t
i
...l
ρ
}
, the family of
role state predicates
):
=0
,is
intended to hold the internal state,
during the
sequence of protocol steps. The behavior of each role
ρ
is described through
a finite number of rules, indexed from 0 to
t
, of a principal in role
ρ ∈ R
l
ρ
.
Intruder (
˜
I
):
are the predicates used to model the intruder
I
, where
I
(
t
),
means that the intruder knows the message
t
.
Persistent Predicates (
˜
):
are ground predicates holding data that does not
change during the unfolding of the protocol (
e.g.,
π
K, K
) indicates that
(
Kp
K
form a pair of public/private keys). Rules use these predicates to
access the value of persistent data.
K
and
A security protocol is expressed in MSR
P
as a set of rewrite rules ˜
r
ofaspe-
cific format called a
security protocol theory
. Given roles
R
, it can be partitioned
as ˜
r
=
∪
ρ∈R
(˜
r
ρ
)
,
r
I
, where ˜
˜
r
ρ
and ˜
r
I
describe the behavior of a role
ρ ∈ R
and
of the intruder
I
. For each role
ρ
, the rules in ˜
r
ρ
consist of:
-
one
instantiation rule
r
ρ
0
:˜
π
(
x
)
→∃
n
.A
ρ
0
(
n
,
x
)
,
π
˜
(
x
)
-
zero or more (
i
=1
...l
ρ
)
message exchange rules
:
send
r
ρ
i
:
A
ρ
i
−
1
(
x
)
→
A
ρ
i
(
x
)
,N
(
t
(
x
))
receive
r
ρ
i
:
A
ρ
i
−
1
(
x
)
,N
(
t
(
x
,
y
))
→
A
ρ
i
(
x
,
y
)
Notice that, differently from [5] where delayed decryption protocols are handled,
the role state predicates are restricted to having only variables as their argu-
ments. The notation
t
(
z
) is meant to indicate that the variables appearing in
term
) from the very last rule.
It should be observed that the form of these rules does not allow representing
protocols that receive an encrypted message component and only at a later stage
are given the key to decrypt it. This case requires a more complicated treatment,
which is presented in [5] and fully analyzed in [4]. The simplified study analyzed
here should not be dismissed, however, since the majority of the protocols studied
in the literature do not manifest the above behavior.
t
are drawn from
z
. We can safely elide
A
ρ
l
ρ
(
x
