Next: Introduction
CryptoLog: A Theorem Prover for Cryptographic Protocols
Bart De Decker and Frank Piessens
Postscript version
Abstract:
Logics for cryptographic protocols have proved very useful in
validating the correctness of these protocols. However,
neither the specification, nor the logic proof help the implementor
of the protocol. Although the proof states the assumptions explicitly,
it does not ---in general--- contain guidelines for the implementation.
In this paper, we present a theorem prover whose input is very close
to a program written in a procedural language. Moreover, explicit
guidelines for implementors may be given.
Bart De Decker
Mon Aug 4 16:31:43 MET DST 1997