Dealing with failed proofs

  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.