O'Reilly logo

The Modelling and Analysis of Security Protocols: the CSP Approach by S. A. Schneider, P. Y.A. Ryan

Stay ahead with the world's most comprehensive technology and business learning platform.

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, tutorials, and more.

Start Free Trial

No credit card required

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

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, interactive tutorials, and more.

Start Free Trial

No credit card required