8.2. Transformations on protocols
In this section we formalize how we represent transformations upon protocols; we then state a result, giving sufficient conditions for a transformation to be safe.
Formalizing transformations
A transformation will be defined via a function
which defines how facts in the original protocol are replaced by facts in the simplified protocol. In the following, we will overload f to apply to several different types of arguments.
We lift the function f to events as follows:
and lift it to traces by applying it pointwise ...
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.
