Next: Enhanced Needham-Schroeder Protocol
Up: CryptoLog: A Theorem Prover
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 ), 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.
Bart De Decker
Mon Aug 4 16:31:43 MET DST 1997