Comparing two information flow security properties
- 23 December 2002
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- p. 116-122
- https://doi.org/10.1109/csfw.1996.503696
Abstract
In this paper we compare two information flow security properties: the lazy security (L-Sec) (11) and the Bisimu- lation Non-deducibility on Compositions (BNDC) (4). To make this we define the Failure Non-deducibility on Com- positions, a failure semantics version of the BNDC. The common specification language used for the comparison is the Security Process Algebra (4), an extension of CCS (8) 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-determini stic 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.Keywords
This publication has 6 references indexed in Scilit:
- The security checker: a semantics-based tool for the verification of security propertiesPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- CSP and determinism in security modellingPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- A Classification of Security Properties for Process Algebras1Journal of Computer Security, 1995
- The concurrency workbenchACM Transactions on Programming Languages and Systems, 1993
- An improved failures model for communicating processesPublished by Springer Nature ,1985
- A Theory of Communicating Sequential ProcessesJournal of the ACM, 1984