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.
