Table 2 shows the enhanced Needham-Schroeder Protocol as it has been published in . 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