Abstract
Non-interference properties are an important class of security properties. Many different non-interference properties have been presented based on different underlying models including the process algebraic languages. Usually, in specifying the non-interference properties using process algebraic languages, a specific semantic equivalence is introduced. Though weak bisimulation based non-interference properties have been studied extensively, it is not always satisfactory. This paper considers the topic on pursuing a probably more suitable semantic equivalence for specifying the non-interference properties. We find several alternatives, e.g., should testing equivalence, impossible future equivalence and possible future equivalence, etc. As another topic in the paper, based on the structural operational semantics, we suggest a compositional rule format, the SISNNI format, for an impossible future equivalence based non-interference property, i.e., the SISNNI property. We show that the SISNNI property is compositional in any SISNNI languages, i.e., languages in the SISNNI format.
This research was financially supported by the National Natural Science Foundation of China (No. 60421001).
Chapter PDF
References
Focardi, R., Gorrieri, R.: Classification of Security Properties(Part I: Information Flow). In: Focardi, R., Gorrieri, R. (eds.) Foundations of Security Analysis and Design. LNCS, vol. 2171, pp. 331–396. Springer, Heidelberg (2001)
Rensink, A., Vogler, W.: Fair Testing. Information and Computation 205(2), 125–198 (2007)
van Glabbeek, R.J.: The Linear Time - Branching Time Spectrum I: The Semantics of Concrete, Sequential Processes. In: Bergstra, J.A., Ponse, A., Smolka, S.A. (eds.) Handbook of Process Algebra, ch. 1, pp. 3–100. Elsevier, Amsterdam (2001)
van Glabbeek, R.J.: The Linear Time - Branching Time Spectrum II: The semantics of sequential systems with silent moves. In: Best, E. (ed.) CONCUR 1993. LNCS, vol. 715, pp. 66–81. Springer, Heidelberg (1993)
De Nicola, R., Hennessy, M.: Testing Equivalences for Processes. Theoretical Computer Science 34, 83–133 (1984)
Huang, X., Jiao, L., Lu, W.: Rule Formats for Weak Parametric Failure Equivalences (submitted)
Ryan, P.Y.A.: Mathematical Models of Computer Security. In: Focardi, R., Gorrieri, R. (eds.) Foundations of Security Analysis and Design. LNCS, vol. 2171, pp. 1–62. Springer, Heidelberg (2001)
van der Meyden, R., Zhang, C.: A Comparison of Semantic Models for Noninterference. In: Dimitrakos, T., Martinelli, F., Ryan, P.Y.A, Schneider, S. (eds.) FAST 2006. LNCS, vol. 4691, Springer, Heidelberg (2006)
Bell, D.E., Padula, L.J.L.: Secure Computer Systems: Unified Exposition and Multics Interpretation. ESD-TR-75-306, MITRE MTR-2997 (March 1976)
Focardi, R., Rossi, S.: Information Flow Security in Dynamic Contexts. In: Proceeding of the IEEE Computer Security Foundations Workshop, pp. 307–319. IEEE Computer Society Press, Los Alamitos (2002)
Tini, S.: Rule Formats for Compositional Non-Interference Properties. Journal of Logic and Algebraic Progamming 60, 353–400 (2004)
Plotkin, G.D.: A Structural Approach to Operational Semantics. The Journal of Logic and Algebraic Programming, 60–61,17–139 (2004)
Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1989)
Mousavi, M.R., Reniers, M.A., Groote, J.F.: SOS formats and meta-theory: 20 years after. Theoretical Computer Science 373, 238–272 (2007)
Aceto, L., Fokkink, W.J., Verhoef, C.: Structural Operational Semantics. In: Bergstra, J.A., Ponse, A., Smolka, S.A. (eds.) Handbook of Process Algebra, Ch. 3, pp. 197–292. Elsevier, Amsterdam (2001)
Groote, J.F., Waandrager, F.W.: Structural Operational Semantics and Bisimulation as a Congruence. Information and Computation 100(2), 202–260 (1992)
Groote, J.F.: Transition System Specifications with Negative Premises. Theoretical Computer Science 118, 263–299 (1993)
Simone, R.D.: Higher-level synchronising devices in Meiji-SCCS. Theoretical Computer Science 37, 245–267 (1985)
Baeten, J.C.M., Weijiland, W.P.: Process Algebra. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge (1990)
Burris, S., Sankappanavar, H.P.: A Course in Universal Algebra. Graduate Texts in Mathematics, vol. 78. Springer, Berlin (1981)
Bloom, B., Istrail, S., Meyer, A.R.: Bisimualtion can’t be Traced. Journal of the ACM 42(1), 232–268 (1995)
Bloom, B.: Structural Operational Semantics for Weak Bisimulations. Theoretical Computer Science 146, 27–68 (1995)
Bloom, B.: Ready Simulation, Bisimulation, and the Semantics of CCS-Like Languages. PhD thesis, MIT (1990)
Ulidowski, I.: Finite Axiom Systems for Testing Preorder and De Simone Process Languages. Theoretical computer Science 239(1), 97–139 (2000)
van Glabbeek, R.J., Voorhoeve, M.: Liveness, Fairness and Impossible Futures. In: Baier, C., Hermanns, H. (eds.) CONCUR 2006. LNCS, vol. 4137, pp. 126–141. Springer, Heidelberg (2006)
Voorhoeve, I., Mauw, S.: Impossible Futures and Determinism. Information Processing Letters 80(1), 51–58 (2001)
Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985)
Bossi, A., Focardi, R., Piazza, C., Rossi, S.: Unwinding in Information Flow Security. Electronic Notes of Theoretical Computer Science 99, 127–154 (2004)
van Glabbeek, R.J.: On Cool Congruence Formats for Weak Bisimulations. In: Van Hung, D., Wirsing, M. (eds.) ICTAC 2005. LNCS, vol. 3722, pp. 331–346. Springer, Heidelberg (2005)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Huang, X., Jiao, L., Lu, W. (2007). What Semantic Equivalences Are Suitable for Non-interference Properties in Computer Security. In: Qing, S., Imai, H., Wang, G. (eds) Information and Communications Security. ICICS 2007. Lecture Notes in Computer Science, vol 4861. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-77048-0_26
Download citation
DOI: https://doi.org/10.1007/978-3-540-77048-0_26
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-77047-3
Online ISBN: 978-3-540-77048-0
eBook Packages: Computer ScienceComputer Science (R0)