Verifying Persistent Security Properties

We study bisimulation-based information flow security properties which are persistent, in the sense that if a system is secure then all of its reachable states are secure too. We show that such properties can be characterized in terms of bisimulation-like equivalence relations, between the full system and the system 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, that allow us to check the security of a system by only verifying the security of its subcomponents.