{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,2]],"date-time":"2026-01-02T07:42:28Z","timestamp":1767339748196,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540404385"},{"type":"electronic","value":"9783540450139"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/3-540-45013-0_16","type":"book-chapter","created":{"date-parts":[[2007,7,16]],"date-time":"2007-07-16T16:06:29Z","timestamp":1184601989000},"page":"199-218","source":"Crossref","is-referenced-by-count":8,"title":["A Proof System for Information Flow Security"],"prefix":"10.1007","author":[{"given":"Annalisa","family":"Bossi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Riccardo","family":"Focardi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Carla","family":"Piazza","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sabina","family":"Rossi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2003,6,24]]},"reference":[{"issue":"5","key":"16_CR1","doi-asserted-by":"publisher","first-page":"749","DOI":"10.1145\/324133.324266","volume":"46","author":"M. Abadi","year":"1999","unstructured":"M. Abadi. Secrecy by Typing in Security Protocols. Journal of the ACM, 46(5):749\u2013786, 1999.","journal-title":"Journal of the ACM"},{"issue":"1","key":"16_CR2","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1006\/inco.2000.3020","volume":"168","author":"C. Bodei","year":"2001","unstructured":"C. Bodei, P. Degano, F. Nielson, and H. Nielson. Static analysis for the pi-calculus with applications to security. Information and Computation, 168(1):68\u201392, 2001.","journal-title":"Information and Computation"},{"key":"16_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/3-540-45719-4_19","volume-title":"Int. Conference on Algebraic Methodology and Software Technology (AMAST\u201902)","author":"A. Bossi","year":"2002","unstructured":"A. Bossi, R. Focardi, C. Piazza, and S. Rossi. Transforming processes to ensure and check information flow security. In H. Kirchner and C. Ringeissen, editors, Int. Conference on Algebraic Methodology and Software Technology (AMAST\u201902), volume 2422 of LNCS, pages 271\u2013286. Springer, 2002."},{"key":"16_CR4","series-title":"Lect Notes Comput Sci","first-page":"96","volume-title":"Proc. of Computer Aided Verification","author":"A. Bouali","year":"1992","unstructured":"A. Bouali and R. de Simone. Symbolic Bisimulation Minimization. In Proc. of Computer Aided Verification, volume 663 of LNCS, pages 96\u2013108. Springer, 1992."},{"key":"16_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"382","DOI":"10.1007\/3-540-48224-5_32","volume-title":"Proc. of Int. Colloquium on Automata, Languages and Programming","author":"G. Boudol","year":"2001","unstructured":"G. Boudol and I. Castellani. Non-Interference for Concurrent Programs. In Proc. of Int. Colloquium on Automata, Languages and Programming, volume 2076 of LNCS, pages 382\u2013395. Springer, 2001."},{"key":"16_CR6","doi-asserted-by":"crossref","unstructured":"C. Braghin, A. Cortesi, and R. Focardi. Control Flow Analysis of Mobile Ambients with Security Boundaries. In Proc. of IFIPM Int. Conf. on Formal Methods for Open Object-Based Distributed Systems, pages 197\u2013212. Kluwer, 2002.","DOI":"10.1007\/978-0-387-35496-5_14"},{"key":"16_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"79","DOI":"10.1007\/3-540-44585-4_8","volume-title":"Proc. of Computer Aided Verification","author":"A. Dovier","year":"2001","unstructured":"A. Dovier, C. Piazza, and A. Policriti. A Fast Bisimulation Algorithm. In Proc. of Computer Aided Verification, volume 2102 of LNCS, pages 79\u201390. Springer, 2001."},{"key":"16_CR8","doi-asserted-by":"crossref","unstructured":"N. A. Durgin, J. C. Mitchell, and D. Pavlovic. A Compositional Logic for Protocol Correctness. In Proc. of Computer Security Foundations Workshop. IEEE, 2001.","DOI":"10.1109\/CSFW.2001.930150"},{"issue":"9","key":"16_CR9","doi-asserted-by":"publisher","first-page":"550","DOI":"10.1109\/32.629493","volume":"23","author":"R. Focardi","year":"1997","unstructured":"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\u2013571, 1997.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"16_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45608-2","volume-title":"Foundations of Security Analysis and Design","author":"R. Focardi","year":"2001","unstructured":"R. Focardi and R. Gorrieri. Classification of Security Properties (Part I: Information Flow). In R. Focardi and R. Gorrieri, editors, Foundations of Security Analysis and Design, volume 2171 of LNCS. Springer, 2001."},{"key":"16_CR11","doi-asserted-by":"crossref","unstructured":"R. Focardi and S. Rossi. Information Flow Security in Dynamic Contexts. In Proc. of 15th Computer Security Foundations Workshop, pages 307\u2013319. IEEE, 2002.","DOI":"10.1109\/CSFW.2002.1021825"},{"key":"16_CR12","doi-asserted-by":"crossref","unstructured":"J. A. Goguen and J. Meseguer. Security Policies and Security Models. In Proc. of the IEEE Symp. on Security and Privacy, pages 11\u201320. IEEE, 1982.","DOI":"10.1109\/SP.1982.10014"},{"key":"16_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1007\/3-540-45022-X_35","volume-title":"Proc. of Int. Colloquium on Automata, Languages and Programming (ICALP\u201900)","author":"M. Hennessy","year":"2000","unstructured":"M. Hennessy and J. Riely. Information Flow vs. Resource Access in the Asynchronous Pi-Calculus. In Proc. of Int. Colloquium on Automata, Languages and Programming (ICALP\u201900), volume 1853 of LNCS, pages 415\u2013427. Springer, 2000."},{"key":"16_CR14","doi-asserted-by":"crossref","unstructured":"D. Lee and M. Yannakakis. Online Minimization of Transition Systems. In Proc. of 24th Symp. on Theory of Computing, pages 264\u2013274. ACM, 1992.","DOI":"10.1145\/129712.129738"},{"key":"16_CR15","doi-asserted-by":"crossref","unstructured":"H. Mantel. Possibilistic Definitions of Security \u2014 An Assebly Kit-. In Proc. of the IEEE Symp. on Security and Privacy, pages 185\u2013199. IEEE, 2000.","DOI":"10.1109\/CSFW.2000.856936"},{"key":"16_CR16","series-title":"Lect Notes Comput Sci","volume-title":"Proc. of European Symp. on Research in Computer Security","author":"H. Mantel","year":"2000","unstructured":"H. Mantel. Unwinding Possibilistic Security Properties. In Proc. of European Symp. on Research in Computer Security, volume 2895 of LNCS. Springer, 2000."},{"key":"16_CR17","doi-asserted-by":"crossref","unstructured":"F. Martinelli. Partial Model Checking and Theorem Proving for Ensuring Security Properties. In Proc. Computer Security Foundations Workshop. IEEE, 1998.","DOI":"10.1109\/CSFW.1998.683154"},{"key":"16_CR18","doi-asserted-by":"crossref","unstructured":"D. McCullough. A Hookup Theorem for Multilevel Security. IEEE Transactions on Software Engineering, pages 563\u2013568, June 1990.","DOI":"10.1109\/32.55085"},{"key":"16_CR19","doi-asserted-by":"crossref","unstructured":"J. McLean. A General Theory of Composition for Trace Sets Closed under Selective Interleaving Functions. In Proc. Symp. on Security and Privacy, pages 79\u201393, 1994.","DOI":"10.1109\/RISP.1994.296590"},{"key":"16_CR20","doi-asserted-by":"crossref","unstructured":"J. K. Millen. Unwinding Forward Correctability. In Proc. of 7th Computer Security Foundations Workshop, pages 2\u201310. IEEE, 1994.","DOI":"10.1109\/CSFW.1994.315952"},{"key":"16_CR21","unstructured":"R. Milner. Communication and Concurrency. Prentice-Hall, 1989."},{"issue":"6","key":"16_CR22","doi-asserted-by":"publisher","first-page":"973","DOI":"10.1137\/0216062","volume":"16","author":"R. Paige","year":"1987","unstructured":"R. Paige and R. E. Tarjan. Three Partition Refinement Algorithms. SIAM Journal on Computing, 16(6):973\u2013989, 1987.","journal-title":"SIAM Journal on Computing"},{"key":"16_CR23","doi-asserted-by":"crossref","unstructured":"L. C. Paulson. Proving Properties of Security Protocols by Induction. In Proc. of 10th Computer Security Foundations Workshop, pages 70\u201383. IEEE, 1997.","DOI":"10.1109\/CSFW.1997.596788"},{"key":"16_CR24","unstructured":"J. Rushby. Noninterference, Transitivity, and Channel-Control Security Policies. Technical Report Technical Report CSL-92-02, SRI International, December 1992."},{"key":"16_CR25","doi-asserted-by":"crossref","unstructured":"A. Sabelfeld and D. Sands. Probabilistic Noninterference for Multi-threaded Programs. In Proc. of Computer Security Foundations Workshop. IEEE, 2000.","DOI":"10.1109\/CSFW.2000.856937"},{"key":"16_CR26","doi-asserted-by":"crossref","unstructured":"S. Schneider. Verifying Authentication Protocols in CSP. IEEE Transactions on Software Engineering, 24(9), 1998.","DOI":"10.1109\/32.713329"},{"key":"16_CR27","unstructured":"V. Shmatikov and J. C. Mitchell. Analysis of a Fair Exchange Protocol. In Proc. of 7th Annual Symp. on Network and Distributed System Security, pages 119\u2013128. Internet Society, 2000."},{"key":"16_CR28","doi-asserted-by":"crossref","unstructured":"G. Smith and D. M. Volpano. Secure Information Flow in a Multi-threaded Imperative Language. In Proc. of 25th Symp. on Principles of Programming Languages, pages 355\u2013364. ACM, 1998.","DOI":"10.1145\/268946.268975"}],"container-title":["Lecture Notes in Computer Science","Logic Based Program Synthesis and Transformation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45013-0_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,19]],"date-time":"2025-01-19T11:48:10Z","timestamp":1737287290000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45013-0_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540404385","9783540450139"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/3-540-45013-0_16","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2003]]}}}