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.