Recall that we wish to prove that, for any i and S , the message T
We now have to define a rank function, which must assign a rank of 1 or above to allow messages which may possibly circulate in the network, and a rank of 0 or below to all messages which may not circulate in the network.
The rank function we used is given in Figure 3.
Figure 3: The Rank Function
Proving that each of the processes maintains rank is very straightforward. The proof consists mainly of PVS macro steps developed specifically for authentication protocols, and presented in [DS97a]. The run times (on a Sparc 5) to check the proofs once they were developed were: userA took 25 seconds, userB took 91 seconds and server took 223 seconds.