Comparing two information flow security properties
Riccardo Focardi · 2002
In this paper we compare two information flow security properties: the lazy security (L-Sec) by A.W. Roscoe et al. (1994) and the bisimulation non-deducibility on compositions (BNDC) by R. Focardi and R. Gorrieri (1996). To make this we define the failure non-deducibility on compositions, a failure semantics version of the BNDC. The common specification language used for the comparison is the Security Process Algebra, an extension of CCS which permits to describe systems where actions belong to two different levels of confidentiality. We prove that BNDC applied to a restricted class of systems, the low-deterministic and non-divergent ones, is equal to L-Sec. So these two properties, which are based on quite different underlying intuitions, become the same if we add some conditions to BNDC.