{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,1]],"date-time":"2022-04-01T01:39:01Z","timestamp":1648777141919},"reference-count":41,"publisher":"Elsevier BV","issue":"1","license":[{"start":{"date-parts":[[2003,1,1]],"date-time":"2003-01-01T00:00:00Z","timestamp":1041379200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2014,11,20]],"date-time":"2014-11-20T00:00:00Z","timestamp":1416441600000},"content-version":"vor","delay-in-days":4341,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/3.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Electronic Notes in Theoretical Computer Science"],"published-print":{"date-parts":[[2003,1]]},"DOI":"10.1016\/s1571-0661(04)00243-9","type":"journal-article","created":{"date-parts":[[2004,1,29]],"date-time":"2004-01-29T10:14:39Z","timestamp":1075371279000},"page":"25-50","source":"Crossref","is-referenced-by-count":0,"title":["Abstract Interpretation for Proving Secrecy Properties in Security Protocols"],"prefix":"10.1016","volume":"55","author":[{"given":"K.","family":"Adi","sequence":"first","affiliation":[]},{"given":"M.","family":"Debbabi","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/S1571-0661(04)00243-9_NEWBIB1","doi-asserted-by":"crossref","unstructured":"M. Abadi and A. D. Gordon. A Calculus for Cryptographic Protocols: The SPI Calculus. Technical report, DEC\/SRC, December 1996.","DOI":"10.1145\/266420.266432"},{"key":"10.1016\/S1571-0661(04)00243-9_NEWBIB2","doi-asserted-by":"crossref","unstructured":"M. Abadi and Andrew D. Gordon. A Calculus for Cryptographic Protocols: The SPI Calculus. In the Proceedings of the Fourth ACM Conference on Computer and Communications Security. ACM Press, April 1997.","DOI":"10.1145\/266420.266432"},{"key":"10.1016\/S1571-0661(04)00243-9_NEWBIB3","doi-asserted-by":"crossref","unstructured":"M. Abadi and M. R. Tuttle. A Semantics for a Logic of Authentication. In Proceedings of the 10th Annual ACM Symposium On Principles of Distributed Computing, pages 201\u2013216, August 1991.","DOI":"10.1145\/112600.112618"},{"key":"10.1016\/S1571-0661(04)00243-9_NEWBIB4","doi-asserted-by":"crossref","unstructured":"S. Abramsky. Game Semantics for Programming Languages. Lecture Notes in Computer Science, 1295, 1997.","DOI":"10.1007\/BFb0029944"},{"key":"10.1016\/S1571-0661(04)00243-9_NEWBIB5","doi-asserted-by":"crossref","unstructured":"Samson Abramsky, Pasquale Malacaria, and Radha Jagadeesan. Full Abstraction for PCF. Lecture Notes in Computer Science, 789, 1994.","DOI":"10.1007\/3-540-57887-0_87"},{"key":"10.1016\/S1571-0661(04)00243-9_NEWBIB6","doi-asserted-by":"crossref","unstructured":"K. Adi, M. Debbabi, and M. Mejri. A New Logic for Electronic Commerce Protocols. In 8th International Conference on Algebraic Methodology and Software Technology, AMAST'2000, Iowa City, Iowa, USA, volume 1816, pages 499\u2013513. Springer-Verlag, 2000.","DOI":"10.1007\/3-540-45499-3_35"},{"key":"10.1016\/S1571-0661(04)00243-9_NEWBIB7","doi-asserted-by":"crossref","unstructured":"P. Bieber. A Logic of Communication in a Hostile Environment. In Proceedings of the Computer Security Foundations Workshop III, pages 14\u201322. IEEE Computer Society Press, 1990.","DOI":"10.1109\/CSFW.1990.128181"},{"key":"10.1016\/S1571-0661(04)00243-9_NEWBIB8","doi-asserted-by":"crossref","unstructured":"P. Bieber and N. B. Cuppens. Formal Development of Authentication Protocols. In Proceedings of the BCS-FACS 6th Refinement Workshop on software Engineering and its Applications, January 1994.","DOI":"10.1007\/978-1-4471-3240-0_5"},{"key":"10.1016\/S1571-0661(04)00243-9_NEWBIB9","doi-asserted-by":"crossref","unstructured":"P. Bieber, N. B. Cuppens, T. Lehman, and E. van Wickeren. Abstract Machines for Communication Security. In the Proceedings of the IEEE Computer Security Foundation Workshop VI, June 1993.","DOI":"10.1109\/CSFW.1993.246632"},{"key":"10.1016\/S1571-0661(04)00243-9_NEWBIB10","doi-asserted-by":"crossref","unstructured":"C. Boyd. A Framework for Authentication. In Proceedings of the European Symposuim on Research in Computer Security, ESORICS 92, pages 273\u2013292. Springer Verlag, Lecture Notes in Computer Science 648, November 1992.","DOI":"10.1007\/BFb0013903"},{"key":"10.1016\/S1571-0661(04)00243-9_NEWBIB11","series-title":"Computer Security\u2014ESORICS '94","first-page":"93","article-title":"Designing Secure Key Exchange Protocols","author":"Boyd","year":"1994"},{"key":"10.1016\/S1571-0661(04)00243-9_NEWBIB12","doi-asserted-by":"crossref","unstructured":"M. Burrows, M. Abadi, and R. Needham. A Logic of Authentication. Technical Report 39, Digital Systems Research Center, February 1989.","DOI":"10.1145\/74850.74852"},{"issue":"2","key":"10.1016\/S1571-0661(04)00243-9_NEWBIB13","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1145\/382258.382790","article-title":"Rejoinder to Nessett","volume":"24","author":"Burrows","year":"1990","journal-title":"ACM Operating Systems Review"},{"key":"10.1016\/S1571-0661(04)00243-9_NEWBIB14","unstructured":"M. Burrows, M. Abadi, and R. Needham. The Scope of a Logic of Authentication. Technical Report 39, Digital Systems Research Center, 1994."},{"key":"10.1016\/S1571-0661(04)00243-9_NEWBIB15","doi-asserted-by":"crossref","unstructured":"U. Carlsen. Formal Specification and Analysis of Cryptographic Protocols. PhD thesis, PARIS XI University, October 1994.","DOI":"10.1109\/RISP.1994.296586"},{"key":"10.1016\/S1571-0661(04)00243-9_NEWBIB16","unstructured":"E. Clarke, W. Marrero, and S. Jha. A Machine Checkable Logic of Knowledge for Specifying Security Properties of Electronic Commerce Protocols. In Proceedings IFIP Working Conference on Programming Concepts and Methods, PROCOMET, June 1998."},{"issue":"2","key":"10.1016\/S1571-0661(04)00243-9_NEWBIB17","doi-asserted-by":"crossref","first-page":"81","DOI":"10.1007\/BF00196790","article-title":"Applying a Formal Analysis Technique to the CCITT X.509 Strong Two-Way Authentication Protocol","volume":"3","author":"Gaarder","year":"1991","journal-title":"Journal of cryptology"},{"key":"10.1016\/S1571-0661(04)00243-9_NEWBIB18","unstructured":"P. Gardiner, D. Jackson, and J. Hulance et B. Roscoe. Security Modeling in CSP and FDR: Deliverable bundle 2. Technical report, Formal Systems (Europe) Ltd, April 1996."},{"key":"10.1016\/S1571-0661(04)00243-9_NEWBIB19","unstructured":"P. Gardiner, D. Jackson, and B. Roscoe. Security Modeling in CSP and FDR: Deliverable bundle 3. Technical report, Formal Systems (Europe) Ltd, July 1996."},{"issue":"3","key":"10.1016\/S1571-0661(04)00243-9_NEWBIB20","doi-asserted-by":"crossref","first-page":"226","DOI":"10.1145\/146937.146940","article-title":"A Logic for Reasoning About Security","volume":"10","author":"Glasgow","year":"1992","journal-title":"TOCS"},{"key":"10.1016\/S1571-0661(04)00243-9_NEWBIB21","unstructured":"V. D. Gligor and R. Kailar. On Belief Evolution in Authentication Protocols. In Proceedings of the IEEE Computer Security Foundations Workshop IV, Franconia, pages 103\u2013116, June 1991."},{"key":"10.1016\/S1571-0661(04)00243-9_NEWBIB22","doi-asserted-by":"crossref","unstructured":"L. Gong, R. Needham, and R. Yahalom. Reasoning About Belief in Cryptographic Protocols. In Deborah Cooper and Teresa Lunt, editors, Proceedings 1990 IEEE Symposium on Research in Security and Privacy, pages 234\u2013248. IEEE Computer Society, May 1990.","DOI":"10.1109\/RISP.1990.63854"},{"key":"10.1016\/S1571-0661(04)00243-9_NEWBIB23","series-title":"Communating Sequential Processes","author":"Hoare","year":"1985"},{"key":"10.1016\/S1571-0661(04)00243-9_NEWBIB24","doi-asserted-by":"crossref","unstructured":"J. M. E. Hyland, and C.-H. L. Ong. Pi-calculus, Dialogue Games and PCF. In Proceedings of the 7th ACM Conference on Functional Programming Languages and Computer Architecture, pages 96\u2013107. ACM Press, 1995.","DOI":"10.1145\/224164.224189"},{"key":"10.1016\/S1571-0661(04)00243-9_NEWBIB25","doi-asserted-by":"crossref","unstructured":"J. Martin E. Hyland. Game Semantics. In P. Dybjer and A. M. Pitts, editors, Semantics and Logics of Computation. Cambridge University Press, 1997. Based on lectures given at the CLICS-II Summer School on Semantics and Logics of Computation, Isaac Newton Institute for Mathematical Sciences, Cambridge UK, September 1995.","DOI":"10.1017\/CBO9780511526619.005"},{"issue":"3","key":"10.1016\/S1571-0661(04)00243-9_NEWBIB26","doi-asserted-by":"crossref","first-page":"131","DOI":"10.1016\/0020-0190(95)00144-2","article-title":"An Attack on the Needham-Schroeder Public Key Authentication Protocol","volume":"56","author":"Lowe","year":"1995","journal-title":"Information Processing Letters"},{"key":"10.1016\/S1571-0661(04)00243-9_NEWBIB27","doi-asserted-by":"crossref","unstructured":"G. Lowe. Breaking and Fixing the Needham Schroeder Public-Key Protocol using FDR. In Proceedings of TACAS, volume 1055, pages 147\u2013166. Springer Verlag, 1996.","DOI":"10.1007\/3-540-61042-1_43"},{"key":"10.1016\/S1571-0661(04)00243-9_NEWBIB28","doi-asserted-by":"crossref","unstructured":"G. Lowe. Some New Attacks upon Security Protocols. In Proceedings of the Computer Security Foundations Workshop VIII. IEEE Computer Society Press, 1996.","DOI":"10.1109\/CSFW.1996.503701"},{"key":"10.1016\/S1571-0661(04)00243-9_NEWBIB29","unstructured":"G. Lowe. SPLICE-AS: A Case Study in Using CSP to Detect Errors in Security Protocols. Technical report, Programming Research Group, Oxford, 1996."},{"key":"10.1016\/S1571-0661(04)00243-9_NEWBIB30","doi-asserted-by":"crossref","unstructured":"W. Mao and C. Boyd. Towards the Formal Analysis of Security Protocols. In Proceedings of the Computer Security Foundations Workshop VI, pages 147\u2013158. IEEE Computer Society Press, 1993.","DOI":"10.1109\/CSFW.1993.246631"},{"key":"10.1016\/S1571-0661(04)00243-9_NEWBIB31","unstructured":"R. Milner, J. Parrow, and D. Walker. A Calculus of Mobile Processes. Technical report, Laboratory for Foundations of Computer Science, Department of Computer Science, University of Edinburgh, 1989."},{"key":"10.1016\/S1571-0661(04)00243-9_NEWBIB32","doi-asserted-by":"crossref","unstructured":"J. C. Mitchell, M. Mitchell, and U. Stern. Automated Analysis of Cryptographic Protocols Using Murphi. In Proceedings 1997 IEEE Symposium on Security and Privacy, pages 141\u2013153. IEEE Computer Society, May 1997.","DOI":"10.1109\/SECPRI.1997.601329"},{"key":"10.1016\/S1571-0661(04)00243-9_NEWBIB33","doi-asserted-by":"crossref","unstructured":"L. E. Moser. A Logic of Knowledge and Belief about Computer Security. In J. Thomas Haigh, editor, Proceedings of the Computer Security Foundations Workshop III, pages 57\u201363. IEEE, Computer Society Press of the IEEE, 1989.","DOI":"10.1109\/CSFW.1989.40587"},{"key":"10.1016\/S1571-0661(04)00243-9_NEWBIB34","doi-asserted-by":"crossref","unstructured":"P. V. Rangan. An Axiomatic Basis of Trust in Distributed Systems. In Proceedings of the 1988 Symposium on Security and Privacy, pages 204\u2013211. IEEE Computer Society Press, April 1988.","DOI":"10.1109\/SECPRI.1988.8112"},{"key":"10.1016\/S1571-0661(04)00243-9_NEWBIB35","doi-asserted-by":"crossref","unstructured":"B. Roscoe and P. Gardiner. Security Modelling in CSP and FDR: Final report. Technical report, Formal Systems Europe, October 1995.","DOI":"10.1109\/CSFW.1995.518556"},{"key":"10.1016\/S1571-0661(04)00243-9_NEWBIB36","doi-asserted-by":"crossref","unstructured":"S. Schneider. Security Properties and CSP. In Proceedings of the 1996 IEEE Symposium on Security and Privacy, pages 174\u2013187. IEEE Computer Society Press, May 1996.","DOI":"10.1109\/SECPRI.1996.502680"},{"key":"10.1016\/S1571-0661(04)00243-9_NEWBIB37","unstructured":"E. Snekkenes. Formal Specification and Analysis of Cryptographic Protocols. PhD thesis, Faculty of Mathematics and Natural Sciences, University of Oslo, Norwegian Defence Research Establishment, P.O. Box 25, N-2007, Kjeller, Norway, January 1995."},{"key":"10.1016\/S1571-0661(04)00243-9_NEWBIB38","doi-asserted-by":"crossref","unstructured":"P. Syverson and P. C. van Oorshot. On Unifying some Cryptographic Protocol Logics. In Proceedings of the IEEE 1994 Computer Society Symposium on Security and Privacy, pages 14\u201328. IEEE Computer Society, May 1994.","DOI":"10.1109\/RISP.1994.296595"},{"key":"10.1016\/S1571-0661(04)00243-9_NEWBIB39","unstructured":"V. Varadharajan. Formal Specification of a Secure Distributed System. In Proceedings of the 12th National Computer Security Conference, pages 146\u2013171, October 1989."},{"key":"10.1016\/S1571-0661(04)00243-9_NEWBIB40","doi-asserted-by":"crossref","DOI":"10.1016\/0167-4048(89)90008-4","article-title":"Verification of Network Security Protocols","volume":"8","author":"Varadharajan","year":"1989","journal-title":"Computers and Security"},{"key":"10.1016\/S1571-0661(04)00243-9_NEWBIB41","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1016\/0920-5489(89)90022-6","article-title":"Use of Formal Technique in the Specification of Authentication protocols","volume":"9","author":"Varadharajan","year":"1990","journal-title":"Computer Standards and Interfaces"}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104002439?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104002439?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2020,3,29]],"date-time":"2020-03-29T12:27:29Z","timestamp":1585484849000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1571066104002439"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,1]]},"references-count":41,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2003,1]]}},"alternative-id":["S1571066104002439"],"URL":"https:\/\/doi.org\/10.1016\/s1571-0661(04)00243-9","relation":{},"ISSN":["1571-0661"],"issn-type":[{"value":"1571-0661","type":"print"}],"subject":[],"published":{"date-parts":[[2003,1]]}}}