10.5. Dependence on infrastructure assumptions

Great care must be taken in dealing with assumptions incorporated in the models used in any analysis. Ideally we should try to be explicit about any assumptions that the models depend upon. It is essential that engineers thinking of incorporating a particular verified protocol in a real architecture understand these assumptions and are able to check that the architecture does indeed guarantee the assumptions on which the protocol depends.

A good example of the dangers of straying outside the modelling assumptions is where the models assume that there is a suitable infrastructure to ensure that public keys can be reliably associated with principals. Suppose further that we assume that each principal ...

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.