Multilevel transitive and intransitive non-interference, causally

We develop a theory of non-interference for multilevel security based on causality, with Petri nets as a reference model. We first focus on transitive non-interference, where the relation representing the admitted flow is transitive. Then we extend the approach to intransitive non-interference, where the transitivity assumption is dismissed, leading to a framework which is suited to model a controlled disclosure of information. Efficient verification algorithms based on the unfolding semantics of Petri nets stem out of the theory. We also argue about the possibility of performing a compositional verification.