8.4. Structural transformations
We now consider two classes of transformations that are not formed by simple renaming of messages within the protocol, but instead change the structure of the protocol: we consider a transformation that splits a single message into two, and another that replaces two messages with a single message, redirecting a message that is sent via a third party so that it is sent direct.
We begin by describing message-splitting transformations. The idea is that if we have a fact m1.m2 that is transmitted in a protocol run, then we replace this with a pair of facts, m1 and m2 respectively.
Such a transformation can be advantageous when model checking, because it reduces the size of the message space (the number of distinct ...
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.
