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.
Rule Formats for Compositional Non Interference Properties
TINI, SIMONE
2004-01-01
Abstract
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.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.