4.4. Counterexamples
When the exploration encounters a pair of states that are not compatible in the model of the check, this is a witness that the refinement does not hold. It remains to cast this into a counterexample that is informative to the user.
The first step is to determine how we got to this point. Each pair is stored with a reference to the pair (or the first of possibly many) from which it was reached during the exploration. Thus it is possible to build up (backwards) a path through the plies of the breadth-first search leading from the initial pair of start states up to the witness. Because this steps forward a ply at a time, it is guaranteed to be minimal in length among such paths, leading to a counterexample with no unnecessary ...
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.
