{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T20:26:11Z","timestamp":1761596771532},"reference-count":23,"publisher":"Elsevier BV","issue":"2","license":[{"start":{"date-parts":[[2002,6,1]],"date-time":"2002-06-01T00:00:00Z","timestamp":1022889600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,17]],"date-time":"2013-07-17T00:00:00Z","timestamp":1374019200000},"content-version":"vor","delay-in-days":4064,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theoretical Computer Science"],"published-print":{"date-parts":[[2002,6]]},"DOI":"10.1016\/s0304-3975(01)00140-2","type":"journal-article","created":{"date-parts":[[2002,10,11]],"date-time":"2002-10-11T07:37:18Z","timestamp":1034321838000},"page":"381-418","source":"Crossref","is-referenced-by-count":34,"title":["Validating firewalls using flow logics"],"prefix":"10.1016","volume":"283","author":[{"given":"Flemming","family":"Nielson","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hanne","family":"Riis Nielson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ren\u00e9 Rydhof","family":"Hansen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/S0304-3975(01)00140-2_BIB1","doi-asserted-by":"crossref","unstructured":"M. Abadi, Secrecy by typing in security protocols, in: Proc. Theoretical Aspects of Computer Software 1997, Lecture Notes in Computer Science, Vol. 1281, Springer, Berlin, 1997, pp. 611\u2013638.","DOI":"10.1007\/BFb0014571"},{"key":"10.1016\/S0304-3975(01)00140-2_BIB2","doi-asserted-by":"crossref","unstructured":"C. Bodei, P. Degano, F. Nielson, H.R. Nielson, Control flow analysis for the \u03c0-calculus, in: Proc. CONCUR\u201998, Lecture Notes in Computer Science, Vol. 1466, Springer, Berlin, 1998, pp. 84\u201398.","DOI":"10.1007\/BFb0055617"},{"key":"10.1016\/S0304-3975(01)00140-2_BIB3","doi-asserted-by":"crossref","unstructured":"C. Bodei, P. Degano, F. Nielson, H.R. Nielson, Static analysis of processes for no read-up and no write-down, in: Proc. of 2nd FoSSaCS\u201999, Lecture Notes in Computer Science, Vol. 1578, Springer, Berlin, 1999, pp. 120\u2013134.","DOI":"10.1007\/3-540-49019-1_9"},{"key":"10.1016\/S0304-3975(01)00140-2_BIB4","doi-asserted-by":"crossref","unstructured":"C. Bodei, P. Degano, F. Nielson, H.R. Nielson, Static analysis for the \u03c0-calculus with applications to security, Inform. Comput. 2001 (to appear).","DOI":"10.1006\/inco.2000.3020"},{"key":"10.1016\/S0304-3975(01)00140-2_BIB5","doi-asserted-by":"crossref","unstructured":"D. Bolignano, An approach to the formal verification of cryptographic protocols, in: Proc. 3rd ACM Conf. on Computer and Communications Security, ACM Press, New York, 1996, pp. 106\u2013118.","DOI":"10.1145\/238168.238196"},{"key":"10.1016\/S0304-3975(01)00140-2_BIB6","doi-asserted-by":"crossref","unstructured":"L. Cardelli, G. Ghelli, A.D. Gordon, Mobility types for mobile ambients, in: Proc. of ICALP\u201999, Lecture Notes in Computer Science, Vol. 1644, Springer, Berlin, 1999, pp. 230\u2013239.","DOI":"10.1007\/3-540-48523-6_20"},{"key":"10.1016\/S0304-3975(01)00140-2_BIB7","doi-asserted-by":"crossref","unstructured":"L. Cardelli, A.D. Gordon, Mobile ambients, in: Proc. of FoSSaCS\u201998, Lecture Notes in Computer Science, Vol. 1378, Springer, Berlin, 1998, pp. 140\u2013155.","DOI":"10.1007\/BFb0053547"},{"key":"10.1016\/S0304-3975(01)00140-2_BIB8","doi-asserted-by":"crossref","unstructured":"L. Cardelli, A.D. Gordon, Types for mobile ambients, in: Proc. of POPL\u201999, ACM Press, New York, 1999, pp. 79\u201392.","DOI":"10.1145\/292540.292550"},{"key":"10.1016\/S0304-3975(01)00140-2_BIB9","doi-asserted-by":"crossref","unstructured":"L. Cardelli, A.D. Gordon, Anytime, anywhere: modal logics for mobile ambients, in: Proc. of POPL\u201900, ACM Press, New York, 2000, pp. 365\u2013377.","DOI":"10.1145\/325694.325742"},{"issue":"12","key":"10.1016\/S0304-3975(01)00140-2_BIB10","doi-asserted-by":"crossref","first-page":"198","DOI":"10.1109\/TIT.1983.1056650","article-title":"On the security of public key protocols","volume":"IT-29","author":"Dolev","year":"1983","journal-title":"IEEE Trans. Inform. Theory"},{"key":"10.1016\/S0304-3975(01)00140-2_BIB11","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1016\/0743-1066(84)90014-1","article-title":"Linear-time algorithms for testing the satisfiability of propositional Horn formulae","volume":"3","author":"Dowling","year":"1984","journal-title":"J. Logic Programm."},{"key":"10.1016\/S0304-3975(01)00140-2_BIB12","doi-asserted-by":"crossref","unstructured":"F.J.T. F\u00e1brega, J.C. Herzog, J.D. Guttman, Strand Spaces: why is a security protocol correct? in: Proc. of 1998 IEEE Symp. on Security and Privacy, IEEE Press, New York, 1998, pp. 160\u2013171.","DOI":"10.1109\/SECPRI.1998.674832"},{"key":"10.1016\/S0304-3975(01)00140-2_BIB13","series-title":"Inside Java 2 Platform Security","author":"Gong","year":"1999"},{"key":"10.1016\/S0304-3975(01)00140-2_BIB14","unstructured":"R.R. Hansen, J.G. Jensen, F.Nielson, H.R. Nielson, Abstract interpretation of mobile ambients, in: Proc. of SAS\u201999, Lecture Notes in Computer Science, Vol. 1694, 1999, pp. 135\u2013148."},{"issue":"1","key":"10.1016\/S0304-3975(01)00140-2_BIB15","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0890-5401(92)90008-4","article-title":"A calculus of mobile processes (I and II)","volume":"100","author":"Milner","year":"1992","journal-title":"Inform. Comput."},{"key":"10.1016\/S0304-3975(01)00140-2_BIB16","doi-asserted-by":"crossref","DOI":"10.1016\/S1571-0661(05)80695-4","article-title":"Flow logics and operational semantics","volume":"10","author":"Nielson","year":"1998","journal-title":"Electron. Notes Theoret. Comput. Sci."},{"key":"10.1016\/S0304-3975(01)00140-2_BIB17","series-title":"Principles of Program Analysis","author":"Nielson","year":"1999"},{"key":"10.1016\/S0304-3975(01)00140-2_BIB18","doi-asserted-by":"crossref","unstructured":"F. Nielson, H.R. Nielson, R.R. Hansen, J.G. Jensen, Validating firewalls in mobile ambients, in: Proc. of Concur\u201999, Lecture Notes in Computer Science, Vol. 1664, Springer, Berlin, 1999, pp. 463\u2013477.","DOI":"10.1007\/3-540-48320-9_32"},{"key":"10.1016\/S0304-3975(01)00140-2_BIB19","doi-asserted-by":"crossref","unstructured":"F. Nielson, H.R. Nielson, M. Sagiv, A Kleene analysis of mobile ambients, in: Proc. of ESOP\u201900, Lecture Notes in Computer Science, Vol. 1782, Springer, Berlin, 2000, pp. 305\u2013319.","DOI":"10.1007\/3-540-46425-5_20"},{"key":"10.1016\/S0304-3975(01)00140-2_BIB20","doi-asserted-by":"crossref","unstructured":"F. Nielson, H. Seidl, Control-flow analysis in cubic time, in: Proc. of ESOP\u20192001, Lecture Notes in Computer Science, Vol. 2028, Springer, Berlin, 2001, pp. 252\u2013268.","DOI":"10.1007\/3-540-45309-1_17"},{"key":"10.1016\/S0304-3975(01)00140-2_BIB21","doi-asserted-by":"crossref","unstructured":"H.R. Nielson, F. Nielson, Flow logics for constraint based analysis, in: Proc. CC\u201998, Lecture Notes in Computer Science, Vol. 1383, Springer, Berlin, 1998, pp. 109\u2013127.","DOI":"10.1007\/BFb0026426"},{"key":"10.1016\/S0304-3975(01)00140-2_BIB22","doi-asserted-by":"crossref","unstructured":"H.R. Nielson, F. Nielson, Shape analysis for mobile ambients, in: Proc. of POPL\u201900, ACM Press, New York, 2000, pp. 142\u2013154.","DOI":"10.1145\/325694.325711"},{"key":"10.1016\/S0304-3975(01)00140-2_BIB23","doi-asserted-by":"crossref","unstructured":"L.C. Paulson, Proving properties of security protocols by induction, in: Proc. 10th Computer Security Foundations Workshop, IEEE, Innsbruck 1997, pp. 70\u201383.","DOI":"10.1109\/CSFW.1997.596788"}],"container-title":["Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397501001402?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397501001402?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,4,11]],"date-time":"2019-04-11T05:25:21Z","timestamp":1554960321000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0304397501001402"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,6]]},"references-count":23,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2002,6]]}},"alternative-id":["S0304397501001402"],"URL":"https:\/\/doi.org\/10.1016\/s0304-3975(01)00140-2","relation":{},"ISSN":["0304-3975"],"issn-type":[{"value":"0304-3975","type":"print"}],"subject":[],"published":{"date-parts":[[2002,6]]}}}