International Journal of Information Security (IJIS), 3(1):42-60, 2004.
Information flow and non-interference are popular concepts for expressing confidentiality and integrity properties. We present the first general definition of probabilistic non-interference in reactive systems that includes a computational case. This case is essential to cope with real cryptography, since noninterference properties can usually only be guaranteed if the underlying cryptographic primitives have not been broken. This might happen, but only with negligible probability.We show that our non-interference definition is maintained under simulatability, the notion of secure implementation of modern cryptography. This allows secure composition of systems and yields a general strategy for including cryptographic primitives in information-flow proofs. As an example we study a cryptographic firewall guarding two honest users from their environment.
This publication is accompanied by links to downloadable versions of this publication. These documents do not necessarily correspond exactly to the cited version. Instead, in most cases full or updated versions are provided. For access to the official version, follow the "Official version" link to the publishers site.