{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T17:38:26Z","timestamp":1725557906254},"publisher-location":"Berlin, Heidelberg","reference-count":50,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540250517"},{"type":"electronic","value":"9783540322542"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/978-3-540-32254-2_26","type":"book-chapter","created":{"date-parts":[[2010,6,22]],"date-time":"2010-06-22T15:16:54Z","timestamp":1277219814000},"page":"452-475","source":"Crossref","is-referenced-by-count":0,"title":["Exploiting Generic Aspects of Security Models in Formal Developments"],"prefix":"10.1007","author":[{"given":"Heiko","family":"Mantel","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Axel","family":"Schairer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"1","key":"26_CR1","first-page":"66","volume":"3","author":"S. Autexier","year":"2000","unstructured":"Autexier, S., Hutter, D., Langenstein, B., Mantel, H., Rock, G., Schairer, A., Stephan, W., Vogt, R., Wolpers, A.: VSE: Formal Methods Meet Industrial Needs. Special Issue on Mechanized Theorem Proving for Technology Transfer of the STTT-Springer International Journal on Software Tools for Technology Transfer\u00a03(1), 66\u201377 (2000)","journal-title":"Special Issue on Mechanized Theorem Proving for Technology Transfer of the STTT-Springer International Journal on Software Tools for Technology Transfer"},{"key":"26_CR2","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1007\/3-540-48660-7_15","volume-title":"Automated Deduction - CADE-16","author":"S. Autexier","year":"1999","unstructured":"Autexier, S., Hutter, D., Mantel, H., Schairer, A.: System Description: INKA 5.0 \u2013 A Logic Voyager. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol.\u00a01632, pp. 207\u2013211. Springer, Heidelberg (1999)"},{"key":"26_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"495","DOI":"10.1007\/3-540-45719-4_34","volume-title":"Algebraic Methodology and Software Technology","author":"S. Autexier","year":"2002","unstructured":"Autexier, S., Hutter, D., Mossakowski, T., Schairer, A.: The Development Graph Manager MAYA. In: Kirchner, H., Ringeissen, C. (eds.) AMAST 2002. LNCS, vol.\u00a02422, p. 495. Springer, Heidelberg (2002)"},{"key":"26_CR4","unstructured":"Biba, K.J.: Integrity Considerations for Secure Computer Systems. Technical Report MTR-3153, MITRE (1977)"},{"key":"26_CR5","doi-asserted-by":"crossref","unstructured":"Bell, D.E., LaPadula, L.: Secure Computer Systems: Unified Exposition and Multics Interpretation. Technical Report MTR-2997, MITRE (March 1976)","DOI":"10.21236\/ADA023588"},{"key":"#cr-split#-26_CR6.1","unstructured":"Common Criteria Project Sponsoring Organisations. Common Criteria for Information Technology Security Evaluation (CC) Version 2.1(1999);"},{"key":"#cr-split#-26_CR6.2","unstructured":"Also appeared as ISO\/IEC 15408: IT ??? Security techniques ??? Evaluation criteria for IT security"},{"issue":"1","key":"26_CR7","doi-asserted-by":"crossref","first-page":"5","DOI":"10.3233\/JCS-1994\/1995-3103","volume":"3","author":"R. Focardi","year":"1995","unstructured":"Focardi, R., Gorrieri, R.: A Classification of Security Properties for Process Algebras. Journal of Computer Security\u00a03(1), 5\u201333 (1995)","journal-title":"Journal of Computer Security"},{"key":"26_CR8","unstructured":"Focardi, R., Ghelli, A., Gorrieri, R.: Using Non Interference for the Analysis of Security Protocols. In: Proceedings of DIMACS Workshop on Design and Formal Verification of Security Protocols (1997)"},{"key":"26_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"354","DOI":"10.1007\/3-540-45022-X_31","volume-title":"Automata, Languages and Programming","author":"R. Focardi","year":"2000","unstructured":"Focardi, R., Gorrieri, R., Martinelli, F.: Non Interference for the Analysis of Cryptographic Protocols. In: Welzl, E., Montanari, U., Rolim, J.D.P. (eds.) ICALP 2000. LNCS, vol.\u00a01853, p. 354. Springer, Heidelberg (2000)"},{"key":"26_CR10","doi-asserted-by":"crossref","unstructured":"Goguen, J.A., Meseguer, J.: Security Policies and Security Models. In: Proceedings of the IEEE Symposium on Security and Privacy, pp. 11\u201320 (1982)","DOI":"10.1109\/SP.1982.10014"},{"key":"26_CR11","doi-asserted-by":"crossref","unstructured":"Goguen, J.A., Meseguer, J.: Inference Control and Unwinding. In: Proceedings of the IEEE Symposium on Security and Privacy, pp. 75\u201386 (1984)","DOI":"10.1109\/SP.1984.10019"},{"key":"26_CR12","unstructured":"Guttman, J.D., Nadel, M.E.: What Needs Securing? In: Proceedings of the IEEE Computer Security Foundations Workshop, pp. 34\u201357 (1988)"},{"key":"26_CR13","volume-title":"Communicating Sequential Processes","author":"C.A.R. Hoare","year":"1985","unstructured":"Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985)"},{"issue":"2","key":"26_CR14","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1109\/TSE.1987.226478","volume":"SE-13","author":"J.T. Haigh","year":"1987","unstructured":"Haigh, J.T., Young, W.D.: Extending the Noninterference Version of MLS for SAT. IEEE Transactions on Software Engineering\u00a0SE-13(2), 141\u2013150 (1987)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"26_CR15","unstructured":"Office for Official Publications of the European Communities. Information Technology Security Evaluation Criteria, ITSEC (1991)"},{"key":"26_CR16","doi-asserted-by":"crossref","unstructured":"Jacob, J.: On the Derivation of Secure Components. In: Proceedings of the IEEE Symposium on Security and Privacy, pp. 242\u2013247 (1989)","DOI":"10.1109\/SECPRI.1989.36298"},{"key":"26_CR17","unstructured":"Johnson, D.M., Thayer, F.J.: Security and the Composition of Machines. In: Proceedings of the Computer Security Foundations Workshop, pp. 72\u201389 (1988)"},{"key":"26_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"395","DOI":"10.1007\/3-540-44618-4_29","volume-title":"CONCUR 2000 - Concurrency Theory","author":"J. J\u00fcrjens","year":"2000","unstructured":"J\u00fcrjens, J.: Secure Information Flow for Concurrent Processes. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol.\u00a01877, pp. 395\u2013409. Springer, Heidelberg (2000)"},{"key":"26_CR19","unstructured":"Lampson, B.W.: Protection. In: Proceedings of 5th Princeton Conference on Information Sciences and Systems, p. 437 (1971)"},{"issue":"10","key":"26_CR20","doi-asserted-by":"publisher","first-page":"613","DOI":"10.1145\/362375.362389","volume":"16","author":"B.W. Lampson","year":"1973","unstructured":"Lampson, B.W.: A Note on the Confinement Problem. Communications of the ACS\u00a016(10), 613\u2013615 (1973)","journal-title":"Communications of the ACS"},{"key":"26_CR21","doi-asserted-by":"crossref","unstructured":"Mantel, H.: Possibilistic Definitions of Security \u2013 An Assembly Kit. In: Proceedings of the IEEE Computer Security Foundations Workshop, pp. 185\u2013199 (2000)","DOI":"10.1109\/CSFW.2000.856936"},{"key":"26_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"238","DOI":"10.1007\/10722599_15","volume-title":"Computer Security - ESORICS 2000","author":"H. Mantel","year":"2000","unstructured":"Mantel, H.: Unwinding Possibilistic Security Properties. In: Cuppens, F., Deswarte, Y., Gollmann, D., Waidner, M. (eds.) ESORICS 2000. LNCS, vol.\u00a01895, pp. 238\u2013254. Springer, Heidelberg (2000)"},{"key":"26_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1007\/3-540-45251-6_9","volume-title":"FME 2001: Formal Methods for Increasing Software Productivity","author":"H. Mantel","year":"2001","unstructured":"Mantel, H.: Information Flow Control and Applications \u2013 Bridging a Gap. In: Oliveira, J.N., Zave, P. (eds.) FME 2001. LNCS, vol.\u00a02021, pp. 153\u2013172. Springer, Heidelberg (2001)"},{"key":"26_CR24","doi-asserted-by":"crossref","unstructured":"Mantel, H.: Preserving Information Flow Properties under Refinement. In: Proceedings of the IEEE Symposium on Security and Privacy, pp. 78\u201391 (2001)","DOI":"10.1109\/SECPRI.2001.924289"},{"key":"26_CR25","doi-asserted-by":"crossref","unstructured":"Mantel, H.: On the Composition of Secure Systems. In: Proceedings of the IEEE Symposium on Security and Privacy, pp. 88\u2013101 (2002)","DOI":"10.1109\/SECPRI.2002.1004364"},{"key":"26_CR26","doi-asserted-by":"crossref","unstructured":"McCullough, D.: Specifications for Multi-Level Security and a Hook-Up Property. In: Proceedings of the IEEE Symposium on Security and Privacy, pp. 161\u2013166 (1987)","DOI":"10.1109\/SP.1987.10009"},{"key":"26_CR27","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1016\/0020-0190(85)90065-1","volume":"20","author":"J.D. McLean","year":"1985","unstructured":"McLean, J.D.: A Comment on the \u201dBasic Security Theorem\u201d of Bell and LaPadula. Information Processing Letters\u00a020, 67\u201370 (1985)","journal-title":"Information Processing Letters"},{"key":"26_CR28","doi-asserted-by":"crossref","unstructured":"McLean, J.D.: Reasoning about Security Models. In: Proceedings of the IEEE Symposium on Security and Privacy, pp. 123\u2013131 (1987)","DOI":"10.21236\/ADA465058"},{"issue":"1","key":"26_CR29","doi-asserted-by":"crossref","first-page":"9","DOI":"10.1109\/2.48795","volume":"23","author":"J.D. McLean","year":"1990","unstructured":"McLean, J.D.: The Specification and Modeling of Computer Security. IEEE Computer\u00a023(1), 9\u201316 (1990)","journal-title":"IEEE Computer"},{"issue":"1","key":"26_CR30","doi-asserted-by":"crossref","first-page":"37","DOI":"10.3233\/JCS-1992-1103","volume":"1","author":"J.D. McLean","year":"1992","unstructured":"McLean, J.D.: Proving Noninterference and Functional Correctness using Traces. Journal of Computer Security\u00a01(1), 37\u201357 (1992)","journal-title":"Journal of Computer Security"},{"key":"26_CR31","doi-asserted-by":"crossref","unstructured":"McLean, J.D.: 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\u201393 (1994)","DOI":"10.1109\/RISP.1994.296590"},{"key":"26_CR32","volume-title":"Encyclopedia of Software Engineering","author":"J.D. McLean","year":"1994","unstructured":"McLean, J.D.: Security Models. In: Marciniak, J. (ed.) Encyclopedia of Software Engineering. John Wiley & Sons, Inc., Chichester (1994)"},{"key":"26_CR33","doi-asserted-by":"crossref","unstructured":"Millen, J.K.: Unwinding Forward Correctability. In: Proceedings of the Computer Security Foundations Workshop, pp. 2\u201310 (1994)","DOI":"10.1109\/CSFW.1994.315952"},{"key":"26_CR34","unstructured":"Mantel, H., Schairer, A., Kabatnik, M., Kreutzer, M., Zugenmaier, A.: Using Information Flow Control to Evaluate Access Protection of Location Information in Mobile Communication Networks. Technical Report 159, CS Department, University of Freiburg (2001)"},{"key":"26_CR35","unstructured":"O\u2019Halloran, C.: A Calculus of Information Flow. In: Proceedings of the European Symposium on Research in Computer Security (ESORICS), pp. 147\u2013159 (1990)"},{"key":"26_CR36","doi-asserted-by":"crossref","unstructured":"Pinsky, S.: Absorbing Covers and Intransitive Non-Interference. In: Proceedings of the IEEE Symposium on Security and Privacy, pp. 102\u2013113 (1995)","DOI":"10.1109\/SECPRI.1995.398926"},{"key":"26_CR37","doi-asserted-by":"crossref","unstructured":"Roscoe, A.W., Goldsmith, M.H.: What is intransitive noninterference? In: Proceedings of the 12th IEEE Computer Security Foundations Workshop, pp. 228\u2013238 (1999)","DOI":"10.1109\/CSFW.1999.779776"},{"key":"26_CR38","doi-asserted-by":"crossref","unstructured":"Roscoe, A.W.: CSP and Determinism in Security Modelling. In: Proceedings of the IEEE Symposium on Security and Privacy, pp. 114\u2013127 (1995)","DOI":"10.1109\/SECPRI.1995.398927"},{"key":"26_CR39","doi-asserted-by":"crossref","unstructured":"Ryan, P.Y.A., Schneider, S.A.: Process Algebra and Non-interference. In: Proceedings of the 12th IEEE Computer Security Foundations Workshop, pp. 214\u2013227 (1999)","DOI":"10.1109\/CSFW.1999.779775"},{"key":"26_CR40","unstructured":"Rushby, J.: Noninterference, Transitivity, and Channel-Control Security Policies. Technical Report CSL-92-02, SRI International (1992)"},{"key":"26_CR41","doi-asserted-by":"crossref","unstructured":"Roscoe, A.W., Wulf, L.: Composing and Decomposing Systems under Security Properties. In: Proceedings of the 8th IEEE Computer Security Foundations Workshop, pp. 9\u201315 (1995)","DOI":"10.1109\/CSFW.1995.518547"},{"key":"26_CR42","unstructured":"Ryan, P.Y.A.: A CSP Formulation of Non-Interference and Unwinding. Cipher, 19\u201330 (Winter 1991)"},{"key":"26_CR43","unstructured":"Schneider, S.: May Testing, Non-interference, and Compositionality. Technical Report CSD-TR-00-02, Royal Holloway, University of London (2001)"},{"key":"26_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/10722599_2","volume-title":"Computer Security - ESORICS 2000","author":"G. Schellhorn","year":"2000","unstructured":"Schellhorn, G., Reif, W., Schairer, A., Karger, P., Austel, V., Toll, D.: Verification of a Formal Security Model for Multiapplicative Smart Cards. In: Cuppens, F., Deswarte, Y., Gollmann, D., Waidner, M. (eds.) ESORICS 2000. LNCS, vol.\u00a01895, pp. 17\u201336. Springer, Heidelberg (2000)"},{"key":"26_CR45","unstructured":"Sutherland, D.: A Model of Information. In: 9th National Computer Security Conference (1986)"},{"key":"26_CR46","doi-asserted-by":"crossref","unstructured":"Wittbold, J.T., Johnson, D.M.: Information Flow in Nondeterministic Systems. In: Proceedings of the IEEE Symposium on Research in Security and Privacy, pp. 144\u2013161 (1990)","DOI":"10.1109\/RISP.1990.63846"},{"key":"26_CR47","unstructured":"Zakinthinos, A.: On the Composition of Security Properties. PhD thesis, Graduate Department of Electrical and Computer Engineering, University of Toronto (1996)"},{"key":"26_CR48","doi-asserted-by":"crossref","unstructured":"Zakinthinos, A., Lee, E.S.: A General Theory of Security Properties. In: Proceedings of the IEEE Symposium on Security and Privacy, pp. 94\u2013102 (1997)","DOI":"10.1109\/SECPRI.1997.601322"},{"key":"26_CR49","doi-asserted-by":"crossref","unstructured":"Zakinthinos, A., Lee, E.S.: Composing Secure Systems that have Emergent Properties. In: Proceedings of the 11th IEEE Computer Security Foundations Workshop, pp. 117\u2013122 (1998)","DOI":"10.1109\/CSFW.1998.683161"}],"container-title":["Lecture Notes in Computer Science","Mechanizing Mathematical Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-32254-2_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T05:37:44Z","timestamp":1559194664000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-32254-2_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540250517","9783540322542"],"references-count":50,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-32254-2_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}