next up previous
Next: Notations Up: CryptoLog: A Theorem Prover Previous: CryptoLog: A Theorem Prover

Introduction

Logics for cryptographic protocols have proved to be of invaluable help in validating and correcting these protocols (see also [2]):

Despite their many merits, they also have their limitations:

These limitations make it difficult for a programmer to implement the protocol correctly and interpret the assumptions in the right way. Many assumptions do influence the implementation. In this paper a new syntax is shown which offers extensive guidelines to the implementors of these protocols.

The rest of this paper is organized as follows. In the next section, we briefly introduce the notations used in this paper. Section 3 illustrates some pitfalls of the GNY and BAN logic. In section 4, we introduce the action-based syntax of CryptoLog, a new theorem prover for cryptographic protocols. Section 5 describes the tasks performed by the prover. Section 6 shows typical input and output for the analyser. In section 7, we discuss some future work. Finally, section 8 summarizes the conclusions.



next up previous
Next: Notations Up: CryptoLog: A Theorem Prover Previous: CryptoLog: A Theorem Prover



Bart De Decker
Mon Aug 4 16:31:43 MET DST 1997