0.11. Limits of formal analysis
It is quite possible to implement a perfectly secure protocol using high-grade crypto-algorithms in such a way that the result is hopelessly flawed. A real example of this is an implementation proposed by a company called APM of a protocol that had been verified by Paulson [69]. This was found to have a glaring vulnerability. Paulson’s analysis was perfectly valid, but the way APM proposed to implement the encryption gave rise to some additional algebraic identities not included in the model. It was these identities that the intruder could exploit. This is documented in [81].
More generally, security properties tend not to be preserved by conventional refinement techniques. This is a widely recognized problem ...
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.
