The use of logics for cryptographic protocols can be hampered in practical applications. In this section, we will show two examples where the `use' of the logics is not optimal:

- in the enhanced Needham-Schroeder protocol (as described
in [3]), a
*hand-made*proof is given which contains, unfortunately, a small error, due to a misinterpretation of the concept of `a good key'. Although the proof itself is neither difficult, nor very long, it is for humans very difficult to construct such a proof one deduction step at a time. Hence, a fully automated theorem prover is really necessary. - in the modified wide-mouthed-frog protocol, the idealization step removed redundant fields. The order of these fields, however, is important in a real implementation.

Mon Aug 4 16:31:43 MET DST 1997