{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,31]],"date-time":"2026-03-31T08:41:00Z","timestamp":1774946460591,"version":"3.50.1"},"reference-count":44,"publisher":"Elsevier BV","issue":"2-3","license":[{"start":{"date-parts":[[2003,5,1]],"date-time":"2003-05-01T00:00:00Z","timestamp":1051747200000},"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":3730,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Science of Computer Programming"],"published-print":{"date-parts":[[2003,5]]},"DOI":"10.1016\/s0167-6423(02)00132-6","type":"journal-article","created":{"date-parts":[[2003,3,25]],"date-time":"2003-03-25T16:44:35Z","timestamp":1048610675000},"page":"177-202","source":"Crossref","is-referenced-by-count":16,"title":["Abstracting cryptographic protocols with tree automata"],"prefix":"10.1016","volume":"47","author":[{"given":"David","family":"Monniaux","sequence":"first","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/S0167-6423(02)00132-6_BIB1","series-title":"14th Symp. on Theoretical Aspects of Computer Science (STACS\u201997), Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0014571","article-title":"Secrecy by typing in security protocols","author":"Abadi","year":"1997"},{"issue":"5","key":"10.1016\/S0167-6423(02)00132-6_BIB2","doi-asserted-by":"crossref","first-page":"749","DOI":"10.1145\/324133.324266","article-title":"Secrecy by typing in security protocols","volume":"46","author":"Abadi","year":"1999","journal-title":"J. ACM"},{"key":"10.1016\/S0167-6423(02)00132-6_BIB3","series-title":"Foundations of Software Science and Computation Structures (FoSSaCS\u201901)","article-title":"Secrecy types for asymmetric communication","volume":"vol. 2030","author":"Abadi","year":"2001"},{"key":"10.1016\/S0167-6423(02)00132-6_BIB4","doi-asserted-by":"crossref","unstructured":"M. Abadi, A.D. Gordon, Reasoning about cryptographic protocols in the spi calculus, in: A. Mazurkiewicz, J. Winkowski (Eds.), CONCUR \u201997: Concurrency Theory, 8th Internat. Conf., Lecture Notes in Computer Science, vol. 1243, Warsaw, Poland, July 1997, Springer, Berlin, 1997, pp. 59\u201373.","DOI":"10.1007\/3-540-63141-0_5"},{"key":"10.1016\/S0167-6423(02)00132-6_BIB5","doi-asserted-by":"crossref","unstructured":"M. Abadi, A.D. Gordon, A calculus for cryptographic protocols: the spi calculus, Research Report 149, Compaq Systems Research Center, Palo Alto, CA, USA, January 1998.","DOI":"10.1145\/266420.266432"},{"key":"10.1016\/S0167-6423(02)00132-6_BIB6","doi-asserted-by":"crossref","unstructured":"M. Abadi, M.R. Tuttle, A semantics for a logic of authentication, in: L. Logrippo, 10th Annual ACM Symp. on Principles of Distributed Computing, Montr\u00e9al, Qu\u00e9bec, Canada, August 1991, ACM Press, New York, pp. 201\u2013216.","DOI":"10.1145\/112600.112618"},{"key":"10.1016\/S0167-6423(02)00132-6_BIB7","series-title":"Proc. Seventh Annu. IEEE Symp. on Logic in Computer Science, Santa Cruz, CA, 22\u201325 June 1992","first-page":"329","article-title":"Solving systems of set constraints (extended abstract)","author":"Aiken","year":"1992"},{"key":"10.1016\/S0167-6423(02)00132-6_BIB8","doi-asserted-by":"crossref","unstructured":"R. Amadio, D. Lugiez, On the reachability problem in cryptographic protocols, Technical Report 3915, INRIA, 2000.","DOI":"10.1007\/3-540-44618-4_28"},{"key":"10.1016\/S0167-6423(02)00132-6_BIB9","series-title":"27th ACM Symp. on Theory of Computing (STOC)","first-page":"57","article-title":"Provably secure session key distribution\u2014the three party case","author":"Bellare","year":"1995"},{"key":"10.1016\/S0167-6423(02)00132-6_BIB10","doi-asserted-by":"crossref","unstructured":"M. Burrows, M. Abadi, R. Needham, A logic of authentication, Technical Report 39, Digital Equipment Corporation, Systems Research Centre, February 1989.","DOI":"10.1145\/74850.74852"},{"key":"10.1016\/S0167-6423(02)00132-6_BIB11","series-title":"CSFW 12","article-title":"A meta-notation for protocol analysis","author":"Cervesato","year":"1999"},{"key":"10.1016\/S0167-6423(02)00132-6_BIB12","series-title":"Model Checking","author":"Clarke","year":"1999"},{"key":"10.1016\/S0167-6423(02)00132-6_BIB13","unstructured":"H. Comon, M. Dauchet, R. Gilleron, D. Lugiez, S. Tison, M. Tommasi, Tree Automata Techniques and Applications, Available through http:\/\/www.grappa.univ-lille3.fr\/tata\/."},{"key":"10.1016\/S0167-6423(02)00132-6_BIB14","unstructured":"P. Cousot, M\u00e9thodes it\u00e9ratives de construction et d'approximation de points fixes d'op\u00e9rateurs monotones sur un treillis, analyse s\u00e9mantique de programmes, Th\u00e8se d\u2019\u00e9tat \u00e8s sciences math\u00e9matiques, Universit\u00e9 scientifique et m\u00e9dicale de Grenoble, Grenoble, France, 21 mars 1978."},{"issue":"13","key":"10.1016\/S0167-6423(02)00132-6_BIB15","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1016\/0743-1066(92)90030-7","article-title":"Abstract interpretation and application to logic programs","volume":"2\u20133","author":"Cousot","year":"1992","journal-title":"J. Logic Progamming"},{"key":"10.1016\/S0167-6423(02)00132-6_BIB16","unstructured":"D. Craigen, M. Saaltink, Using EVES to analyze authentication protocols, Technical Report TR-96-5508-05, ORA Canada, Ottawa, March 1996."},{"key":"10.1016\/S0167-6423(02)00132-6_BIB17","doi-asserted-by":"crossref","unstructured":"D. Dolev, C. Dwork, M. Naor, Non-malleable cryptography, in: ACM, editor, Proc. 23rd annual ACM Symp. on Theory of Computing, New Orleans, Louisiana, May 6\u20138, 1991, IEEE Computer Society Press, Silver Spring, MD, 1991, pp. 542\u2013552 (Full version available from authors).","DOI":"10.1145\/103418.103474"},{"key":"10.1016\/S0167-6423(02)00132-6_BIB18","unstructured":"M. F\u00e4hndrich, BANE: analysis programmer interface, Computer Science Department, University of California at Berkeley, 1998."},{"key":"10.1016\/S0167-6423(02)00132-6_BIB19","series-title":"Rewriting Techniques and Applications (RTA-98)","article-title":"Decidable approximations of sets of descendants and sets of normal forms","volume":"vol. 1379","author":"Genet","year":"1998"},{"key":"10.1016\/S0167-6423(02)00132-6_BIB20","series-title":"Automated Deduction (CADE-17)","article-title":"Rewriting for cryptographic protocol verification","volume":"vol. 1831","author":"Genet","year":"2000"},{"key":"10.1016\/S0167-6423(02)00132-6_BIB21","unstructured":"Li Gong, Cryptographic protocols for distributed systems, Ph.D. Thesis, University of Cambridge, Cambridge, England, April 1990."},{"key":"10.1016\/S0167-6423(02)00132-6_BIB22","series-title":"IEEE Symp. on Research in Security and Privacy, Oakland, California, May 1990","first-page":"234","article-title":"Reasoning about belief in cryptographic protocols","author":"Li Gong","year":"1990"},{"key":"10.1016\/S0167-6423(02)00132-6_BIB23","unstructured":"Li Gong, P. Syverson, Fail-stop protocols: an approach to designing secure protocols, in: 5th Internat. Working Conf. on Dependable Computing for Critical Applications, September 1995."},{"key":"10.1016\/S0167-6423(02)00132-6_BIB24","unstructured":"J. Goubault-Larrecq, Clap, a simple language for cryptographic protocols, available on the WWW, 1999."},{"key":"10.1016\/S0167-6423(02)00132-6_BIB25","series-title":"Beverly Sanders, Dominique M Fifth Internat. Workshop on Formal Methods for Parallel Programming","article-title":"A method for automatic cryptographic protocol verification","volume":"vol. 1800","author":"Goubault-Larrecq","year":"2000"},{"key":"10.1016\/S0167-6423(02)00132-6_BIB26","unstructured":"S. Hanley, DNS overview with a discussion of DNS spoofing, http:\/\/www.sans.org\/infosecFAQ\/DNS\/DNS.htm."},{"key":"10.1016\/S0167-6423(02)00132-6_BIB27","article-title":"Rewrite systems","volume":"vol. B","author":"Jouannaud","year":"1990"},{"key":"10.1016\/S0167-6423(02)00132-6_BIB28","unstructured":"D. Kindred, J.M. Wing, Fast, automatic checking of security protocols, in: Second USENIX Workshop on Electronic Commerce, Oakland, California, November 1996, USENIX, pp. 41\u201352."},{"key":"10.1016\/S0167-6423(02)00132-6_BIB29","unstructured":"N. Klarlund, A. M\u00f8ller, MONA version 1.3: User Manual, BRICS, University of Aarhus, 1998."},{"key":"10.1016\/S0167-6423(02)00132-6_BIB30","first-page":"147","article-title":"Breaking and fixing the Needham\u2013Schroeder public-key protocol using FDR","volume":"vol. 1055","author":"Lowe","year":"1996"},{"key":"10.1016\/S0167-6423(02)00132-6_BIB31","series-title":"11th Computer Security Foundations Workshop","article-title":"Towards a completeness result for model checking of security protocols","author":"Lowe","year":"1998"},{"key":"10.1016\/S0167-6423(02)00132-6_BIB32","doi-asserted-by":"crossref","unstructured":"W. Marrero, E.M. Clarke, S. Jha, Model checking for security protocols, Technical Report CMU-SCS-97-139, Carnegie Mellon University, May 1997.","DOI":"10.21236\/ADA327281"},{"key":"10.1016\/S0167-6423(02)00132-6_BIB33","doi-asserted-by":"crossref","unstructured":"L. Mauborgne, Representation of Sets of Trees for Abstract Interpretation, Ph.D. Thesis, \u00c9cole Polytechnique, 2000.","DOI":"10.1007\/3-540-46425-5_18"},{"key":"10.1016\/S0167-6423(02)00132-6_BIB34","doi-asserted-by":"crossref","unstructured":"C. Meadows, The NRL protocol analyzer: an overview, J. Logic Programming 26 (2) (1996). Also available at http:\/\/chacs.nrl.navy.mil\/publications\/CHACS\/1995\/1995meadows-toappearJLP.ps.","DOI":"10.1016\/0743-1066(95)00095-X"},{"key":"10.1016\/S0167-6423(02)00132-6_BIB35","series-title":"Proc. 1984 Symp. on Security and Privacy (SSP \u201984), Los Angeles, CA, USA, April 1990","first-page":"134","article-title":"The interrogator","author":"Millen","year":"1990"},{"key":"10.1016\/S0167-6423(02)00132-6_BIB36","unstructured":"J.K. Millen, CAPSL: common authentication protocol specification language, available on the WWW."},{"key":"10.1016\/S0167-6423(02)00132-6_BIB37","article-title":"Abstracting cryptographic protocols with tree automata","volume":"vol. 1694","author":"Monniaux","year":"1999"},{"key":"10.1016\/S0167-6423(02)00132-6_BIB38","series-title":"12th Computer Security Foundations Workshop","article-title":"Decision procedures for the analysis of cryptographic protocols by logics of belief","author":"Monniaux","year":"1999"},{"key":"10.1016\/S0167-6423(02)00132-6_BIB39","series-title":"Applied Cryptography","author":"Schneier","year":"1996"},{"key":"10.1016\/S0167-6423(02)00132-6_BIB40","doi-asserted-by":"crossref","unstructured":"J. Schumann, Automatic verification of cryptographic protocols with SETHEO, in: W. McCune (Ed.), Proc. 14th Internat. Conf. on Automated deduction, Lecture Notes in Artificial Intelligence, vol. 1249, July 13\u201317 1997, Springer, Berlin, 1997, pp. 87\u2013100.","DOI":"10.1007\/3-540-63104-6_12"},{"key":"10.1016\/S0167-6423(02)00132-6_BIB41","doi-asserted-by":"crossref","unstructured":"D.Song. Athena: a new efficient automatic checker for security protocol analysis, in: 12th Computer Security Foundations Workshop, IEEE, New York, 1999, pp. 192\u2013202.","DOI":"10.1109\/CSFW.1999.779773"},{"key":"10.1016\/S0167-6423(02)00132-6_BIB42","series-title":"1st ACM Conf. on Computer and Communications Security","first-page":"97","article-title":"Adding time to a logic of authentication","author":"Syverson","year":"1993"},{"key":"10.1016\/S0167-6423(02)00132-6_BIB43","doi-asserted-by":"crossref","DOI":"10.1016\/S1571-0661(04)80072-0","article-title":"Towards a strand semantics for authentication logics","volume":"20","author":"Syverson","year":"1999","journal-title":"Electron. Notes Theoret. Comput. Sci."},{"key":"10.1016\/S0167-6423(02)00132-6_BIB44","doi-asserted-by":"crossref","unstructured":"P. Syverson, P.C. van Oorschot, On unifying some cryptographic protocol logics, in: 1994 IEEE Computer Society Symp. on Research in Security and Privacy, May 1994, pp. 14\u201328.","DOI":"10.21236\/ADA465512"}],"container-title":["Science of Computer Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0167642302001326?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0167642302001326?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2023,4,25]],"date-time":"2023-04-25T20:10:21Z","timestamp":1682453421000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0167642302001326"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,5]]},"references-count":44,"journal-issue":{"issue":"2-3","published-print":{"date-parts":[[2003,5]]}},"alternative-id":["S0167642302001326"],"URL":"https:\/\/doi.org\/10.1016\/s0167-6423(02)00132-6","relation":{},"ISSN":["0167-6423"],"issn-type":[{"value":"0167-6423","type":"print"}],"subject":[],"published":{"date-parts":[[2003,5]]}}}