** Next:** References
** Up:** CSP, PVS and a
** Previous:** Corrected Implementation

One of the less intuitive parts of the proof method outlined above is
the rank function. It is not easy to tell at a glance whether a
particular rank function will work or not, and if a proof fails it is
not necessarily obvious whether this is because the protocol is
flawed, or because the rank function was inappropriate. To some
extent, improvements on a flawed rank function may be deduced by
considering the PVS output. After applying the macro steps, we can
reduce nontrivial sequents to their component parts (using `
grind`), which gives us a list of consequents and antecedents.
The antecedents originate essentially from the information that the
rank function provides about messages which have already been observed
in the network.
If none of the consequents follow from the antecedents , then it is sometimes possible to deduce a strengthening of
the rank function by observing the consequents. Further protocol
verification attempts are required in order to develop heuristics for
this.