The Modelling and Analysis of Security Protocols: the CSP Approach

7.4. Authentication

Authentication can also be established using the rank function approach. We want to establish that R precedes T. This can be achieved by restricting R and showing that T cannot occur in the resulting system. This works because

Hence we simply have to show that which we can do using rank functions: simply find an appropriate rank function for which all facts in T have rank 0.

Furthermore, the restriction of R can be distributed to the various components of System. Since R will actually be a set of signal events associated with ...