Abstract
In the recent years, many formalizations of security properties have been proposed, most of which are based on different underlying models and are consequently difficult to compare. A classification of security properties is thus of interest for understanding the relationships among different definitions and for evaluating the relative merits. In this paper, many non-interference-like properties proposed for computer security are classified and compared in a unifying framework. The resulting taxonomy is evaluated through some case studies of access control in computer systems. The approach has been mechanized, resulting in the tool CoSeC. Various extensions (e.g., the application to cryptographic protocol analysis) and open problems are discussed.
This work has been partially supported byMURST projects TOSCA, “Certificazione automatica di programmi mediante interpretazione astratta” and “Interpretazione astratta, type systems e analisi control-flow”, and also partially supported by Microsoft Research Europe.
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. Abadi. “Secrecy by Typing in Security Protocols”. Journal of ACM, 46(5):749–786, 1999. 331
M. Abadi and A. D. Gordon. A calculus for cryptographic protocols: The spi calculus. Information and Computation, 148(1):1–70, 1999. 331, 392
A. Aldini. “Probabilistic Information Flow in a Process Algebra”. To appear in proceedings of CONCUR’01, 2001. 391
P. G. Allen. “A Comparison of Non-Interference and Non-Deducibility using CSP”. In Proceedings of the Fourth IEEE Computer Security Foundations Workshop, pages 43–54, Franconia, New Hampshire, June 1991. 368
D. E. Bell and L. J. La Padula. “Secure Computer Systems: Unified Exposition and Multics Interpretation”. ESD-TR-75-306, MITRE MTR-2997, March 1976.332.
J. A. Bergstra and J. W. Klop. “Algebra of Communicating Processes with Abstraction”. Theoretical Computer Science, 37:77–121, 1985. 356
P. Bieber and F. Cuppens. “A Logical View of Secure Dependencies”. Journal of Computer Security, 1(1):99–129, 1992. 333
C. Bodei, P. Degano, F. Nielson, and H. Riis Nielson. “Static Analysis of Processes for No Read-Up and No Write-Down”. In proc. of 2nd FoSSaCS’99, Amsterdam, March 1999. Springer. 331
S. D. Brookes, C. A. R. Hoare, and A. W. Roscoe. “A Theory of Communicating Sequential Processes”. Journal of the Association for Computing Machinery, 31(3):560–599, July 1984. 340, 348, 353
S. D. Brookes and A. W. Roscoe. “An Improved Failures Model for Communicating Processes”. In Proceedings of the Pittsburgh seminar on concurrency, pages 281–305. Springer-Verlag, LNCS 197, 1985. 370, 375
C. Bodei, P. Degano, R. Focardi, and C. Priami. “Authentication via Localized Names”. In Proceedings of CSFW’99, pages 98–110. IEEE press, 1999. 331, 392
C. Bodei, P. Degano, R. Focardi, and C. Priami. “Primitives for Authentication in Process Algebras”. Theoretical Computer Science, to appear, 2001. 331, 392
L. Cardelli and A. Gordon. “Mobile Ambients”. In proceedings of FoSSaCS’98, pages 140–155. Springer LNCS 1378, 1998. 392
R. Cleaveland, J. Parrow, and B. Steffen. “The Concurrency Workbench: a Semantics Based Tool for the Verification of Concurrent Systems”. ACM Transactions on Programming Languages and Systems, Vol. 15 No. 1:36–72, January 1993. 334,377, 379, 380
A. Durante, R. Focardi, and R. Gorrieri. “A Compiler for Analysing Cryptographic Protocols Using Non-Interference”. ACM Transactions on Software Engineering and Methodology, 9(4):489–530, 2000. 392
A. Durante, R. Focardi, and R. Gorrieri. “CVS at Work: A Report on New Failures upon Some Cryptographic Protocols”. In proceedings of Mathematical Methods, Models and Architectures for Computer Networks Security, pages 287–299, St. Petersburg, Russia, May 2001. LNCS 2052. 392
N. Durgin, J. Mitchell, and D. Pavlovic. “Protocol composition and correctness”. In proceedings of Workshop on Issues in the Theory of Security (WITS’ 00), University of Geneva, July 2000. 331
R. Focardi. “Comparing Two Information Flow Security Properties”. In Proceedings of Ninth IEEE Computer Security Foundation Workshop, (CSFW’96), (M. Merritt Ed.), pages 116–122. IEEE press, June 1996. 348, 368
R. Focardi. “Located Entity Authentication”. Technical Report CS98-5, University of Venice, 1998. 392
R. Focardi. “Using Entity Locations for the Analysis of Authentication Protocols”. In Proceedings of Sixth Italian Conference on Theoretical Computer Science (ICTCS’98), November 1998. 392
R. Focardi. Analysis and Automatic Detection of Information Flows in Systems and Networks. PhD thesis, University of Bologna (Italy), 1999. 331, 348
R. Focardi and R. Gorrieri. “An Information Flow Security Property for CCS”. In Proceedings of the Second North American Process Algebra Workshop (NAPAW’ 93), TR 93-1369, Cornell (Ithaca), August 1993. 348
R. Focardi and R. Gorrieri. “A Taxonomy of Trace-based Security Properties for CCS ”. In Proceedings Seventh IEEE Computer Security Foundation Workshop, (CSFW’94), (Li Gong Ed.), pages 126–136, Franconia (NH), June 1994. IEEE Press. 348,349.
R. Focardi and R. Gorrieri. “A Classification of Security Properties for Process Algebras”. Journal of Computer Security, 3(1):5–33, 1994/1995. 333, 335, 348,362, 363, 376, 377
R. Focardi and R. Gorrieri. “Automatic Compositional Verification of Some Security Properties”. In Proceedings of Second International Workshop on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’96), pages167–186, Passau (Germany), March 1996. Springer-Verlag, LNCS 1055. 377
R. Focardi and R. Gorrieri. “The Compositional Security Checker: A Tool for the Verification of Information Flow Security Properties”. IEEE Transactions on Software Engineering, 23(9):550–571, September 1997. 335, 348, 377
R. Focardi, R. Gorrieri, and F. Martinelli. “Classification of Security Properties (Part II: Network Security)”. Forthcoming. 392
R. Focardi, R. Gorrieri, and F. Martinelli. “Information Flow Analysis in a Discrete Time Process Algebra”. In Proceedings of 13th IEEE Computer Security Foundations Workshop (CSFW13), (P. Syverson ed.), pages 170–184. IEEE CS Press, July 2000. 391
R. Focardi, R. Gorrieri, and F. Martinelli. Message authentication through noninterference. In Proc. of 8th International Conference in Algebraic Methodology and Software Technology (AMAST), 2000. 392
R. Focardi, R. Gorrieri, and F. Martinelli. “Non Interference for the Analysis of Cryptographic Protocols”. In Proceedings of ICALP’00, pages 744–755. LNCS 1853, July 2000. 331, 392
R. Focardi, R. Gorrieri, and F. Martinelli. Secrecy in security protocols as noninterference. In Workshop on secure architectures and information flow, volume 32 of ENTCS, 2000. 392
R. Focardi, R. Gorrieri, and V. Panini. “The Security Checker: a Semanticsbased Tool for the Verification of Security Properties”. In Proceedings Eight IEEE Computer Security Foundation Workshop, (CSFW’95) (Li Gong Ed.), pages 60–69, Kenmare (Ireland), June 1995. IEEE Press. 377
R. Focardi, R. Gorrieri, and R. Segala. “A New Definition of Multilevel Security”. In proceedings of Workshop on Issues in the Theory of Security (WITS’ 00), University of Geneva, July 2000. 391
R. Focardi and F. Martinelli. “A Uniform Approach for the Definition of Security Properties”. In Proceedings of World Congress on Formal Methods (FM’99), pages 794–813. Springer, LNCS 1708, 1999. 392
C. Fournet and M. Abadi. “Mobile Values, New Names, and Secure Communication”. In Proceedings of the 28th ACM Symposium on Principles of Programming Languages (POPL’01), pages 104–115, January 2001. 392
J. A. Goguen and J. Meseguer. “Security Policy and Security Models”. In Proceedings of the 1982 Symposium on Security and Privacy, pages 11–20. IEEE Computer Society Press, April 1982. 332, 333, 348
M. Hennessy and J. Riely. “Information Flow vs. Resource Access in the Asynchronous Pi-Calculus”. In proceedings of ICALP, pages 415–427, 2000. 392
Y. Hirshfeld. “Bisimulation Trees and the Decidability of Weak Bisimulations“. Technical report, Tel Aviv University, 1996. 356
C. A. R. Hoare. Communicating Sequential Processes. Prentice-Hall, 1985. 336,337, 368
J. Hopcroft and J. Ullman. Introduction to Automata Theory, Languages and Computation., pages 22–24. Addison-Wesley, 1979. 381
D. M. Johnson and F. J. Thayer. “Security and the Composition of Machines”. In Proceedings of the Computer Security Foundations Workshop, pages 72–89, June 1988. 333, 376
P. Kanellakis and S. A. Smolka. “CCS Expressions, Finite State Processes, and Three Problems of Equivalence”. Information & Computation 86, pages 43–68, May 1990. 355, 380, 381
R. Keller. “Formal Verification of Parallel Programs”. Communications of the ACM, 19 (7):561–572, 1976. 333
G. Lowe. “Casper: A Compiler for the Analysis of Security Protocols”. Journal of Computer Security, 6:53–84, 1998. 331
G. Lowe and B. Roscoe. “Using CSP to detect Errors in the TMN Protocol”. IEEE Transactions on Software Engineering, 23(10):659–669, 1997. 331
D. Marchignoli and F. Martinelli. Automatic verification of cryptographic protocols through compositional analysis techniques. In Proceedings of the International Conference on Tools and Algorithms for the Construction and the Analysis of Systems (TACAS), 1999. 392
F. Martinelli. “Partial Model Checking and Theorem Proving for Ensuring Security Properties”. In Proceedings of the 11th Computer Security Foundation Workshop, (CSFW’98). IEEE press, 1998. 361, 392
D. McCullough. “Noninterference and the Composability of Security Properties”. In Proceedings, 1988 IEEE Symposium on Security and Privacy, pages 177–186. IEEE Computer Society Press, April 1988. 333, 376
J. K. Millen. “Hookup Security for Synchronous Machines”. In Proceedings of the Third Computer Security Foundation Workshop III. IEEE Computer Society Press, 1990. 333
R. Milner. Communication and Concurrency. Prentice-Hall, 1989. 333, 335, 337,339, 340, 343, 344, 361, 363, 364
J. C. Mitchell, M. Mitchell, and U. Stern. “Automated Analysis of Cryptographic Protocols Using Murø”. In Proceedings of the 1997 IEEE Symposium on Research in Security and Privacy, pages 141–153. IEEE Computer Society Press, 1997. 331
R. De Nicola and M. Hennessy. “Testing equivalences for processes”. Theoretical Computer Science, 34:83–133, 1984. 341, 348, 353
L. C. Paulson. “Proving Properties of Security Protocols by Induction”. In 10th Computer Security Foundations Workshop, pages 70–83. IEEE Computer Society Press, 1997. 331
G. Plotkin. “A Structural Approach to Operational Semantics”. Technical Report DAIMI-FN-19, Aarhus University, 1981. 334
A. W. Roscoe. “Model Checking CSP”. In A. W. Roscoe (ed) A Classical Mind. Prentice Hall, 1994. 368, 375
A.W. Roscoe, J. C. P. Woodcock, and L. Wulf. “Non-interference through Determinism”. In Proceeding of European Symposium on Research in Computer Security 1994 (ESORICS’94), pages 33–53. Springer-Verlag LNCS 875, 1994. 368, 369, 370,375
P. Y. A. Ryan. “A CSP Formulation of Non-Interference”. In Proceedings of the 1990 Computer Security Foundation Workshop III, Franconia, 1990. IEEE press.368
P. Y. A. Ryan. “Mathematical Models of Computer Security”. In this volume.376
S. Schneider. “Verifying authentication protocols in CSP”. IEEE Transactions on Software Engineering, 24(9), September 1998. 331,396.
G. Smith and D. M. Volpano. “Secure Information Flow in a Multi-Threaded Imperative Language”. In Proc. of POPL, pages 355–364, 1998. 331
L. J. Stockmeyer and A. R. Meyer. “Word problems requiring exponential time”. In Proceedings of the 5th ACM Symposium on Theory of Computing, pages 1–9, Austin, Texas, 1973. 355
D. Sutherland. “A Model of Information”. In Proceedings of the 9th National Computer Security Conference, pages 175–183. National Bureau of Standards and National Computer Security Center, September 1986. 333, 376
C. R. Tsai, V. D. Gligor, and C. S. Chandersekaran. “On the Identification of Covert Storage Channels in Secure Systems”. IEEE Transactions on Software Engineering, pages 569–580, June 1990. 332
J. T. Wittbold and D. M. Johnson. “Information Flow in Nondeterministic Systems”. In Proceedings of the 1990 IEEE Symposium on Research in Security and Privacy, pages 144–161. IEEE Computer Society Press, 1990. 333 bm 397 397
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Focardi, R., Gorrieri, R. (2001). Classification of Security Properties. In: Focardi, R., Gorrieri, R. (eds) Foundations of Security Analysis and Design. FOSAD 2000. Lecture Notes in Computer Science, vol 2171. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45608-2_6
Download citation
DOI: https://doi.org/10.1007/3-540-45608-2_6
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42896-1
Online ISBN: 978-3-540-45608-7
eBook Packages: Springer Book Archive