Bisimulation and unwinding for verifying possibilistic security properties

We study bisimulation-based information flow security properties which are persistent, in the sense that if a system is secure, then all states reachable from it are secure too. We show that such properties can be characterized in terms of bisimulation-like equivalence relations between the system and the system itself prevented from performing confidential actions. Moreover, we provide a characterization of such properties in terms of unwinding conditions which-demand properties of individual actions. These two different characterizations naturally lead to efficient methods for the verification and construction of secure systems. We also prove several compositionality results and discuss a sufficient condition to define refinement operators preserving security.