The CryptoLog Analyser

The CryptoLog Analyser has been written in Prolog. Also, the input for the analyser (i.e. the protocol to be analysed) is a genuine prolog program: it consists of one or more Horn-clauses. Every initial assumption and every action is a subgoal of one of these clauses. In the next section, an extensive example of the input-syntax is shown.

The analyser performs the following tasks:

• it checks the soundness of every assumption/action;
  e.g. every assumption/action should be preceded by a principal name, ...
• it modifies the holds- and believes-relations;
  see tables 8 and 9.
• when the action is `send a message', the analyser will additionally:
  • expand the included function calls:
    i.e. expand pre-defined short-cuts;
  • canonicalize the message;
  • append annotations:
    these are beliefs of the sender (see [3]);
  • check the sender-rules:
    the analyser verifies the possession and belief consistency rules (sender may only send messages it was able to assemble; and only current beliefs may be included as annotations in a message);
  • apply receiver-rules:
    in this step, the holds- and beliefs-relations of the receiver are expanded (if possible);
    currently, the deduction rules, described in the GNY-paper [3], have been implemented;
  • apply the eavesdropper-rules:
    in this step, the analyser checks whether secret information is leaked.
• at the end, the analyser will print an overview of the holds- and beliefs-relations.
• finally, for every password used as a cryptographic key, the analyser checks the severeness of a successful dictionary attack. It lists all the secrets that will become known to the eavesdropper if the attack succeeds.

 
Table 8:  Transformation of the initial Assumptions

 
Table 9:  Transformation of actions by the Analyser