Recall that we wish to prove that, for any *i* and *S* , the message
*T*

authenticates *R*

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

The rank of all text, nonces and user identities is one. All session keys apart from the one between

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.