next up previous
Next: Introduction

CryptoLog: A Theorem Prover for Cryptographic Protocols

Bart De Decker and Frank Piessens gif

Postscript version


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