Abstract
Unwinding conditions are helpful to prove that deterministic systems fulfill non-interference. In order to generalize non-interference to non-deterministic systems various possibilistic security properties have been proposed. In this paper, we present generic unwinding conditions which are applicable to a large class of such security properties. That these conditions are sufficient to ensure security is demonstrated by unwinding theorems. In certain cases they are also necessary. The practical usefulness of our results is illustrated by instantiating the generic unwinding conditions for well-known security properties. Furthermore, similarities of proving security with proving refinement are identified which results in proof techniques which are correct as well as complete.
Keywords
Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
Alpern, B., Schneider, F.B.: Defining Liveness. Information Processing Letters 21, 181–185 (1985)
Focardi, R., Gorrieri, R.: A Classification of Security Properties for Process Algebras. Journal of Computer Security 3(1), 5–33 (1995)
Foley, S.N.: A Universal Theory of Information Flow. In: Proceedings of the IEEE Symposium on Security and Privacy, pp. 116–122 (1987)
Graham-Cumming, J., Sanders, J.W.: On the Refinement of Noninterference. In: Proceedings of the IEEE Computer Security Foundations Workshop, pp. 35–42 (1991)
Goguen, J.A., Meseguer, J.: Security Policies and Security Models. In: Proceedings of the IEEE Symposium on Security and Privacy, pp. 11–20 (1982)
Goguen, J.A., Meseguer, J.: Inference Control and Unwinding. In: Proceedings of the IEEE Symposium on Security and Privacy, pp. 75–86 (1984)
Jacob, J.: On the Derivation of Secure Components. In: Proceedings of the IEEE Symposium on Security and Privacy, pp. 242–247 (1989)
Jacob, J.: Categorising Non-interference. In: Proceedings of the Computer Security Workshop, pp. 44–50 (1990)
Lynch, N., Vaandrager, F.: Forward and Backward Simulations, Part I: Untimed Systems. Information and Computation 121(2), 214–233 (1995)
Mantel, H.: Possibilistic Definitions of Security –An Assembly Kit–. In: Proceedings of the IEEE Computer Security Foundations Workshop (2000)
McCullough, D.: Specifications for Multi-Level Security and a Hook-Up Property. In: Proceedings of the IEEE Symposium on Security and Privacy, pp. 161–166 (1987)
McLean, J.: A General Theory of Composition for Trace Sets Closed under Selective Interleaving Functions. In: Proceedings of the IEEE Symposium on Research in Security and Privacy, pp. 79–93 (1994)
Millen, J.K.: Unwinding Forward Correctability. In: Proceedings of the Computer Security Foundations Workshop, pp. 2–10 (1994)
O’Halloran, C.: A Calculus of Information Flow. In: Proceedings of the European Symposium on Research in Computer Security, ESORICS 1990 (1990)
Ryan, P.Y.A., Schneider, S.A.: Process Algebra and Non-interference. In: Proceedings of the 12th IEEE Computer Security Foundations Workshop, pp. 214–227 (1999)
Rushby, J.: Noninterference, Transitivity, and Channel-Control Security Policies. Technical Report CSL-92-02, SRI International (1992)
Roscoe, A.W., Woodcock, J.C.P., Wulf, L.: Non-interference through Determinism. In: Gollmann, D. (ed.) ESORICS 1994. LNCS, vol. 875, pp. 33–53. Springer, Heidelberg (1994)
Ryan, P.Y.A.: A CSP Formulation of Non-Interference and Unwinding. Cipher, 19–30 (Winter 1991)
Sutherland, D.: A Model of Information. In: Proceedings of 9th National Computer Security Conference (1986)
van Glabbeek, R.J.: The Linear Time – Branching Time Spectrum. In: Baeten, J.C.M., Klop, J.W. (eds.) CONCUR 1990. LNCS, vol. 458, pp. 278–297. Springer, Heidelberg (1990)
Zakinthinos, A., Lee, E.S.: A General Theory of Security Properties. In: Proceedings of the IEEE Symposium on Security and Privacy, pp. 94–102 (1997)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Mantel, H. (2000). Unwinding Possibilistic Security Properties. In: Cuppens, F., Deswarte, Y., Gollmann, D., Waidner, M. (eds) Computer Security - ESORICS 2000. ESORICS 2000. Lecture Notes in Computer Science, vol 1895. Springer, Berlin, Heidelberg. https://doi.org/10.1007/10722599_15
Download citation
DOI: https://doi.org/10.1007/10722599_15
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-41031-7
Online ISBN: 978-3-540-45299-7
eBook Packages: Springer Book Archive