The analysis and verification techniques discussed in previous chapters make use of model-checking methods to analyze protocols. In order to do this they must make various finitary restrictions to enable the model-checking to terminate. Using these restrictions flaws can be quickly identified. Furthermore, data-independence results permit general protocol correctness to be deduced in some cases from correctness of the checked finite system.
This chapter is concerned with the development of a general proof technique built upon the traces model of CSP. Properties of the Yahalom protocol will be verified as a running example. In Chapter 2 we introduced a general CSP model of protocols and intruders, and in Chapter 3