Next: An Example: The
Up: CryptoLog: A Theorem Prover
Previous: Action Based Input
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
- expand the included function calls:
i.e. expand pre-defined short-cuts;
- canonicalize the message;
- append annotations:
these are beliefs of the sender (see );
- check the sender-rules:
the analyser verifies the possession and belief
(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 , have been
- 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
Table 8: Transformation of the initial Assumptions
Table 9: Transformation of actions by the Analyser
Bart De Decker
Mon Aug 4 16:31:43 MET DST 1997