Table 2 shows the enhanced Needham-Schroeder Protocol as it has been published in [3]. The purpose of the modifications (which are underlined) is
Table 2: The enhanced Needham-Schroeder protocol
In the original proof, the authors derive from the 
message:
P |
Q |
The authors come to that conclusion by applying the following deduction rule:
However, this rule can not be applied. P does not believe that
(
,Q,K) is fresh! It could be a replay of a previous run!
In the initial assumptions, S believes that K is a suitable key
for P and Q (S |
). However, nowhere is
mentioned that K should be freshly generated by S.
Hence, a final modification is necessary
(as shown in table 3; the modification is underlined twice).
Another possibility is to let
S generate a new key K for every run of the protocol (S |
#(K)).
This short example proves clearly that a hand-made analysis is error-prone, and should be examined very cautiously.
Table 3: The correctly enhanced Needham-Schroeder protocol