Abstract
In recent times information flow and non-interference have become very popular concepts for expressing both integrity and privacy properties. We present the first general definition of probabilistic non-interference in reactive systems which includes a computational case. This case is essential to cope with real cryptography since non-interference properties can usually only be guaranteed if the underlying cryptographic primitives have not been broken. This might happen, but only with negligible probability. Furthermore, our definition links noninterference with the common approach of simulatability that modern cryptography often uses. We show that our definition is maintained under simulatability, which allows secure composition of systems, and we present a general strategy how cryptographic primitives can be included in information flow proofs. As an example we present an abstract specification and a possible implementation of a cryptographic firewall guarding two honest users from their environment.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
M. Backes. Cryptographically sound analysis of security protocols. Ph.D thesis, Computer Science Department, Saarland University, 2002. Available at http://www-krypt.cs.uni-sb.de/~mbackes/diss.ps.
M. Backes, C. Jacobi, and B. Pfitzmann. Deriving cryptographically sound implementations using composition and formally verified bisimulation. In Proceedings of Formal Methods Europe 2002 (FME’02), Copenhagen, 2002.
D. Bell and L. LaPadula. Secure computer systems: Unified exposition and multics interpretation. Technical Report ESD-TR-75-306, The Mitre Corporation, Bedford MA, USA, March 1976.
D. Clark, C. Hankin, S. Hunt, and R. Nagarajan. Possibilistic information flow is safe for probabilistic non-interference. Workshop on Issues in the Theory of Security (WITS’00), available at http://www.doc.ic.ac.uk/clh/Papers/witscnh.ps.gz.
D. E. Denning. A lattice model of secure information flow. Communications of the ACM 19/5 (1976) 236–243.
J. A. Goguen and J. Meseguer. Security policies and security models. IEEE Symposium on Security and Privacy, IEEE Computer Society Press, Washington 1982, 11–20.
J. A. Goguen and J. Meseguer. Unwinding and inference control. IEEE Symposium on Security and Privacy, IEEE Computer Society Press, Oakland 1984, 75–86.
O. Goldreich. Foundations of cryptography: Basic tools. Cambridge University Press, 2001.
J.W. Gray III. Probabilistic interference. IEEE Symposium on Security and Privacy, IEEE Computer Society Press, Los Alamitos 1990, 170–179.
J. W. Gray III. Toward a mathematical foundation for information flow security. Journal of Computer Security, Vol. 1, no. 3,4, 1992, 255–295.
C.A. R. Hoare. Communicating sequential processes. International Series in Computer Science, Prentice Hall, Hemel Hempstead 1985.
P. Laud. Semantics and program analysis of computationally secure information flow. 10th European Symposium On Programming (ESOP 2001), LNCS 2028, Springer-Verlag, Berlin 2001, 77–91.
N. Lynch. Distributed algorithms. Morgan Kaufmann Publishers, San Francisco 1996.
H. Mantel. Unwinding possibilistic security properties. 6th European Symposium on Research in Computer Security (ESORICS’00), Toulouse 2000, 238–254.
D. McCullough. Specifications for multi-level security and a hook-up property. IEEE Symposium on Security and Privacy, IEEE Computer Society Press, Oakland 1987, 161–166.
J. McLean. Security models. in: John Marciniak (ed.): Encyclopedia of Software Engineering; Wiley Press, 1994.
J. McLean. Security models and information flow. IEEE Symposium on Security and Privacy, IEEE Computer Society Press, Los Alamitos 1990, 180–187.
B. Pfitzmann and M. Waidner. A model for asynchronous reactive systems and its application to secure message transmission. IEEE Symposium on Security and Privacy, Oakland, May 2001, 184–201.
D. Sutherland. A model of information. 9th National Computer Security Conference; National Bureau of Standards, National Computer Security Center, September 1986, 175–183.
J. T. Wittbold and D. M. Johnson. Information flow in nondeterministic systems. IEEE Symposium on Security and Privacy, IEEE Computer Society Press, Los Alamitos 1990, 144–161.
A. C. Yao. Protocols for secure computations. 23rd Symposium on Foundations of Computer Science (FOCS) 1982, IEEE Computer Society, 1982, 160–164.
A. Zakinthinos and E. S. Lee. A general theory of security properties. IEEE Symposium on Security and Privacy, IEEE Computer Society Press, Washington 1997, 94–102.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Backes, M., Pfitzmann, B. (2002). Computational Probabilistic Non-interference. In: Gollmann, D., Karjoth, G., Waidner, M. (eds) Computer Security — ESORICS 2002. ESORICS 2002. Lecture Notes in Computer Science, vol 2502. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45853-0_1
Download citation
DOI: https://doi.org/10.1007/3-540-45853-0_1
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-44345-2
Online ISBN: 978-3-540-45853-1
eBook Packages: Springer Book Archive