Information Technology Reference
In-Depth Information
a false session with
B
. The attack involves two interleaved executions of the
protocol, one in which the intruder
I
acts as the responder and one in which it
acts as the initiator.
Theorem 2.
The NSPK protocol does not satisfy the authentication and Con-
fidentiality properties. There exists a path
s
don't such that
A
[
out
(
{
N
BA
}
Pub
B
)]
←
B
[
out
(
{
Bauth.AbyN
BA
}
)]
thus
C
0
|
=
A
[
out
(
{
N
BY
}
Pub
B
)]
←
B
[
out
(
{
Bauth.AbyN
BY
}
)]
don't hold. i.e.
B
can not authenticate
A
by the correspondence assertion; and
s
N
BA
, i.e. the protocol does not satisfy the confidentiality property.
Proof.
We know
EM
0
=
{
Pub
A
,Pub
B
,Pub
I
,Prv
I
}
.
C
0
generates the path
s
=
α
1
···
α
8
,where:
α
1
=
A
[
out
(
{N
AI
,A}
Pub
I
)]
α
2
=
B
[
in
(
{
N
AI
,A
}
Pub
B
)]
α
3
=
B
[
out
(
{
N
AI
,N
BA
}
Pub
A
)]
α
4
=
A
[
in
(
{
N
AI
,N
BA
}
Pub
A
)]
α
5
=
A
[
out
(
{
Aauth.IbyN
AI
}
)]
α
6
=
A
[
out
(
{
N
BA
}
Pub
I
)]
α
7
=
B
[
in
(
{
N
BA
}
Pub
B
)]
α
8
=
B
[
out
(
{
Bauth.AbyN
BA
}
)]
It is clearly that the path
s
do not satisfy
A
[
out
(
{
N
BA
}
Pub
B
)]
←
B
[
out
(
{
B
auth. A by N
BA
}
N
BA
. Thus the protocol does not
satisfy the authentication and Confidentiality properties.
)], and (
msg
(
s
)
∪
EM
0
)
5
Conclusion and Further Work
In this paper we present a generic model (GSPM) for security protocols that
allows one to reason about formal definitions of a variety of security properties.
In GSPM one does not explicitly model intruders. We have formulated security
properties such as confidentiality, authentication, non-repudiation, fairness, and
anonymity in GSPM. We have taken the Needham-Schroeder public-key proto-
col as a case study to demonstrate the expressive power of GSPM. We plan to
construct an automatic tool to help analyzing the security protocol using GSPM.
However we have to consider the following questions:
1. The active environment possesses infinite messages. Since the protocol
participant must receive the matched messages, we are ready to take into account
the symbolic method.
