Introduction

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

• these logics help to formalize the reasoning about useful abstract properties of these protocols;
• the logics require to write down the initial security assumptions of the protocol that might otherwise be buried in the implementation details;
• the logics achieve reasonably well-defined goals; the analysis process ties the evolution of beliefs to message contents and number of messages; this has certainly many advantages:
  • it helps to determine the minimum number of messages to achieve a certain set of beliefs;
  • useless or erroneous message exchanges can be spotted easily;
  • subtle differences between similar protocols come to the surface.

Despite their many merits, they also have their limitations:

• most logics are based on assumptions that are not written explicitly;
  for instance, many assume that the concatenation of expressions is commutative and that the sender can recognize its own messages; moreover, they assume that the integrity of encrypted (or signed) messages is always preserved (i.e. they withstand message-splicing attacks),
• many require an `idealization' process, or at least the addition of extra annotations;
  this `process', which need to be done prior to the analysis, is not fully automated, and therefore error-prone;
• often, the analyser uses a cumbersome syntax, which makes it harder to non-experts to understand the `subtleties' of the protocol.

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.