A Logical View of Secure Dependencies *

Abstract

In the context of the modal logic of security, confidentiality is defined by the formula ${\mathit{K}}_{\mathit{B}}\mathit{\phi }\to {\mathit{R}}_{\mathit{B}}\mathit{\phi }$ that could be read “If B knows φ then B should have the permission to know φ”. We propose a new semantics for the ${\mathit{R}}_{\mathit{B}}$ modal operator, such that the definition of security would allow a certain number of dependencies (called secure dependencies) between objects of the system. We formally compare this new definition of security with non-interference, non-deducibility and generalized non-interference, especially with respect to assumptions of non-determinism and input-totalness.