Information Technology Reference
In-Depth Information
4AnExamp e
We consider the Needham-Schroeder public-key protocol. This protocol aims
to establish mutual authentication between an initiator
A
and a responder
B
,
and share with the secret nonces. Every participant
Id
has a private key
Prv
Id
and a corresponding public key
Pub
Id
. We will write
}
k
for the message
m
encrypted with the key
k
. Any participant can encrypt a message
m
using
A
's
public key
Pub
A
{
m
}
Pub
A
;only
A
can decrypt this message. The
protocol also uses nonces: random numbers generated with the purpose of being
used in a single run of the protocol. We denote nonces by
N
AX
and
N
BY
:the
subscripts are intended to denote that the nonces were generated by
A
and
B
are
sent to
X
and
Y
, respectively. The complete protocol involves seven steps. Here
we consider a simplified version with only three steps. This version is related to
the assumption that each agent initially has the other's public key. The simplified
protocol can be described as:
to produce
{
m
1.
A
−→
B
:
{
N
AB
,A
}
Pub
B
2.
B
−→
A
:
{
N
AB
,N
BA
}
Pub
A
N
BA
}
Pub
B
The three protocol participants are named
A, B, I
.Here
I
is a malicious insider:
in other words, the hostile environment has registered itself as a legitimate par-
ticipant having name
I
,privatekey
Prv
I
and public key
Pub
I
. We add an action
'
out
(
3.
A
−→
B
:
{
)' that the participant
X
performs when he believes to
have successfully authenticated the participant
Y
by message
m
.Theformal
description of the protocol is as follows:
{
Xauth.Y bym
}
A
de
=
A
[
Π
X∈{I,B}
(
out
(
newN
AX
{
N
AX
,A
}
Pub
X
)
.in
(
{
N
AX
,
?
N
x
}
Pub
A
)
.out
(
{
Aauth.XbyN
AX
}
)
.out
(
{
N
x
}
Pub
X
)
,
{
Pub
A
,Pub
B
,Pub
I
,Prv
A
}
]
B
de
=
B
[
Π
Y ∈{I,A}
(
in
(
{
?
N
y
,Y
}
Pub
B
)
.out
(
newN
BY
(
{
N
y
,N
BY
}
Pub
Y
))
.in
(
{
N
BY
}
Pub
B
)
.out
(
{
Bauth.Y byN
BY
}
)
,
{
Pub
A
,Pub
B
,Pub
I
,Prv
B
}
]
System
de
=
A
B
In order to make the description more readable some obvious meta-notation is
used. In particular we have abbreviated '
P
1
|···|
P
n
'to'
Π
i∈
1
,···,n
P
i
'.
This version of the protocol is subject to a subtle form attack [10]. In this
protocol, the initiator
A
and the responder
B
authenticates each other by ex-
changing nonce, and only
A
and
B
know the exchanging nonces. Formally the
authentication goal is that
C
0
|
=
B
[
out
(
{
N
AB
,N
BA
}
Pub
A
)]
←
A
[
out
(
{
Aauth.BbyN
AB
}
)]
and
)]
hold. But this is not that case for the latter. The attack is that,
A
tries to
establish a session with the intruder
I
, while
I
impersonates
A
to establish
C
0
|
=
A
[
out
(
{
N
BY
}
Pub
B
)]
←
B
[
out
(
{
Bauth.AbyN
BY
}
