{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:33:41Z","timestamp":1759638821880,"version":"3.30.1"},"reference-count":28,"publisher":"Elsevier BV","issue":"6","license":[{"start":{"date-parts":[[2002,5,1]],"date-time":"2002-05-01T00:00:00Z","timestamp":1020211200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Future Generation Computer Systems"],"published-print":{"date-parts":[[2002,5]]},"DOI":"10.1016\/s0167-739x(02)00047-x","type":"journal-article","created":{"date-parts":[[2002,10,11]],"date-time":"2002-10-11T02:27:33Z","timestamp":1034303253000},"page":"747-756","source":"Crossref","is-referenced-by-count":12,"title":["Flow logic for Dolev\u2013Yao secrecy in cryptographic processes"],"prefix":"10.1016","volume":"18","author":[{"given":"C.","family":"Bodei","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"P.","family":"Degano","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"F.","family":"Nielson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"H.","family":"Riis Nielson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"issue":"46","key":"10.1016\/S0167-739X(02)00047-X_BIB1","first-page":"18","article-title":"Secrecy by typing in security protocols","volume":"5","author":"Abadi","year":"1999","journal-title":"J. ACM"},{"key":"10.1016\/S0167-739X(02)00047-X_BIB2","doi-asserted-by":"crossref","unstructured":"M. Abadi, Security protocols and specifications, in: Proceedings of the FoSSaCS\u201999, Lecture Notes in Computer Science, Vol. 1578, Springer, Berlin, 1999, pp. 1\u201313.","DOI":"10.1007\/3-540-49019-1_1"},{"key":"10.1016\/S0167-739X(02)00047-X_BIB3","doi-asserted-by":"crossref","unstructured":"M. Abadi, B. Blanchet, Secrecy types for asymmetric communication, in: Proceedings of the FoSSaCS\u201999, Lecture Notes in Computer Science, Vol. 2030, Springer, Berlin, 2001, pp. 25\u201341.","DOI":"10.1007\/3-540-45315-6_2"},{"key":"10.1016\/S0167-739X(02)00047-X_BIB4","doi-asserted-by":"crossref","unstructured":"M. Abadi, C. Fournet, Mobile values, new names, and secure communication, in: Proceedings of the POPL\u201901, ACM, New York, 2001, pp. 104\u2013115.","DOI":"10.1145\/360204.360213"},{"issue":"1","key":"10.1016\/S0167-739X(02)00047-X_BIB5","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1006\/inco.1998.2740","article-title":"A calculus for cryptographic protocols\u2014the spi calculus","volume":"148","author":"Abadi","year":"1999","journal-title":"Inform. Comput."},{"key":"10.1016\/S0167-739X(02)00047-X_BIB6","doi-asserted-by":"crossref","unstructured":"M. Abadi, J. J\u00fcrjens, Formal eavesdropping and its computational interpretation, in: Proceedings of the TACS\u201901, Lecture Notes in Computer Science, Springer, Berlin, 2001.","DOI":"10.1007\/3-540-45500-0_4"},{"key":"10.1016\/S0167-739X(02)00047-X_BIB7","unstructured":"C. Bodei, Security issues in process calculi, Ph.D. Thesis, Dipartimento di Informatica, Universit\u00e0 di Pisa, Pisa, 2000."},{"key":"10.1016\/S0167-739X(02)00047-X_BIB8","doi-asserted-by":"crossref","unstructured":"C. Bodei, P. Degano, F. Nielson, H. Riis Nielson, Control flow analysis for the \u03c0-calculus, in: Proceedings of the CONCUR\u201998, Lecture Notes in Computer Science, Vol. 1466, Springer, Berlin, 1998, pp. 84\u201398.","DOI":"10.1007\/BFb0055617"},{"key":"10.1016\/S0167-739X(02)00047-X_BIB9","doi-asserted-by":"crossref","unstructured":"C. Bodei, P. Degano, F. Nielson, H. Riis Nielson, Static analysis for secrecy and non-interference in network of processes, in: Proceedings of the PaCT\u201901, Lecture Notes in Computer Science, Vol. 2127, Springer, Berlin, 2001, pp. 27\u201341.","DOI":"10.1007\/3-540-44743-1_3"},{"key":"10.1016\/S0167-739X(02)00047-X_BIB10","doi-asserted-by":"crossref","first-page":"68","DOI":"10.1006\/inco.2000.3020","article-title":"Static analysis for the \u03c0-calculus with their application to security","volume":"168","author":"Bodei","year":"2001","journal-title":"Inform. Comput."},{"key":"10.1016\/S0167-739X(02)00047-X_BIB11","doi-asserted-by":"crossref","unstructured":"D. Bolignano, An approach to the formal verification of cryptographic protocols, in: Proceedings of the Third ACM Conference on Computer and Communications Security, ACM, New York, 1996, pp. 106\u2013118.","DOI":"10.1145\/238168.238196"},{"key":"10.1016\/S0167-739X(02)00047-X_BIB12","doi-asserted-by":"crossref","unstructured":"L. Cardelli, A.D. Gordon, Types for mobile ambients, in: Proceedings of the POPL\u201999, ACM, New York, 1999, pp. 79\u201392.","DOI":"10.1145\/292540.292550"},{"issue":"1","key":"10.1016\/S0167-739X(02)00047-X_BIB13","doi-asserted-by":"crossref","first-page":"215","DOI":"10.1016\/S0304-3975(99)00232-7","article-title":"Types for access control","volume":"240","author":"De Nicola","year":"2000","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/S0167-739X(02)00047-X_BIB14","doi-asserted-by":"crossref","first-page":"236","DOI":"10.1145\/360051.360056","article-title":"A lattice model of secure information flow","volume":"20","author":"Denning","year":"1976","journal-title":"Commun. ACM"},{"issue":"7","key":"10.1016\/S0167-739X(02)00047-X_BIB15","doi-asserted-by":"crossref","first-page":"504","DOI":"10.1145\/359636.359712","article-title":"Certification of programs for secure information flow","volume":"20","author":"Denning","year":"1977","journal-title":"Commun. ACM"},{"issue":"12","key":"10.1016\/S0167-739X(02)00047-X_BIB16","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\/S0167-739X(02)00047-X_BIB17","unstructured":"R.R. Hansen, J.G. Jensen, F. Nielson, H. Riis Nielson, Abstract interpretation of mobile ambients, in: Proceedings of the SAS\u201999, Lecture Notes in Computer Science, Vol. 1694, Springer, Berlin, 1999, pp. 135\u2013148."},{"key":"10.1016\/S0167-739X(02)00047-X_BIB18","doi-asserted-by":"crossref","unstructured":"N. Heintze, J.G. Riecke, The SLam calculus: programming with secrecy and integrity, in: Proceedings of the POPL\u201998, ACM, New York, 1998, pp. 365\u2013377.","DOI":"10.1145\/268946.268976"},{"issue":"12","key":"10.1016\/S0167-739X(02)00047-X_BIB19","doi-asserted-by":"crossref","first-page":"993","DOI":"10.1145\/359657.359659","article-title":"Using encryption for authentication in large networks of computers","volume":"21","author":"Needham","year":"1978","journal-title":"Commun. ACM"},{"key":"10.1016\/S0167-739X(02)00047-X_BIB20","doi-asserted-by":"crossref","unstructured":"F. Nielson, H. Riis Nielson, Flow Logics and Operational Semantics, Electronic Notes in Computer Science, Vol. 10, Elsevier, Amsterdam, 1998.","DOI":"10.1016\/S1571-0661(05)80695-4"},{"key":"10.1016\/S0167-739X(02)00047-X_BIB21","doi-asserted-by":"crossref","unstructured":"F. Nielson, H. Riis Nielson, R.R. Hansen, J.G. Jensen, Validating firewalls in mobile ambients, in: Proceedings of the 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\/S0167-739X(02)00047-X_BIB22","doi-asserted-by":"crossref","unstructured":"F. Nielson, H. Seidl, Control-flow analysis in cubic time, in: Proceedings of the ESOP\u201901, Lecture Notes in Computer Science, Vol. 2028, Springer, Berlin, 2001, pp. 252\u2013268.","DOI":"10.1007\/3-540-45309-1_17"},{"key":"10.1016\/S0167-739X(02)00047-X_BIB23","doi-asserted-by":"crossref","unstructured":"H. Riis Nielson, F. Nielson, H. Seidl, Cryptographic analysis in cubic time, in: Proceedings of the TOSCA\u201901, Electronic Notes in Computer Science, Vol. 62, Elsevier, Amsterdam, 2002.","DOI":"10.1016\/S1571-0661(04)00316-0"},{"key":"10.1016\/S0167-739X(02)00047-X_BIB24","doi-asserted-by":"crossref","unstructured":"L.C. Paulson, Proving properties of security protocols by induction, in: Proceedings of the CSFW\u201997, IEEE Press, New York, 1997, pp. 70\u201383.","DOI":"10.1109\/CSFW.1997.596788"},{"key":"10.1016\/S0167-739X(02)00047-X_BIB25","doi-asserted-by":"crossref","unstructured":"J. Riely, M. Hennessy, A typed language for distributed mobile processes, in: Proceedings of the POPL\u201998, ACM, New York, 1998, pp. 378\u2013390.","DOI":"10.1145\/268946.268978"},{"key":"10.1016\/S0167-739X(02)00047-X_BIB26","doi-asserted-by":"crossref","unstructured":"J. Riely, M. Hennessy, Trust and partial typing in open systems of mobile agents, in: Proceedings of the POPL\u201999, ACM, New York, 1999, pp. 93\u2013104.","DOI":"10.1145\/292540.292551"},{"key":"10.1016\/S0167-739X(02)00047-X_BIB27","doi-asserted-by":"crossref","first-page":"4","DOI":"10.3233\/JCS-1996-42-304","article-title":"A sound type system for secure flow analysis","volume":"4","author":"Volpano","year":"1996","journal-title":"J. Comput. Security"},{"key":"10.1016\/S0167-739X(02)00047-X_BIB28","doi-asserted-by":"crossref","unstructured":"D. Volpano, G. Smith, Secure information flow in a multi-threaded imperative language, in: Proceedings of the POPL\u201998, ACM, New York, 1998, pp. 355\u2013364.","DOI":"10.1145\/268946.268975"}],"container-title":["Future Generation Computer Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0167739X0200047X?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0167739X0200047X?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2024,12,6]],"date-time":"2024-12-06T21:19:55Z","timestamp":1733519995000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0167739X0200047X"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,5]]},"references-count":28,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2002,5]]}},"alternative-id":["S0167739X0200047X"],"URL":"https:\/\/doi.org\/10.1016\/s0167-739x(02)00047-x","relation":{},"ISSN":["0167-739X"],"issn-type":[{"type":"print","value":"0167-739X"}],"subject":[],"published":{"date-parts":[[2002,5]]}}}