7.6. Summary

This chapter has introduced the rank-function technique, initially given in [86]. This technique is used for establishing that certain events in a protocol execution cannot occur, or can only occur under particular circumstances. The idea is to provide a function that assigns a value or rank to facts and to signals, such that only those with positive rank can arise in a protocol execution: if agents only receive facts of positive rank, then they can only ever produce facts and signals of positive rank. Thus verification of the overall protocol is reduced to proof obligations on each of the components separately.

The laws of CSP allow different cases to be considered separately, and hence to be verified with different rank functions. ...

Get The Modelling and Analysis of Security Protocols: the CSP Approach now with the O’Reilly learning platform.

O’Reilly members experience books, live events, courses curated by job role, and more from O’Reilly and nearly 200 top publishers.