** 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