7.5. Machine assistance
In practice, the identification of suitable rank functions can be difficult, and (as the previous case study has shown) the verification proofs can generate an almost overwhelming amount of detail to keep track of. Two forms of mechanical support that address this problem are currently available for the rank function verification technique.
The first form of mechanical assistance is provided by the general purpose theorem prover PVS(Prototype Verification System) [91]. This interactive theorem prover allows theories to be constructed and verified in a hierarchical fashion, making use of previously verified theories. A theory for the trace semantics of CSP has been provided, and then more specialized theories about rank ...
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.
