Information Technology Reference
In-Depth Information
The rest of this subsection will give a deeper insight into the abstract system
model.
Message space
. The message space we used for the analysis of security pro-
tocols is as follows:
k
::=
Public key
|
Private key
|
Symmetric key
Keys
a
::=
k
|
Nonces
|
Plaintext
Atomic messages
M
::=
a
|
M.M
|{
M
}
k
|
Hash
(
M
)
Messages
Plaintexts, nonces and keys are atomic messages. The other messages are com-
posite. Like in [16] we have rules defining how messages may be generated from
existing ones. We write
M
to mean that the message
M
may be derived
from the finite set of messages
M
M
. The following rules define the generated
relation
:
M
∈M
=
⇒M
M
(1)
M
M
1
∧M
M
2
=
⇒M
M
1
.M
2
(2)
M
M
1
.M
2
=
⇒M
M
1
∧M
M
2
(3)
M
M
∧M
k
=
⇒M{
M
}
k
(4)
M{
M
}
Publickey
∧M
privatekey
=
⇒M
M
(5)
M{
M
}
Symmetrickey
∧M
Symmetrickey
=
⇒M
M
(6)
M
M
=
⇒M
Hash
(
M
)
(7)
Let
el
(
M
) be the set of the elements of the message base
M
. We can obtain
the
el
(
) by iteration as follows:
Do while
M
M
is not empty, we get a message
M
from
M
(1) When
M
is atomic message, we put
M
into
el
(
M
);
(2) When
M
=
M
1
.M
2
, we put
M
1
and
M
2
into
M
;
M
1
}
k
,if
k
−
1
and
k
−
1
)(
k
−
1
is the
k
's correspond-
(3) When
M
=
{
∈M
∈
el
(
M
ing key) then we put
M
into
el
(
M
)elseweput
M
1
into
M
.
Enddo.
M
is a message base, and
M
is a message, then
M
M
is
Theorem 1.
Let
decidable.
Proof.
It can be proved by induction on the structure of message.
(1) If
M
is atomic message or hash message, then
M
M
only when
M
∈
el
(
M
);
(2) If
M
=
M
1
.M
2
,then
M
M
only when
el
(
M
)
M
1
and
el
(
M
)
M
2
.
(3) If
M
=
{
M
1
}
k
,then
M
M
only when
M
∈
el
(
M
)or
M
k
and
el
(
M
)
M
1
.
Protocol participants
. For each protocol participant there are a set of pro-
cesses and a message base
IM
. Each process of a participant corresponds to
an instance of the participant involved in a particular execution of the proto-
col. All the processes work asynchronously and concurrently. The concurrency
is simulated by non-deterministic interleaving of process running.
