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 ...
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.
