The authentication property

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

$$rec(b, i, encrypt(longterm(lt(b)), conc3(S, Ia, Nb)))$$

authenticates R

$$\{ trans(s, j, encrypt(longterm(lt(b)), conc3(S, Ia, Nb))) \}$$

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.