Chapter 7. Theorem proving
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
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.
