Information Technology Reference
In-Depth Information
A The Needham-Schroeder Public-Key Protocol
To help understand the detail of the specification and of the mappings, we will
analyze an example, consisting of the following classical protocol:
A −→ B
:
{A, N
A
}
K
B
B −→ A
:
{B, N
A
,N
B
}
K
A
A −→ B
:
{N
B
}
K
B
A.1 NSPK in MSR
P
R
NSPK
=
The MSR
P
specification of this protocol will consist of the rule-set
(
R
A
, R
B
).
R
A
and
R
B
implement the roles of the initiator (
A
) and the responder
(
B
) respectively. They are given as follows:
π
˜
(
A
)
→∃N
A
.
π
˜
(
A
)
,
0
(
A
,N
A
)
A
0
(
A
,N
A
)
→ N
(
{A, N
A
}
K
B
)
,A
1
(
A
,N
A
)
R
A
A
1
(
A
,N
A
)
,
N
(
{B, N
A
,N
B
}
K
A
)
→
A
2
(
A
,N
A
,N
B
)
A
2
(
A
,N
A
,N
B
)
→ N
(
{N
B
}
K
B
)
,
A
3
(
A
,N
A
,N
B
)
˜
π
(
B
)
→∃N
B
.
˜
π
(
B
)
,
B
0
(
B
,N
B
)
B
0
(
B
,N
B
)
,
N
(
{A, N
A
}
K
B
)
→
B
1
(
B
,N
B
,N
A
)
R
B
B
1
(
B
,N
B
N
A
)
→ N
(
{B, N
A
,N
B
}
K
A
)
,B
2
(
B
,N
B
,N
A
)
B
2
(
B
,N
B
,N
A
)
,N
(
{N
B
}
K
B
)
→
B
3
(
B
,N
B
,N
A
)
A, B, K
A
,K
A
,K
B
)
where:
A
=(
B, A, K
B
,K
B
,K
A
)
B
=(
X, Y, K
X
,K
X
,K
Y
)=
X, K
X
K
X
,K
X
π
˜
(
(
X
)
,
PrK
(
)
,
PbK
(
Y, K
Y
)
,
Kp
(
)
Pr
In addition, we assume the state portion of a configuration consists of:
a, b, k
a
,k
a
,k
b
)
b, e, k
b
,k
b
,k
e
)
e, a, k
e
,k
e
,k
a
)
k
e
)
˜
π
(
,
˜
π
(
,
π
˜
(
,
I
(
e
)
,I
(
k
e
)
,I
(
˜
˜
π
˜
I
N
A
k
are constants (
where
a
,
b
,
e
,
k
and
e
stands for the intruder).
A.2 NSPK in PA
P
NSPK
=
P
!
net
Q
!
I
P
!
A
P
!
B
Q
!
π
Q
I
0
P
!
net
and
Q
!
I
have already been defined. The other processes are as follows:
