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

10.8. Data independence

The pragmatics of running model-checkers such as FDR mean, unfortunately, that the sizes of types, such as that of nonces, have to be restricted to far smaller sizes than the types they represent in implementations. Usually they have to be kept down to single figures if the combinatories of how they can create messages of the protocol is not to take other types that have to be considered, such as the overall alphabet size and the set of facts that a potential intruder might learn, beyond the level that can be managed. The models that have been crafted by hand, and which are produced by Casper, therefore allocate a small finite number of these values to each node that has to ‘invent’ them during a run, so that each time ...

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