{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T04:58:21Z","timestamp":1725512301403},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540714095"},{"type":"electronic","value":"9783540714101"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-71410-1_8","type":"book-chapter","created":{"date-parts":[[2007,5,21]],"date-time":"2007-05-21T10:57:52Z","timestamp":1179745072000},"page":"94-110","source":"Crossref","is-referenced-by-count":6,"title":["Combining Different Proof Techniques for Verifying Information Flow Security"],"prefix":"10.1007","author":[{"given":"Heiko","family":"Mantel","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Henning","family":"Sudbrock","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tina","family":"Krau\u00dfer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"8_CR1","first-page":"155","volume-title":"IEEE Computer Security Foundations Workshop","author":"A. Banerjee","year":"2003","unstructured":"Banerjee, A., Naumann, D.A.: Using Access Control for Secure Information Flow in a Java-like Language. In: IEEE Computer Security Foundations Workshop, pp. 155\u2013169. IEEE Computer Society Press, Los Alamitos (2003)"},{"key":"8_CR2","doi-asserted-by":"publisher","first-page":"100","DOI":"10.1109\/CSFW.2004.1310735","volume-title":"IEEE Computer Security Foundations Workshop","author":"G. Barthe","year":"2004","unstructured":"Barthe, G., D\u2019Argenio, P.R., Rezk, T.: Secure Information Flow by Self-Composition. In: IEEE Computer Security Foundations Workshop, pp. 100\u2013114. IEEE Computer Society Press, Los Alamitos (2004)"},{"key":"8_CR3","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1145\/1040294.1040304","volume-title":"ACM SIGPLAN International Workshop on Types in Languages Design and Implementation","author":"G. Barthe","year":"2005","unstructured":"Barthe, G., Rezk, T.: Non-Interference for a JVM-like Language. In: ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, pp. 103\u2013112. ACM Press, New York (2005)"},{"key":"8_CR4","doi-asserted-by":"crossref","unstructured":"Bossi, A., Focardi, R., Piazza, C., Rossi, S.: Unwinding in Information Flow Security. In: ENTCS 99, pp. 127\u2013154 (2004)","DOI":"10.1016\/j.entcs.2004.02.006"},{"key":"8_CR5","first-page":"14","volume-title":"IEEE Computer Security Foundations Workshop","author":"A. Bossi","year":"2003","unstructured":"Bossi, A., Macedonio, D., Piazza, C., Rossi, S.: Secure Contexts for Confidential Data. In: IEEE Computer Security Foundations Workshop, pp. 14\u201325. IEEE Computer Society Press, Los Alamitos (2003)"},{"issue":"1-2","key":"8_CR6","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1016\/S0304-3975(02)00010-5","volume":"281","author":"G. Boudol","year":"2002","unstructured":"Boudol, G., Castellani, I.: Noninterference for Concurrent Programs and Thread Systems. Theoretical Computer Science\u00a0281(1-2), 109\u2013130 (2002)","journal-title":"Theoretical Computer Science"},{"key":"8_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1007\/978-3-540-32004-3_20","volume-title":"Security in Pervasive Computing","author":"\u00c1. Darvas","year":"2005","unstructured":"Darvas, \u00c1., H\u00e4hnle, R., Sands, D.: A Theorem Proving Approach to Analysis of Secure Information Flow. In: Hutter, D., Ullmann, M. (eds.) SPC 2005. LNCS, vol.\u00a03450, pp. 193\u2013209. Springer, Heidelberg (2005)"},{"key":"8_CR8","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1109\/CSFW.2004.1310736","volume-title":"IEEE Computer Security Foundations Workshop","author":"Z. Deng","year":"2004","unstructured":"Deng, Z., Smith, G.: Lenient Array Operations for Practical Secure Information Flow. In: IEEE Computer Security Foundations Workshop, pp. 115\u2013124. IEEE Computer Society Press, Los Alamitos (2004)"},{"key":"8_CR9","volume-title":"Cryptography and Data Security","author":"D.E. Denning","year":"1982","unstructured":"Denning, D.E.: Cryptography and Data Security. Addison-Wesley, Reading (1982)"},{"issue":"7","key":"8_CR10","doi-asserted-by":"publisher","first-page":"504","DOI":"10.1145\/359636.359712","volume":"20","author":"D.E. Denning","year":"1977","unstructured":"Denning, D.E., Denning, P.J.: Certification of Programs for Secure Information Flow. Communications of the ACM\u00a020(7), 504\u2013513 (1977)","journal-title":"Communications of the ACM"},{"issue":"1","key":"8_CR11","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":"8_CR12","first-page":"11","volume-title":"IEEE Symposium on Security and Privacy","author":"J.A. Goguen","year":"1982","unstructured":"Goguen, J.A., Meseguer, J.: Security Policies and Security Models. In: IEEE Symposium on Security and Privacy, pp. 11\u201320. IEEE Computer Society Press, Los Alamitos (1982)"},{"key":"8_CR13","first-page":"75","volume-title":"IEEE Symposium on Security and Privacy","author":"J.A. Goguen","year":"1984","unstructured":"Goguen, J.A., Meseguer, J.: Inference Control and Unwinding. In: IEEE Symposium on Security and Privacy, pp. 75\u201386. IEEE Computer Society Press, Los Alamitos (1984)"},{"key":"8_CR14","unstructured":"Knudsen, J.: Networking, User Experience, and Threads (2002), \n                    \n                      http:\/\/developers.sun.com\/techtopics\/mobility\/midp\/articles\/threading\/"},{"key":"8_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1007\/11679219_5","volume-title":"Formal Aspects in Security and Trust","author":"B. K\u00f6pf","year":"2006","unstructured":"K\u00f6pf, B., Mantel, H.: Eliminating Implicit Information Leaks by Transformational Typing and Unification. In: Dimitrakos, T., Martinelli, F., Ryan, P.Y.A., Schneider, S. (eds.) FAST 2005. LNCS, vol.\u00a03866, pp. 47\u201362. Springer, Heidelberg (2006)"},{"key":"8_CR16","unstructured":"Mahmoud, Q.H.: Preventing Screen Lockups of Blocking Operations (2004), \n                    \n                      http:\/\/developers.sun.com\/techtopics\/mobility\/midp\/ttips\/screenlock\/"},{"key":"8_CR17","first-page":"185","volume-title":"IEEE Computer Security Foundations Workshop","author":"H. Mantel","year":"2000","unstructured":"Mantel, H.: Possibilistic Definitions of Security \u2013 An Assembly Kit. In: IEEE Computer Security Foundations Workshop, pp. 185\u2013199. IEEE Computer Society Press, Los Alamitos (2000)"},{"key":"8_CR18","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":"8_CR19","first-page":"161","volume-title":"IEEE Symposium on Security and Privacy","author":"D. McCullough","year":"1987","unstructured":"McCullough, D.: Specifications for Multi-Level Security and a Hook-Up Property. In: IEEE Symposium on Security and Privacy, pp. 161\u2013166. IEEE Computer Society Press, Los Alamitos (1987)"},{"key":"8_CR20","first-page":"79","volume-title":"IEEE Symposium on Research in Security and Privacy","author":"J.D. McLean","year":"1994","unstructured":"McLean, J.D.: A General Theory of Composition for Trace Sets Closed under Selective Interleaving Functions. In: IEEE Symposium on Research in Security and Privacy, pp. 79\u201393. IEEE Computer Society Press, Los Alamitos (1994)"},{"key":"8_CR21","first-page":"84","volume-title":"IEEE Symposium on Research in Security and Privacy","author":"J.K. Millen","year":"1990","unstructured":"Millen, J.K.: Hookup Security for Synchronous Machines. In: IEEE Symposium on Research in Security and Privacy, pp. 84\u201390. IEEE Computer Society Press, Los Alamitos (1990)"},{"key":"8_CR22","unstructured":"C. P\u00f6pper. A Security Analyzer for Multi-Threaded Programs. Diploma thesis, ETH Zurich, March (2005)"},{"key":"8_CR23","first-page":"114","volume-title":"IEEE Symposium on Security and Privacy","author":"A.W. Roscoe","year":"1995","unstructured":"Roscoe, A.W.: CSP and Determinism in Security Modelling. In: IEEE Symposium on Security and Privacy, pp. 114\u2013127. IEEE Computer Society Press, Los Alamitos (1995)"},{"key":"8_CR24","unstructured":"Rushby, J.M.: Noninterference, Transitivity, and Channel-Control Security Policies. Technical Report CSL-92-02, SRI International (1992)"},{"key":"8_CR25","volume-title":"IEEE Computer Security Foundations Workshop","author":"A. Russo","year":"2006","unstructured":"Russo, A., Sabelfeld, A.: Securing Interaction between Threads and the Scheduler. In: IEEE Computer Security Foundations Workshop, IEEE Computer Society Press, Los Alamitos (2006)"},{"key":"8_CR26","doi-asserted-by":"crossref","first-page":"214","DOI":"10.1109\/CSFW.1999.779775","volume-title":"IEEE Computer Security Foundations Workshop","author":"P.Y.A. Ryan","year":"1999","unstructured":"Ryan, P.Y.A., Schneider, S.A.: Process Algebra and Non-interference. In: IEEE Computer Security Foundations Workshop, pp. 214\u2013227. IEEE Computer Society Press, Los Alamitos (1999)"},{"key":"8_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"260","DOI":"10.1007\/978-3-540-39866-0_27","volume-title":"Perspectives of System Informatics","author":"A. Sabelfeld","year":"2004","unstructured":"Sabelfeld, A.: Confidentiality for Multithreaded Programs via Bisimulation. In: Broy, M., Zamulin, A.V. (eds.) PSI 2003. LNCS, vol.\u00a02890, pp. 260\u2013274. Springer, Heidelberg (2004)"},{"issue":"1","key":"8_CR28","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1109\/JSAC.2002.806121","volume":"21","author":"A. Sabelfeld","year":"2003","unstructured":"Sabelfeld, A., Myers, A.C.: Language-based Information-Flow Security. IEEE Journal on Selected Areas in Communication\u00a021(1), 5\u201319 (2003)","journal-title":"IEEE Journal on Selected Areas in Communication"},{"key":"8_CR29","first-page":"200","volume-title":"IEEE Computer Security Foundations Workshop","author":"A. Sabelfeld","year":"2000","unstructured":"Sabelfeld, A., Sands, D.: Probabilistic Noninterference for Multi-threaded Programs. In: IEEE Computer Security Foundations Workshop, pp. 200\u2013215. IEEE Computer Society Press, Los Alamitos (2000)"},{"key":"8_CR30","first-page":"3","volume-title":"IEEE Computer Security Foundations Workshop","author":"G. Smith","year":"2003","unstructured":"Smith, G.: Probabilistic Noninterference through Weak Probabilistic Bisimulation. In: IEEE Computer Security Foundations Workshop, pp. 3\u201313. IEEE Computer Society Press, Los Alamitos (2003)"},{"key":"8_CR31","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1145\/268946.268975","volume-title":"ACM Symposium on Principles of Programming Languages","author":"G. Smith","year":"1998","unstructured":"Smith, G., Volpano, D.: Secure Information Flow in a Multi-threaded Imperative Language. In: ACM Symposium on Principles of Programming Languages, pp. 355\u2013364. ACM Press, New York (1998)"},{"key":"8_CR32","first-page":"34","volume-title":"IEEE Computer Security Foundations Workshop","author":"D. Volpano","year":"1998","unstructured":"Volpano, D., Smith, G.: Probabilistic Noninterference in a Concurrent Language. In: IEEE Computer Security Foundations Workshop, pp. 34\u201343. IEEE Computer Society Press, Los Alamitos (1998)"},{"key":"8_CR33","first-page":"29","volume-title":"IEEE Computer Security Foundations Workshop","author":"S. Zdancewic","year":"2003","unstructured":"Zdancewic, S., Myers, A.C.: Observational Determinism for Concurrent Program Security. In: IEEE Computer Security Foundations Workshop, pp. 29\u201343. IEEE Computer Society Press, Los Alamitos (2003)"}],"container-title":["Lecture Notes in Computer Science","Logic-Based Program Synthesis and Transformation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-71410-1_8.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T05:19:47Z","timestamp":1605763187000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-71410-1_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540714095","9783540714101"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-71410-1_8","relation":{},"subject":[]}}