After reviewing the protocol analysis provided in Section 4 there is an apparent strategy to the proofs. This strategy involves specification of the protocol in expanded form, from the point of view of the recipient; generation of the set of post conditions for the protocol; and then systematic generation of the set of preconditions for the protocol. What if we took this one step further? Suppose that we only defined the post conditions of the protocol and used a variable, Pl to denote the list of protocol steps. Define Pl as , which means Pl is a list of steps that terminates with step . Choosing an appropriate , we can generate the wps for with respect to the given postconditions. We can now use these as postconditions for . Following this process we can incrementally unwind the protocol specification generating preconditions as we go. Once we have reached a set of satisfactory preconditions, we can stop.
This is not trivial, and definitely not readily automatable, but there we can develop some heuristics to assist in this effort. For example, we can search the list of postconditions for those which correspond to an appropriate weakest precondition rule. We then insert the operation associated with the rule and modify the preconditions. Any precondition of a form that is typical of protocol premises (such as A sees its own public and private keys) can be ignored and propagated up.
It is our belief that with some work, now underway at the University of Idaho, we can develop a set of heuristics that will enable us to formalize the derivation of protocols.