Information Technology Reference
In-Depth Information
2.2 Process Algebras
The language of PA is defined by the following grammar:
Parallel processes
Q
::=
0
|
Q P
|
Q
!
P
Sequential processes
P
::=
0
|
a
(
t
)
.P
|
a
(
t
)
.P
|
νx.P
Parallel processes are defined as a parallel composition of, possibly replicated,
sequential processes. These, in turn, are a sequence of commu
ni
cation actions
(input or output) and constant generation. An output process
a
(
t
)
.P
is ready
to send a tuple
t
=(
t
1
,...,t
k
), built over a signature
Σ
, along the polyadic
channel named
a
. An input process
a
(
t
)
.P
is ready to receive a tuple of messages
and match them against the patterns
, possibly binding previously unbound
variables in it. Finally, the creation of a new object in
t
P
(as in the
π
-calculus [23])
is written as
νx.P
. The binders of our language are
νx.
and
a
(
t
), which bind
x
, respectively. This induces the
usual definition of free and bound variables in a term or process. We write
var
(
and any first occurrence of a variable in
t
; no channel name is ever
free. This language is suciently expressive to conveniently formalize immediate
decryption protocols. The general case, which makes use of delayed decryption,
requires an explicit pattern matching operator. A preliminary solution to this
more general problem is presented in [5], while a proper treatment appears in [4].
The operational semantics of PA is given by the following judgments:
t
) for the free symbols occurring in a process
Q
Q ⇒ Q
;
Q ⇒
∗
Q
Single interaction
Iterated interaction
They are defined as follows:
t
[
t
=
θ
]
k ∈
var
(
Q, P
)
t
)
.P
)
Q P P
[
(
Q
a
(
t
)
.P
a
(
⇒
(
θ
])
(
Q νx.P
)
⇒
(
Q P
[
k/x
])
Q ⇒ Q
Q
⇒
∗
Q
Q ⇒
∗
Q
The first inference (
reaction
) shows how two sequential processes, respectively
one ready to perform an output of ground terms
Q ≡ Q
Q
⇒ Q
Q ⇒ Q
Q ⇒
∗
Q
t
, and one ready to perform an
t
react by applying the instantiating substitution
θ
P
.
input over patterns
to
νx
The second rule defines the semantics of
as instantiation with an eigenvari-
able. The next rule allows interactions to happen modulo structural equivalence,
≡
, that in our case contains the usual monoidal equalities of parallel processes
with respect to
and 0, and the unfolding of replication (
i.e.,
,!
P
=!
P P
).
⇒
∗
as the reflexive and transitive closure
Finally, the last two inferences define
of
⇒
.
3 Security Protocols
We now consider sublanguages of MSR and PA (here referred as MSR
P
and
PA
P
) that have gained recent popularity for the specification of cryptographic
