Information Technology Reference
In-Depth Information
Active environment
. The active environment also is an intruder. It reads all
message outputs of protocol participants, and can output any message which it
generates to any protocol participant that allows for honest message passing,
redirecting messages, replaying messages, and inventing new messages. The in-
truder can also be a legitimate protocol participant. In our model we are only
interested in the active environment's message capability, and describe the mes-
sages the active environment posses as
EM
.Welet
EM
0
stand for the active
environment's initial messages.
2.2 The Syntax of GSPM
In order define GSPM we need the syntactic sets defined below:
-
N
: an infinite set of names, ranged over by
n, m, k, Id, Id
1
···
.A
name is plaintext, participant's name, nonce, key, or atomic name variable
etc.; A key k is either public key (
Pub
N
), or a private key (
Prv
N
), or a
shared/secret key (
SecKey
).
-
Variables over messages
ϕ, ψ, ψ
,ψ
1
,
,x,x
1
,
···
···
.
-
{
.
}
k
represents symmetric encryption,
{
.
}
+
k
represents asymmetric encryp-
tion,
{
.
}
−k
represents asymmetric decryption.
M
::=
N
|
ϕ
|
(
M
1
,M
2
)
|{
M
}
k
|{
M
}
+
k
|
H
(
M
)
Message expr.
}
−k
Pattern expr.
The grammar for processes is similar to that of the pi calculus, except that
here messages may contain terms (rather than only names) and that the notion
of channel is absent:
P, Q, R
::=
Patt
::=
M
|
?
x
|
?
ϕ
|
(
Patt
1
,Patt
2
)
|{
Patt
}
k
|{
Patt
process
0
null process
in
(
patt
(
x ϕ
))
.P
message input
out
(
newxM
)
.P
message output
Q
parallel composition
In the above definition
x
for example abbreviates some possibly empty list
x
1
,
P
|
,x
l
. An informal explanation of the GSPM is similar to the one in [6].
The null process
0
does nothing;
in
(
patt
(
x ϕ
))
.P
awaits an input that matches
the pattern for some binding of the pattern variables
x ϕ
and resumes as
P
under
this binding. Here
patt
(
x ϕ
) represents that there may be some variables
x ϕ
in
the pattern.
out
(
newxM
)
.P
chooses fresh, distinct names
n
=
n
1
,
···
···
,n
l
and
binds them to the variables
x
=
x
1
,
,x
l
. Then the message
M
[
n/x
] is output
to the network and the process resumes as
P
[
n/x
]. The communication is asyn-
chronous in the sense that the action of output does not await input. The
new
construct is like that of Pitts and Stark [15] and abstracts out an important
property of a value chosen randomly from some large set.
Furthermore we extend processes with the location to agent:
A, B, C
::=
···
Agents
Id
[
P, IM
]
e t
Id
performs
P
with
IM
A
B
parallel composition
