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:
S: A,B,N 
A: {N ,B,K 
,{K ,A} 
} 
B: {K ,A} A: {N 
} 
B: {N -1} The expanded protocol from A's point of view is:
: A,B,N {A sends a message}
A: {N ,B,K ,{K ,A} } {A receives the message}
{A decrypts the message}
B)
)
{K ,A}
A: {N }
}
,1) = N -1
-1,K ) = {N -1}
{N -1}
Steps NS-A1 through NS-A5 are used in testing A's postconditions. The postconditions for A should be:
) Discharged in step NS-A2 B)
Discharged in step NS-A4 )) Discharged in step NS-A5
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:
) B) )
S) , and K 
)
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:
B: {K ,A}
,A}
B)
)
,K ) = {N }
{N }
B: {N -1}
-1}
Steps NS-A1 through NS-A5 are used in testing A's postconditions. The postconditions for B should be:
) Discharged in step NS-B2 B)
Discharged in step NS-B3 )) Discharged in step NS-B4
) Discharged in step 8
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:
) B) )
S)
,N )
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.