Some Pitfalls of Logics

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.

• Enhanced Needham-Schroeder Protocol
• Modified Wide-Mouthed-Frog Protocol