{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T06:39:51Z","timestamp":1725518391498},"publisher-location":"Berlin, Heidelberg","reference-count":50,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540710691"},{"type":"electronic","value":"9783540710707"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-71070-7_34","type":"book-chapter","created":{"date-parts":[[2008,8,29]],"date-time":"2008-08-29T09:56:30Z","timestamp":1220003790000},"page":"396-409","source":"Crossref","is-referenced-by-count":2,"title":["Challenges in the Automated Verification of Security Protocols"],"prefix":"10.1007","author":[{"given":"Hubert","family":"Comon-Lundh","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"1\u20132","key":"34_CR1","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1016\/j.tcs.2006.08.032","volume":"367","author":"M. Abadi","year":"2006","unstructured":"Abadi, M., Cortier, V.: Deciding knowledge in security protocols under equational theories. Theoretical Computer Science\u00a0367(1\u20132), 2\u201332 (2006)","journal-title":"Theoretical Computer Science"},{"key":"34_CR2","doi-asserted-by":"crossref","unstructured":"Abadi, M., Fournet, C.: Mobile values, new names, and secure communication. In: Proceedings of the 28th ACM Symposium on Principles of Programming Languages (POPL 2001), January 2001, pp. 104\u2013115 (2001)","DOI":"10.1145\/360204.360213"},{"key":"34_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44929-9_1","volume-title":"Theoretical Computer Science: Exploring New Frontiers of Theoretical Informatics","author":"M. Abadi","year":"2000","unstructured":"Abadi, M., Rogaway, P.: Reconciling two views of cryptography: the computational soundness of formal encryption. In: Watanabe, O., Hagiya, M., Ito, T., van Leeuwen, J., Mosses, P.D. (eds.) TCS 2000. LNCS, vol.\u00a01872. Springer, Heidelberg (2000)"},{"key":"34_CR4","unstructured":"Affeldt, R., Comon-Lundh, H.: First-order logic and security protocols (unpublished manuscript) (April 2008)"},{"key":"34_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73449-9_4","volume-title":"Term Rewriting and Applications","author":"S. Anantharaman","year":"2007","unstructured":"Anantharaman, S., Narendran, P., Rusinowitch, M.: Intruders with caps. In: Baader, F. (ed.) RTA 2007. LNCS, vol.\u00a04533. Springer, Heidelberg (2007)"},{"key":"34_CR6","doi-asserted-by":"crossref","unstructured":"Arapinis, M., Delaune, S., Kremer, S.: From one session to many: Dynamic tags for security protocols. Research Report LSV-08-16, Laboratoire Sp\u00e9cification et V\u00e9rification, ENS Cachan, France (May 2008)","DOI":"10.1007\/978-3-540-89439-1_9"},{"key":"34_CR7","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74621-8_7","volume-title":"Frontiers of Combining Systems","author":"M. Arnaud","year":"2007","unstructured":"Arnaud, M., Cortier, V., Delaune, S.: Combining algorithms for deciding knowledge in security protocols. In: Konev, B., Wolter, F. (eds.) FroCos 2007. LNCS (LNAI), vol.\u00a04720. Springer, Heidelberg (2007)"},{"issue":"1","key":"34_CR8","doi-asserted-by":"crossref","first-page":"70","DOI":"10.1145\/363647.363681","volume":"48","author":"D. Basin","year":"2001","unstructured":"Basin, D., Ganzinger, H.: Automated complexity analysis based on ordered resolution. Journal of the Association of Computing Machinery\u00a048(1), 70\u2013109 (2001)","journal-title":"Journal of the Association of Computing Machinery"},{"key":"34_CR9","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1145\/948109.948154","volume-title":"Proceedings of CCS 2003","author":"D. Basin","year":"2003","unstructured":"Basin, D., M\u00f6dersheim, S., Vigan\u00f2, L.: Constraint Differentiation: A New Reduction Technique for Constraint-Based Analysis of Security Protocols. In: Proceedings of CCS 2003, pp. 335\u2013344. ACM Press, New York (2003)"},{"key":"34_CR10","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","DOI":"10.1007\/11591191_38","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"D. Basin","year":"2005","unstructured":"Basin, D., M\u00f6dersheim, S., Vigan\u00f2, L.: Algebraic intruder deductions. In: Sutcliffe, G., Voronkov, A. (eds.) LPAR 2005. LNCS (LNAI), vol.\u00a03835. Springer, Heidelberg (2005)"},{"key":"34_CR11","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1145\/1102120.1102125","volume-title":"Proceedings of the 12th ACM Conference on Computer and Communications Security (CCS 2005)","author":"M. Baudet","year":"2005","unstructured":"Baudet, M.: Deciding security of protocols against off-line guessing attacks. In: Proceedings of the 12th ACM Conference on Computer and Communications Security (CCS 2005), Alexandria, Virginia, USA, November 2005, pp. 16\u201325. ACM Press, New York (2005)"},{"key":"34_CR12","unstructured":"Baudet, M.: S\u00e9curit\u00e9 des protocoles cryptographiques\u00a0: aspects logiques et calculatoires. Th\u00e8se de doctorat, Laboratoire Sp\u00e9cification et V\u00e9rification, ENS Cachan, France (January 2007)"},{"key":"34_CR13","unstructured":"Baudet, M.: Yapa: Yet another protocol analyser (2008), http:\/\/www.lsv.ens-cachan.fr\/~baudet\/yapa\/index.html"},{"key":"34_CR14","series-title":"Lecture Notes in Computer Science","volume-title":"Revised Selected Papers of the 11th Asian Computing Science Conference (ASIAN 2006)","author":"V. Bernat","year":"2008","unstructured":"Bernat, V., Comon-Lundh, H.: Normal proofs in intruder theories. In: Revised Selected Papers of the 11th Asian Computing Science Conference (ASIAN 2006). LNCS, vol.\u00a04435. Springer, Heidelberg (2008)"},{"key":"34_CR15","first-page":"82","volume-title":"14th IEEE Computer Security Foundations Workshop (CSFW-14)","author":"B. Blanchet","year":"2001","unstructured":"Blanchet, B.: An Efficient Cryptographic Protocol Verifier Based on Prolog Rules. In: 14th IEEE Computer Security Foundations Workshop (CSFW-14), Cape Breton, Nova Scotia, Canada, June 2001, pp. 82\u201396. IEEE Computer Society, Los Alamitos (2001)"},{"key":"34_CR16","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"Automated Deduction \u2013 CADE-20","author":"B. Blanchet","year":"2005","unstructured":"Blanchet, B.: An automatic security protocol verifier based on resolution theorem proving (invited tutorial). In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol.\u00a03632. Springer, Heidelberg (2005)"},{"issue":"1","key":"34_CR17","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.jlap.2007.06.002","volume":"75","author":"B. Blanchet","year":"2008","unstructured":"Blanchet, B., Abadi, M., Fournet, C.: Automated verification of selected equivalences for security protocols. Journal of Logic and Algebraic Programming\u00a075(1), 3\u201351 (2008)","journal-title":"Journal of Logic and Algebraic Programming"},{"issue":"1\u20132","key":"34_CR18","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1016\/j.tcs.2004.10.018","volume":"333","author":"B. Blanchet","year":"2005","unstructured":"Blanchet, B., Podelski, A.: Verification of cryptographic protocols: Tagging enforces termination. Theoretical Computer Science\u00a0333(1\u20132), 67\u201390 (2005)","journal-title":"Theoretical Computer Science"},{"key":"34_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73147-4_10","volume-title":"Rewriting, Computation and Proof","author":"S. Bursuc","year":"2007","unstructured":"Bursuc, S., Comon-Lundh, H., Delaune, S.: Deducibility constraints, equational theory and electronic money. In: Comon-Lundh, H., Kirchner, C., Kirchner, H. (eds.) Jouannaud Festschrift. LNCS, vol.\u00a04600. Springer, Heidelberg (2007)"},{"key":"34_CR20","doi-asserted-by":"crossref","unstructured":"Canetti, R., Rabin, T.: Universal composition with joint state. Cryptology ePrint Archive, report 2002\/47 (November 2003)","DOI":"10.1007\/978-3-540-45146-4_16"},{"key":"34_CR21","series-title":"Lecture Notes in Computer Science","volume-title":"FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science","author":"Y. Chevalier","year":"2003","unstructured":"Chevalier, Y., K\u00fcsters, R., Rusinowitch, M., Turuani, M.: Deciding the security of protocols with Diffie-Hellman exponentiation and products in exponents. In: Pandya, P.K., Radhakrishnan, J. (eds.) FSTTCS 2003. LNCS, vol.\u00a02914. Springer, Heidelberg (2003)"},{"key":"34_CR22","doi-asserted-by":"crossref","unstructured":"Chevalier, Y., K\u00fcsters, R., Rusinowitch, M., Turuani, M.: An NP decision procedure for protocol insecurity with XOR. In: Eighteenth Annual IEEE Symposium on Logic in Computer Science (LICS) (2003)","DOI":"10.1109\/LICS.2003.1210066"},{"key":"34_CR23","doi-asserted-by":"crossref","unstructured":"Chevalier, Y., K\u00fcsters, R., Rusinowitch, M., Turuani, M.: Deciding the security of protocols with commuting public key encryption. In: Proc. Workshop on Automated Reasoning for Security Protocol Analysis (ARSPA). Electronic Notes in Theoretical Computer Science, vol.\u00a0125 (2004)","DOI":"10.1016\/j.entcs.2004.05.019"},{"key":"34_CR24","series-title":"Lecture Notes in Computer Science","volume-title":"Automata, Languages and Programming","author":"Y. Chevalier","year":"2005","unstructured":"Chevalier, Y., Rusinowitch, M.: Combining Intruder Theories. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds.) ICALP 2005. LNCS, vol.\u00a03580. Springer, Heidelberg (2005)"},{"key":"34_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/11805618_9","volume-title":"Term Rewriting and Applications","author":"Y. Chevalier","year":"2006","unstructured":"Chevalier, Y., Rusinowitch, M.: Hierarchical Combination of Intruder Theories. In: Pfenning, F. (ed.) RTA 2006. LNCS, vol.\u00a04098, pp. 108\u2013122. Springer, Heidelberg (2006)"},{"issue":"1","key":"34_CR26","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1016\/j.tcs.2004.09.036","volume":"331","author":"H. Comon","year":"2005","unstructured":"H.\u00a0Comon and V.\u00a0Cortier. Tree automata with one memory, set constraints and cryptographic protocols. Theoretical Computer Science, 331(1):143\u2013214, Feb. 2005.","journal-title":"Theoretical Computer Science"},{"key":"34_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44881-0_12","volume-title":"Rewriting Techniques and Applications","author":"H. Comon-Lundh","year":"2003","unstructured":"Comon-Lundh, H., Cortier, V.: New decidability results for fragments of first-order logic and application to cryptographic protocols. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol.\u00a02706. Springer, Heidelberg (2003)"},{"issue":"1-3","key":"34_CR28","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1016\/j.scico.2003.12.002","volume":"50","author":"H. Comon-Lundh","year":"2004","unstructured":"Comon-Lundh, H., Cortier, V.: Security properties: Two agents are sufficient. Science of Computer Programming\u00a050(1-3), 51\u201371 (2004)","journal-title":"Science of Computer Programming"},{"key":"34_CR29","series-title":"Lecture Notes in Computer Science","volume-title":"Term Rewriting and Applications","author":"H. Comon-Lundh","year":"2005","unstructured":"Comon-Lundh, H., Delaune, S.: The finite variant property: How to get rid of some algebraic properties. In: Giesl, J. (ed.) RTA 2005. LNCS, vol.\u00a03467. Springer, Heidelberg (2005)"},{"key":"34_CR30","series-title":"Lecture Notes in Computer Science","volume-title":"Verification: Theory and Practice","author":"H. Comon-Lundh","year":"2004","unstructured":"Comon-Lundh, H., Treinen, R.: Easy intruder deductions. In: Dershowitz, N. (ed.) Verification: Theory and Practice. LNCS, vol.\u00a02772. Springer, Heidelberg (2004)"},{"key":"34_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-77050-3_29","volume-title":"FSTTCS 2007: Foundations of Software Technology and Theoretical Computer Science","author":"V. Cortier","year":"2007","unstructured":"Cortier, V., Delaitre, J., Delaune, S.: Safely composing security protocols. In: Arvind, V., Prasad, S. (eds.) FSTTCS 2007. LNCS, vol.\u00a04855. Springer, Heidelberg (2007)"},{"key":"34_CR32","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-75560-9_16","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"V. Cortier","year":"2007","unstructured":"Cortier, V., Delaune, S.: Deciding knowledge in security protocols for monoidal equational theories. In: Dershowitz, N., Voronkov, A. (eds.) LPAR 2007. LNCS (LNAI), vol.\u00a04790. Springer, Heidelberg (2007)"},{"issue":"1","key":"34_CR33","doi-asserted-by":"crossref","first-page":"1","DOI":"10.3233\/JCS-2006-14101","volume":"14","author":"V. Cortier","year":"2006","unstructured":"Cortier, V., Delaune, S., Lafourcade, P.: A survey of algebraic properties used in cryptographic protocols. Journal of Computer Security\u00a014(1), 1\u201343 (2006)","journal-title":"Journal of Computer Security"},{"key":"34_CR34","doi-asserted-by":"crossref","unstructured":"Cortier, V., Rusinowitch, M., Zalinescu, E.: A resolution strategy for verifying cryptographic protocols with CBC encryption and blind signatures. In: 7th ACM-SIGPLAN International Conference on Principles and Practice of Declarative Programming (PPDP) (2005)","DOI":"10.1145\/1069774.1069776"},{"issue":"6","key":"34_CR35","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1016\/j.ipl.2005.11.008","volume":"97","author":"S. Delaune","year":"2006","unstructured":"Delaune, S.: Easy intruder deduction problems with homomorphisms. Information Processing Letters\u00a097(6), 213\u2013218 (2006)","journal-title":"Information Processing Letters"},{"key":"34_CR36","volume-title":"Proceedings of the 19th Computer Security Foundations Workshop (CSFW)","author":"S. Delaune","year":"2006","unstructured":"Delaune, S., Kremer, S., Ryan, M.D.: Coercion-resistance and receipt-freeness in electronic voting. In: Proceedings of the 19th Computer Security Foundations Workshop (CSFW), IEEE Computer Society Press, Los Alamitos (2006)"},{"key":"34_CR37","doi-asserted-by":"publisher","first-page":"312","DOI":"10.1016\/j.ic.2007.07.005","volume":"206","author":"S. Delaune","year":"2008","unstructured":"Delaune, S., Lafourcade, P., Lugiez, D., Treinen, R.: Symbolic protocol analysis for monoidal equational theories. Information and Computation\u00a0206, 312\u2013351 (2008)","journal-title":"Information and Computation"},{"key":"34_CR38","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-75560-9_19","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"S. Delaune","year":"2007","unstructured":"Delaune, S., Lin, H.: Protocol verification via rigid\/flexible resolution. In: Dershowitz, N., Voronkov, A. (eds.) LPAR 2007. LNCS (LNAI), vol.\u00a04790, Springer, Heidelberg (2007)"},{"key":"34_CR39","first-page":"1793","volume-title":"Handbook of Automated Reasoning, ch. 25","author":"C. Ferm\u00fcller","year":"2001","unstructured":"Ferm\u00fcller, C., Leitsch, A., Hustadt, U., Tamet, T.: Resolution decision procedure. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, ch. 25, vol.\u00a02, pp. 1793\u20131849. North-Holland, Amsterdam (2001)"},{"key":"34_CR40","unstructured":"Huttel, H.: Deciding framed bisimulation. In: 4th International Workshop on Verification of Infinite State Systems INFINITY 2002, pp. 1\u201320 (2002)"},{"key":"34_CR41","doi-asserted-by":"crossref","unstructured":"K\u00fcsters, R., Tuengerthal, M.: Joint state theorems for public-key encryption and digital signature functionalities with local computations. In: Computer Security Foundations (CSF 2008) (2008)","DOI":"10.1109\/CSF.2008.18"},{"issue":"3","key":"34_CR42","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1016\/0020-0190(95)00144-2","volume":"56","author":"G. Lowe","year":"1996","unstructured":"Lowe, G.: An attack on the Needham-Schroeder public-key authentication protocol. Information Processing Letters\u00a056(3), 131\u2013133 (1996)","journal-title":"Information Processing Letters"},{"key":"34_CR43","doi-asserted-by":"crossref","unstructured":"Lowe, G.: Towards a completeness result for model checking of security protocols. Journal of Computer Security\u00a07(1) (1999)","DOI":"10.3233\/JCS-1999-72-302"},{"key":"34_CR44","doi-asserted-by":"crossref","unstructured":"McAllester, D.: Automatic recognition of tractability in inference relations. J.\u00a0ACM\u00a040(2) (1993)","DOI":"10.1145\/151261.151265"},{"issue":"2","key":"34_CR45","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1016\/0743-1066(95)00095-X","volume":"26","author":"C. Meadows","year":"1996","unstructured":"Meadows, C.: The NRL protocol analyzer: An overview. Journal of Logic Programming\u00a026(2), 113\u2013131 (1996)","journal-title":"Journal of Logic Programming"},{"key":"34_CR46","doi-asserted-by":"crossref","unstructured":"Millen, J., Shmatikov, V.: Symbolic protocol analysis with an Abelian group operator or Diffie-Hellman exponentiation. J. Computer Security (2005)","DOI":"10.3233\/JCS-2005-13404"},{"key":"34_CR47","doi-asserted-by":"crossref","unstructured":"Millen, J.K., Ko, H.-P.: Narrowing terminates for encryption. In: Proc. Ninth IEEE Computer Security Foundations Workshop (CSFW) (1996)","DOI":"10.1109\/CSFW.1996.503689"},{"key":"34_CR48","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"363","DOI":"10.1007\/978-3-540-24597-1_31","volume-title":"FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science","author":"R. Ramanujam","year":"2003","unstructured":"Ramanujam, R., Suresh, S.P.: Tagging makes secrecy decidable with unbounded nonces as well. In: Pandya, P.K., Radhakrishnan, J. (eds.) FSTTCS 2003. LNCS, vol.\u00a02914, pp. 363\u2013374. Springer, Heidelberg (2003)"},{"key":"34_CR49","doi-asserted-by":"crossref","unstructured":"Rusinowitch, M., Turuani, M.: Protocol insecurity with finite number of sessions is np-complete. In: Proc. 14th IEEE Computer Security Foundations Workshop, Cape Breton, Nova Scotia (June 2001)","DOI":"10.1109\/CSFW.2001.930145"},{"key":"34_CR50","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"314","DOI":"10.1007\/3-540-48660-7_29","volume-title":"Automated Deduction - CADE-16","author":"C. Weidenbach","year":"1999","unstructured":"Weidenbach, C.: Towards an automatic analysis of security protocols in first-order logic. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol.\u00a01632, pp. 314\u2013328. Springer, Heidelberg (1999)"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-71070-7_34.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,19]],"date-time":"2023-05-19T19:48:55Z","timestamp":1684525735000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-71070-7_34"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540710691","9783540710707"],"references-count":50,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-71070-7_34","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}