next up previous
Next: An Example: The Up: CryptoLog: A Theorem Prover Previous: Action Based Input

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:

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