{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,7]],"date-time":"2026-02-07T00:19:40Z","timestamp":1770423580885,"version":"3.49.0"},"reference-count":50,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2001,3,1]],"date-time":"2001-03-01T00:00:00Z","timestamp":983404800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2001,3,1]],"date-time":"2001-03-01T00:00:00Z","timestamp":983404800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Higher-Order and Symbolic Computation"],"published-print":{"date-parts":[[2001,3]]},"DOI":"10.1023\/a:1011553200337","type":"journal-article","created":{"date-parts":[[2002,12,23]],"date-time":"2002-12-23T10:55:34Z","timestamp":1040640934000},"page":"59-91","source":"Crossref","is-referenced-by-count":124,"title":["A Per Model of Secure Information Flow in Sequential Programs"],"prefix":"10.1007","volume":"14","author":[{"given":"Andrei","family":"Sabelfeld","sequence":"first","affiliation":[]},{"given":"David","family":"Sands","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"323060_CR1","doi-asserted-by":"crossref","unstructured":"Abadi, M., Banerjee, A., Heintze, N., and Riecke, J. A core calculus of dependency. In POPL '99, Proceedings of the 26th Annual ACM Symposium on Principles of Programming Languages (January 1999), 1999.","DOI":"10.1145\/292540.292555"},{"key":"323060_CR2","doi-asserted-by":"crossref","unstructured":"Abadi, M. and Plotkin, G. A per model of polymorphism and recursive types. In Proceedings of the Fifth Annual Symposium on Logic in Computer Science, 1990, pp. 355-365.","DOI":"10.1109\/LICS.1990.113761"},{"issue":"1","key":"323060_CR3","doi-asserted-by":"crossref","first-page":"56","DOI":"10.1145\/357084.357088","volume":"2","author":"G.R. Andrews","year":"1980","unstructured":"Andrews, G.R. and Reitman, R.P. An axiomatic approach to information flow in programs. ACM TOPLAS\n2(1) (1980) 56-75.","journal-title":"ACM TOPLAS"},{"key":"323060_CR4","doi-asserted-by":"crossref","unstructured":"Ban\u00e2 tre, J.-P., Bryce, C., and Le M\u00e9tayer, D. Compile-time detection of information flow in sequential programs. In Computer Security-ESORICS '94, 3rd European Symposium on Research in Computer Security, 1994, D. Gollmann (Ed.). pp. 55-73. Vol. 875 of Lecture Notes in Computer Science.","DOI":"10.1007\/3-540-58618-0_56"},{"key":"323060_CR5","doi-asserted-by":"crossref","DOI":"10.21236\/ADA023588","volume-title":"Secure computer systems: Unified exposition and multics interpretation","author":"D. Bell","year":"1976","unstructured":"Bell, D. and LaPadula, L. Secure computer systems: Unified exposition and multics interpretation. MTR-2997, Rev. 1, The MITRE Corporation, Bedford, Mass, 1976."},{"issue":"5","key":"323060_CR6","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1145\/1067625.806556","volume":"11","author":"E.S. Cohen","year":"1977","unstructured":"Cohen, E.S. Information transmission in computational systems. ACM SIGOPS Operating Systems Review\n11(5) (1977) 133-139.","journal-title":"ACM SIGOPS Operating Systems Review"},{"key":"323060_CR7","unstructured":"Cohen, E.S. Information transmission in sequential programs. In Foundations of Secure Computation, R.A. DeMillo, D.P. Dobkin, A.K. Jones, and R.J. Lipton (Eds.). Academic Press, 1978, pp. 297-335."},{"key":"323060_CR8","doi-asserted-by":"crossref","unstructured":"Das, M., Reps, T., and Hentenryck, P.V. Semantic foundations of binding-time analysis for imperative programs. Partial Evaluation and Seman-tics-Based Program Manipulation. La Jolla, California, 1995, pp. 100-110.","DOI":"10.1145\/215465.215569"},{"issue":"5","key":"323060_CR9","doi-asserted-by":"crossref","first-page":"236","DOI":"10.1145\/360051.360056","volume":"19","author":"D.E. Denning","year":"1976","unstructured":"Denning, D.E. A lattice model of secure information flow. Communications of the ACM\n19(5) (1976) 236-243.","journal-title":"Communications of the ACM"},{"issue":"7","key":"323060_CR10","doi-asserted-by":"crossref","first-page":"504","DOI":"10.1145\/359636.359712","volume":"20","author":"D.E. Denning","year":"1977","unstructured":"Denning, D.E. and Denning, P.J. Certification of programs for secure information flow. Communications of the ACM\n20(7) (1977) 504-513.","journal-title":"Communications of the ACM"},{"issue":"1","key":"323060_CR11","doi-asserted-by":"crossref","first-page":"5","DOI":"10.3233\/JCS-1994\/1995-3103","volume":"3","author":"R. Focardi","year":"1994","unstructured":"Focardi, R. and Gorrieri, R. A classification of security properties for process algebra. J. Computer Security\n3(1) (1994) 5-33.","journal-title":"J. Computer Security"},{"key":"323060_CR12","doi-asserted-by":"crossref","unstructured":"Goguen, J. and Meseguer, J. Security policies and security models. In Proceedings of the IEEE Symposium on Security and Privacy, 1982.","DOI":"10.1109\/SP.1982.10014"},{"key":"323060_CR13","doi-asserted-by":"crossref","unstructured":"Gray III, J. Probabilistic interference. In Proceedings of the IEEE Symposium on Security and Privacy, Oakland, California, 1990, pp. 170-179.","DOI":"10.1109\/RISP.1990.63848"},{"key":"323060_CR14","doi-asserted-by":"crossref","unstructured":"Hankin, C.L. and Le M\u00e9tayer, D. A type-based framework for program analysis. In Proceedings of the First Static Analysis Symposium, 1994. Vol. 864 of LNCS.","DOI":"10.1007\/3-540-58485-4_53"},{"key":"323060_CR15","doi-asserted-by":"crossref","unstructured":"Heintze, N. and Riecke, J.G. The slam calculus: Programming with secrecy and integrity. In Conference Record of POPL'98: The 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Diego, California 1998, pp. 365-377.","DOI":"10.1145\/268946.268976"},{"key":"323060_CR16","doi-asserted-by":"crossref","unstructured":"Henglein, F. and Sands, D. A semantic model of binding times for safe partial evaluation. In Proc. Programming Languages: Implementations, Logics and Programs (PLILP), Utrecht, The Netherlands, M. Hermenegildo and S.D. Swierstra (Eds.). 1995, pp. 299-320. Vol. 982 of Lecture Notes in Computer Science.","DOI":"10.1007\/BFb0026827"},{"key":"323060_CR17","unstructured":"Hunt, L.S. Abstract interpretation of functional languages: From theory to practice. Ph.D. thesis, Department of Computing, Imperial College of Science, Technology and Medicine, 1991."},{"key":"323060_CR18","unstructured":"Hunt, S. PERs generalise projections for strictness analysis. In Draft Proceedings of the third glasgow Functional Programming Workshop. Ullapool, 1900."},{"key":"323060_CR19","doi-asserted-by":"crossref","unstructured":"Hunt, S. and Sands, D. Binding time analysis: A new perspective. In Proceedings of the ACM Symposium on Partial Evaluation and Semantics-Based Program Manipulation (PEPM'91), 1991, pp. 154-164. ACM SIGPLAN Notices\n26(9).","DOI":"10.1145\/115866.115881"},{"key":"323060_CR20","unstructured":"Jensen, T.P. Abstract interpretation in logical form. Ph.D. thesis, Imperial College, University of London. 1992. Available as DIKU Report 93\/11 from DIKU, University of Copenhagen."},{"key":"323060_CR21","doi-asserted-by":"crossref","unstructured":"Jones, C. and Plotkin, G.D. A probabilistic powerdomain of evaluations. In Proceedings, Fourth Annual Symposium on Logic in Computer Science, Asilomar Conference Center, Pacific Grove, California, 1989, pp. 186-195.","DOI":"10.1109\/LICS.1989.39173"},{"key":"323060_CR22","doi-asserted-by":"crossref","first-page":"328","DOI":"10.1016\/0022-0000(81)90036-2","volume":"22","author":"D. Kozen","year":"1981","unstructured":"Kozen, D. Semantics of probabilistic programs. Journal of Computer and System Sciences\n22 (1981) 328-350.","journal-title":"Journal of Computer and System Sciences"},{"key":"323060_CR23","doi-asserted-by":"crossref","first-page":"162","DOI":"10.1016\/0022-0000(85)90012-1","volume":"30","author":"D. Kozen","year":"1985","unstructured":"Kozen, D. A probabilistic PDL. Journal of Computer and System Sciences\n30 (1985) 162-178.","journal-title":"Journal of Computer and System Sciences"},{"key":"323060_CR24","unstructured":"Launchbury, J. Projection factorisations in partial evaluation. Ph.D. thesis, Department of Computing, University of Glasgow, 1989."},{"key":"323060_CR25","unstructured":"Leino, K.R.M. and Joshi, R. A semantic approach to secure information flow. In MPC'98, 1998."},{"issue":"1-3","key":"323060_CR26","doi-asserted-by":"crossref","first-page":"113","DOI":"10.1016\/S0167-6423(99)00024-6","volume":"37","author":"K.R.M. Leino","year":"2000","unstructured":"Leino, K.R.M. and Joshi, R. A semantic approach to secure information flow. Science of Computer Programming\n37(1-3) (2000) 113-138.","journal-title":"Science of Computer Programming"},{"key":"323060_CR27","unstructured":"Manes, E. Graduate Texts in Mathematics. Vol. 26, 1976, Springer-Verlag."},{"key":"323060_CR28","doi-asserted-by":"crossref","unstructured":"McCullough, D. Specifications for multi-level security and hook-up property. In Proceedings of the IEEE Symposium on Security and Privacy, 1987, pp. 161-166.","DOI":"10.1109\/SP.1987.10009"},{"key":"323060_CR29","doi-asserted-by":"crossref","unstructured":"McLean, J. Security models and information flow. In Proceedings of the IEEE Symposium on Security and Privacy, Oakland, California, 1990a, pp. 180-187.","DOI":"10.1109\/RISP.1990.63849"},{"issue":"1","key":"323060_CR30","doi-asserted-by":"crossref","first-page":"9","DOI":"10.1109\/2.48795","volume":"23","author":"J. McLean","year":"1990","unstructured":"McLean, J. The specification and modeling of computer security. Computer\n23(1) (1990b) 9-16.","journal-title":"Computer"},{"key":"323060_CR31","unstructured":"McLean, J. Security models. In Encyclopedia of Software Engineering, J. Marciniak (Ed.). Wiley &;;; Sons. 1994."},{"issue":"6A","key":"323060_CR32","doi-asserted-by":"crossref","first-page":"727","DOI":"10.1007\/BF03180570","volume":"4","author":"M. Mizuno","year":"1992","unstructured":"Mizuno, M. and Schmidt, D. Ascurity flowcontrol algorithm and its denotational semantics correctness proof. Formal Aspects of Computing\n4(6A) (1992) 727-754.","journal-title":"Formal Aspects of Computing"},{"key":"323060_CR33","doi-asserted-by":"crossref","unstructured":"Moskowitz, I.S. and Costich, O.L. A classical automata approach to noninterference type problems. In The Computer Security Foundations Workshop V proceedings, the Franconia Inn, Franconia, New Hampshire. June 16-18, 1992, pp. 2-8.","DOI":"10.1109\/CSFW.1992.236792"},{"key":"323060_CR34","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1016\/0304-3975(89)90091-1","volume":"69","author":"F. Nielson","year":"1989","unstructured":"Nielson, F. Two-level semantics and abstract interpretation. Theoretical Computer Science-Fundamental Studies\n69 (1989) 117-242.","journal-title":"Theoretical Computer Science-Fundamental Studies"},{"key":"323060_CR35","unstructured":"\u00d8rb\u00e6 k, P. Can you trust your data?. In Proceedings of the TAPSOFT\/FASE'95 Conference, P.D. Mosses, M.I. Schwartzbach, and M. Nielsen (Eds.). Aarhus, Denmark, 1995, pp. 575-590."},{"key":"323060_CR36","unstructured":"\u00d8rb\u00e6 k, P. Trust and dependence analysis. Ph.D. thesis, Dept. of Computer Science, Univ. of Aarhus. BRICS report DS-97-2, 1997."},{"key":"323060_CR37","doi-asserted-by":"crossref","unstructured":"\u00d8rb\u00e6 k, P. and Palsberg, J. Trust in the \u03bb-calculus. Journal of Functional Programming\n7(4) (1997).","DOI":"10.1017\/S0956796897002906"},{"key":"323060_CR38","unstructured":"Plotkin, G. Post-graduate lecture notes in advanced domain theory (incorporating the \u201cPisa Notes\u201d). Dept. of Computer Science, Univ. of Edinburgh. 1981."},{"issue":"3","key":"323060_CR39","doi-asserted-by":"crossref","first-page":"452","DOI":"10.1137\/0205035","volume":"5","author":"G.D. Plotkin","year":"1976","unstructured":"Plotkin, G.D. A power domain construction. SIAM Journal on Computing\n5(3) (1976) 452-487.","journal-title":"SIAM Journal on Computing"},{"key":"323060_CR40","first-page":"513","volume-title":"Proceedings 9th IFIP World Computer Congress, Information Processing '83, Paris, France, 19-23 Sept 1983","author":"J.C. Reynolds","year":"1983","unstructured":"Reynolds, J.C. Types, abstraction and parametric polymorphism. In Proceedings 9th IFIP World Computer Congress, Information Processing '83, Paris, France, 19-23 Sept 1983, R.E.A. Mason (Ed.). North Holland, Amsterdam; 1983, pp. 513-523."},{"key":"323060_CR41","doi-asserted-by":"crossref","unstructured":"Sabelfeld, A. and Sands, D. A per model of secure information flow in sequential programs. In Proceedings of the 8th European Symposium on Programming, ESOP'99, Amsterdam, 1999, pp. 40-58.","DOI":"10.1007\/3-540-49099-X_4"},{"key":"323060_CR42","unstructured":"Sabelfeld, A. and Sands, D. Probabilistic noninterference for multi-threaded programs. In Proceedings of the 13th IEEE Computer Security Foundations Workshop, Cambridge, England, 2000."},{"key":"323060_CR43","doi-asserted-by":"crossref","unstructured":"Smith, G. and Volpano, D. Secure information flow in a multi-threaded imperative language. In Conference Record of POPL '98: The 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 1998, pp. 355-364.","DOI":"10.1145\/268946.268975"},{"issue":"1","key":"323060_CR44","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1016\/0022-0000(78)90048-X","volume":"16","author":"M.B. Smyth","year":"1978","unstructured":"Smyth, M.B. Power domains. Journal of Computer and Systems Sciences\n16(1) (1978) 23-36.","journal-title":"Journal of Computer and Systems Sciences"},{"key":"323060_CR45","unstructured":"Thiemann, P. and Klaeren, H. Binding-time analysis by security analysis. Universitt T\u00fcbingen, 1997."},{"key":"323060_CR46","doi-asserted-by":"crossref","unstructured":"Volpano, D. and Smith, G. Eliminating covert flows with minimum typings. In Proc. 10th IEEE Computer Security Foundations Workshop, 1997, pp. 156-168.","DOI":"10.1109\/CSFW.1997.596807"},{"issue":"23","key":"323060_CR47","doi-asserted-by":"crossref","first-page":"231","DOI":"10.3233\/JCS-1999-72-305","volume":"7","author":"D. Volpano","year":"1999","unstructured":"Volpano, D. and Smith, G. Probabilistic noninterference in a concurrent language. Journal of Computer Security\n7(2,3) (1999) 231-253.","journal-title":"Journal of Computer Security"},{"issue":"3","key":"323060_CR48","first-page":"1","volume":"4","author":"D. Volpano","year":"1996","unstructured":"Volpano, D., Smith, G., and Irvine, C. A sound type system for secure flow analysis. J. Computer Security\n4(3) (1996) 1-21.","journal-title":"J. Computer Security"},{"key":"323060_CR49","doi-asserted-by":"crossref","unstructured":"Wadler, P. Theorems for free. Functional Programming Languages and Computer Architecture. 1989, pp. 347-359.","DOI":"10.1145\/99370.99404"},{"key":"323060_CR50","doi-asserted-by":"crossref","unstructured":"Wadler, P. and Hughes, R.J.M. Projections for strictness analysis. In 1987 Conference on Functional Programming and Computer Architecture, Portland, Oregon, 1987, pp. 385-407.","DOI":"10.1007\/3-540-18317-5_21"}],"container-title":["Higher-Order and Symbolic Computation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1011553200337.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1011553200337\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1011553200337.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,8]],"date-time":"2025-07-08T13:47:43Z","timestamp":1751982463000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1011553200337"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001,3]]},"references-count":50,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2001,3]]}},"alternative-id":["323060"],"URL":"https:\/\/doi.org\/10.1023\/a:1011553200337","relation":{},"ISSN":["1388-3690","1573-0557"],"issn-type":[{"value":"1388-3690","type":"print"},{"value":"1573-0557","type":"electronic"}],"subject":[],"published":{"date-parts":[[2001,3]]}}}