Unwinding conditions provide a general framework for the definition of security properties. They basically depend on the operational semantics and on the (low level) observational equivalence of the specification language under consideration. Hence, …