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.
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 ...