8.3. Examples of safe simplifying transformations
In this section we present a number of transformations that satisfy the conditions from the previous section, and are hence safe.
Removing encryptions
We begin by defining a transformation that removes some of the encryptions from the protocol. We identify a set Encs of encrypted messages such that all encrypted components {m}k from Encs that appear in the protocol should be replaced with the body m. The transformation function f is as follows:
The interesting case is the case for {m}k with {m}k ∊ Encs, where the outermost encryption is stripped off; most of the other cases simply apply the ...
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.
