next up previous
Next: Modified Wide-Mouthed-Frog Protocol Up: Some Pitfalls of Previous: Some Pitfalls of

Enhanced Needham-Schroeder Protocol

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

Bart De Decker
Mon Aug 4 16:31:43 MET DST 1997