From the previous section, we may conclude that it is extremely important to have (a) a fully automated theorem prover, but also (b) a protocol description that is suitable for implementors. In the best case, the description can lead to an automatic code generation. This releases us from the burden of proving that an implementation corresponds to the (idealized?) specification of the protocol.
Our research group has built a theorem prover `CryptoLog', which has action-based input (i.e. input written in some imperative language). The following rules were adopted when this input-language was designed:
If the code that implements the protocol for each participant were written as a single procedure, the initial assumptions would be input parameters, be it pre-installed keys, or a list of participants (servers, trusted third parties, ...) that fulfil the jurisdiction conditions.
The second kind of assumptions refer to actual actions that have to be performed in the procedure.
Table 6: Assumptions understood by the Analyser
Table 7: Actions understood by the Analyser