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 A and B have rank one, and all
longterm keys have rank one, apart from the ones belonging to A , B
and the server. All hashed messages have a rank of one. Encrypted
messages have the same rank as the message itself, unless it is
encrypted with either A or B 's longterm key. All messages
encrypted with either A or B 's longterm key have rank one greater
than the message itself, except for the authenticating message.
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.
