Rule Formats for Compositional Non Interference Properties

We introduce the transition rule formats rooted SBSNNI and CP_BNDC. We prove that the non-interference property rooted SBSNNI introduced in the present paper, and the already known non-interference property CP_BNDC, are preserved by constructs of all process algebras with SOS transition rules respecting the restrictions of the formats rooted SBSNNI and CP_BNDC, respectively. To show that our formats have practical applications, we prove that a slight variant of Focardi and Gorrieri's Security Process Algebra, the Kleene star recursion construct, the replication construct of polyadic π-calculus, and a process algebra extending BPAετ to deal with two level systems, respect both formats. By means of some counterexamples, we prove also that all restrictions of the formats are necessary.