Computational probabilistic noninterference

Information flow and noninterference are popular concepts for expressing confidentiality and integrity properties. We present the first general definition of probabilistic noninterference in reactive systems that includes a computational case. This case is essential for coping 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 noninterference 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.