Security properties have proved to be unexpectedly complex to grasp and formalize. One of the fundamental reasons for this is that security properties are not safety properties (w.r.t. the Alper-Schneider framework [1]}). Most of the verification methods, results and tools developed for almost half a century by the Software Engineering community have been aimed at safety properties. Then, most of them fall short when dealing with security properties. Only very recently some of these methods and tools have been adapted for the problem of security properties.
