This section presentes the use of the weakest precondition calculus to prove the Needham-Schroeder protocol for key distribution (not for public keys). The original protocol is:
The expanded protocol from A's point of view is:
Steps NS-A1 through NS-A5 are used in testing A's postconditions. The postconditions for A should be:
Note that we do not include a post-condition that A sent any message to initiate the protocol. We strongly believe that such a post condition is important, and that specific ordering between protocol steps should be maintained. This is discussed further in [AF97].
Table 14: Proof of A's postconditions for NS protocol.
The proof of A's postconditions (steps 1 through 9 of the protocol) are presented in Table 14, generating the following preconditions for A:
It's now been proven that A believes (A
B) and that A believes
(fresh(K
)). However, steps 5 and 4 are not entirely correct. In
step 8 ``S says K
'' is treated as ``S says A
B''. Either ``A believes (S says
K
S says A
B)''
should be a premise or ``K
'' should be idealized as ``A
B'' in S's message to A.
Similarly in step 9 ``A believes (S says
)'' is used where ``A
believes (S says (fresh(K
)))'' is necessary. Again the two
solutions are a premise saying ``A believes (S says K
S says
fresh(K
)'' or an idealization. For both of these problems Syverson
and van Oorschot [Syv96] use the premise approach, we have opted
for protocol idealization.
The expanded protocol from B's point of view is:
Steps NS-A1 through NS-A5 are used in testing A's postconditions. The postconditions for B should be:
The first three postconditions are symmetric to those of A. The last is
used to help prove currency, and requires an additional premise that N
is fresh.
One difficulty in this proof comes from conditions of the form
B sent {K
,A}
. The truth of this negated
conditions comes from making sure that B sent {K
,A}
isn't in any of the preconditions. This may raise complications that
aren't there for the other conditions which can be proven in a single step.
Table 15: Proof of B's postconditions for NS protocol.
The proof of B's postconditions is shown in Table 15 and generates the following preconditions for B:
The problems arise in steps 2, 3, and 4. First, just as for participant
A, the server S only mentions the key K and does not explicitly
mention its freshness or validity. Unlike in A's proof an idealization
(e.g. K
idealized as fresh (K
)) won't work for B. Because of
the nonce N
participant A could believe ``S says K
'', but at
best B can only prove ``S said K
'' (step 12). Thus, the proof:
S says fresh (K )
S controls fresh (K
)
fresh (K
)
doesn't work. Instead a premise such as:
S said fresh (K )
fresh (K
)
is necessary. Of course, using said in the place of says is quite risky as
B can be subjected to a replay attack using old, broken keys for K
and K
even if the key K
remains valid. Again, we have assumed
a protocol idalization to remove this problem. Further work is definitely
needed to resolve this problem in the verification of this protocol.