{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T19:47:56Z","timestamp":1725565676422},"publisher-location":"Berlin, Heidelberg","reference-count":38,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540223450"},{"type":"electronic","value":"9783540259848"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-25984-8_8","type":"book-chapter","created":{"date-parts":[[2010,9,11]],"date-time":"2010-09-11T02:31:38Z","timestamp":1284172298000},"page":"137-151","source":"Crossref","is-referenced-by-count":6,"title":["Attacking a Protocol for Group Key Agreement by Refuting Incorrect Inductive Conjectures"],"prefix":"10.1007","author":[{"given":"Graham","family":"Steel","sequence":"first","affiliation":[]},{"given":"Alan","family":"Bundy","sequence":"additional","affiliation":[]},{"given":"Monika","family":"Maidl","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"8_CR1","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"211","DOI":"10.1007\/3-540-45620-1_18","volume-title":"Automated Deduction - CADE-18","author":"W. Ahrendt","year":"2002","unstructured":"Ahrendt, W.: Deductive search for errors in free data type specifications using model generation. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol.\u00a02392, pp. 211\u2013225. Springer, Heidelberg (2002)"},{"issue":"17","key":"8_CR2","doi-asserted-by":"publisher","first-page":"1627","DOI":"10.1016\/S0140-3664(00)00249-8","volume":"23","author":"N. Asokan","year":"2000","unstructured":"Asokan, N., Ginzboorg, P.: Key-agreement in ad-hoc networks. Computer Communications\u00a023(17), 1627\u20131637 (2000)","journal-title":"Computer Communications"},{"issue":"4","key":"8_CR3","doi-asserted-by":"publisher","first-page":"628","DOI":"10.1109\/49.839937","volume":"18","author":"G. Ateniese","year":"2000","unstructured":"Ateniese, G., Steiner, M., Tsudik, G.: New multiparty authentication services and key agreement protocols. IEEE Journal on Selected Areas in Communications\u00a018(4), 628\u2013639 (2000)","journal-title":"IEEE Journal on Selected Areas in Communications"},{"key":"8_CR4","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4684-7118-2","volume-title":"Canonical Equational Proofs.","author":"L. Bachmair","year":"1991","unstructured":"Bachmair, L.: Canonical Equational Proofs. Birkhauser, Basel (1991)"},{"key":"8_CR5","doi-asserted-by":"crossref","unstructured":"Bachmair, L., Ganzinger, H.: Completion of First-order clauses with equality by strict superposition. In: Proceedings 2nd International CTRS Workshop, Montreal, Canada, pp. 162\u2013180 (1990) (extended abstract)","DOI":"10.1007\/3-540-54317-1_89"},{"key":"#cr-split#-8_CR6.1","doi-asserted-by":"crossref","unstructured":"Basin, D., M\u00f6dersheim, S., Vigan\u00f2, L.: An on-the-fly model-checker for security protocol analysis. In: Proceedings of the 2003 European Symposium on Research in Computer Security, pp. 253\u2013270 (2003);","DOI":"10.1007\/978-3-540-39650-5_15"},{"key":"#cr-split#-8_CR6.2","unstructured":"Extended version available as Technical Report 404, ETH Zurich"},{"key":"8_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"352","DOI":"10.1007\/10930755_23","volume-title":"Theorem Proving in Higher Order Logics","author":"G. Bella","year":"2003","unstructured":"Bella, G.: Verifying second-level security protocols. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol.\u00a02758, pp. 352\u2013366. Springer, Heidelberg (2003)"},{"key":"8_CR8","doi-asserted-by":"crossref","unstructured":"Bond, M., Anderson, R.: API level attacks on embedded systems. IEEE Computer Magazine, 67\u201375 (October 2001)","DOI":"10.1109\/2.955101"},{"issue":"2","key":"8_CR9","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1007\/BF00881856","volume":"14","author":"A. Bouhoula","year":"1995","unstructured":"Bouhoula, A., Rusinowitch, M.: Implicit induction in conditional theories. Journal of Automated Reasoning\u00a014(2), 189\u2013235 (1995)","journal-title":"Journal of Automated Reasoning"},{"key":"8_CR10","unstructured":"Clark, J., Jacob, J.: A survey of authentication protocol literature: Version 1.0 (1997), Available via http:\/\/www.cs.york.ac.uk\/jac\/papers\/drareview.ps.gz"},{"key":"8_CR11","doi-asserted-by":"crossref","unstructured":"Cohen, E.: TAPS a first-order verifier for cryptographic protocols. In: Proceedings of the 13th IEEE Computer Security Foundations Workshop, Cambridge, England, July 2000, pp. 144\u2013158 (2000)","DOI":"10.1109\/CSFW.2000.856933"},{"issue":"1-2","key":"8_CR12","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1006\/inco.2000.2875","volume":"159","author":"H. Comon","year":"2000","unstructured":"Comon, H., Nieuwenhuis, R.: Induction = I-Axiomatization + First-Order Consistency. Information and Computation\u00a0159(1-2), 151\u2013186 (2000)","journal-title":"Information and Computation"},{"issue":"29","key":"8_CR13","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1109\/TIT.1983.1056650","volume":"2","author":"D. Dolev","year":"1983","unstructured":"Dolev, D., Yao, A.: On the security of public key protocols. IEEE Transactions in Information Theory\u00a02(29), 198\u2013208 (1983)","journal-title":"IEEE Transactions in Information Theory"},{"key":"8_CR14","unstructured":"Durgin, N., Lincoln, P., Mitchell, J., Scedrov, A.: Undecidability of bounded security protocols. In: Heintze, N., Clarke, E. (eds.) Proceedings of the Workshop on Formal Methods and Security Protocols \u2014 FMSP, Trento, Italy (July 1999), Electronic proceedings available at http:\/\/www.cs.bell-labs.com\/who\/nch\/fmsp99\/program.html"},{"key":"8_CR15","doi-asserted-by":"crossref","first-page":"191","DOI":"10.3233\/JCS-1999-72-304","volume":"7","author":"F. F\u00e1brega","year":"1999","unstructured":"F\u00e1brega, F., Herzog, J.: Strand spaces: Proving security protocols correct. Journal of Computer Security\u00a07, 191\u2013230 (1999)","journal-title":"Journal of Computer Security"},{"key":"8_CR16","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"Automated Deduction - CADE-16","year":"1999","unstructured":"Ganzinger, H. (ed.): CADE 1999. LNCS (LNAI), vol.\u00a01632. Springer, Heidelberg (1999)"},{"key":"8_CR17","doi-asserted-by":"crossref","first-page":"441","DOI":"10.1007\/978-3-322-95233-2_27","volume-title":"Informatik \u2014 Festschrift zum 60, Geburtstag von G\u00fcnter Hotz","author":"H. Ganzinger","year":"1992","unstructured":"Ganzinger, H., Stuber, J.: Inductive theorem proving by consistency for first-order clauses. In: Informatik \u2014 Festschrift zum 60, Geburtstag von G\u00fcnter Hotz, pp. 441\u2013462. Teubner, Stuttgart (1992)"},{"key":"8_CR18","unstructured":"Green, C.: Theorem proving by resolution as a basis for question-answering systems. In: Meltzer, B., Michie, D. (eds.) Machine Intelligence, vol.\u00a04, pp. 183\u2013208. Edinburgh University Press (1969)"},{"key":"8_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1007\/3-540-61042-1_43","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G. Lowe","year":"1996","unstructured":"Lowe, G.: Breaking and fixing the Needham Schroeder public-key protocol using FDR. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol.\u00a01055, pp. 147\u2013166. Springer, Heidelberg (1996)"},{"issue":"2","key":"8_CR20","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":"8_CR21","doi-asserted-by":"crossref","unstructured":"Meadows, C.: Extending formal cryptographic protocol analysis techniques for group protocols and low-level cryptographic primitives. In: Degano, P. (ed.) Proceedings of the First Workshop on Issues in the Theory of Security, Geneva, Switzerland, July 2000, pp. 87\u201392 (2000)","DOI":"10.21236\/ADA464085"},{"key":"8_CR22","doi-asserted-by":"publisher","first-page":"238","DOI":"10.1109\/DISCEX.2003.1194888","volume-title":"DISCEX III, DARPA Information Survivability Conference and Exposition","author":"J. Millen","year":"2003","unstructured":"Millen, J., Denker, G.: MuCAPSL. In: DISCEX III, DARPA Information Survivability Conference and Exposition, pp. 238\u2013249. IEEE Computer Society, Los Alamitos (2003)"},{"key":"8_CR23","doi-asserted-by":"crossref","unstructured":"Millen, J., Shmatikov, V.: Symbolic protocol analysis with products and Diffie- Hellman exponentiation. In: 16th IEEE Computer Security Foundations Workshop, pp. 47\u201361 (2003)","DOI":"10.1109\/CSFW.2003.1212704"},{"key":"8_CR24","first-page":"154","volume-title":"Proceedings 7th ACM Symp. on Principles of Programming Languages","author":"D. Musser","year":"1980","unstructured":"Musser, D.: On proving inductive properties of abstract data types. In: Proceedings 7th ACM Symp. on Principles of Programming Languages, pp. 154\u2013162. ACM, New York (1980)"},{"issue":"12","key":"8_CR25","doi-asserted-by":"publisher","first-page":"993","DOI":"10.1145\/359657.359659","volume":"21","author":"R. Needham","year":"1978","unstructured":"Needham, R., Schroeder, M.: Using encryption for authentication in large networks of computers. Communications of the ACM\u00a021(12), 993\u2013999 (1978)","journal-title":"Communications of the ACM"},{"key":"8_CR26","series-title":"Lecture Notes in Computer Science","volume-title":"Isabelle","year":"1994","unstructured":"Paulson, L.C. (ed.): Isabelle. LNCS, vol.\u00a0828. Springer, Heidelberg (1994)"},{"key":"8_CR27","doi-asserted-by":"crossref","first-page":"85","DOI":"10.3233\/JCS-1998-61-205","volume":"6","author":"L.C. Paulson","year":"1998","unstructured":"Paulson, L.C.: The Inductive Approach to Verifying Cryptographic Protocols. Journal of Computer Security\u00a06, 85\u2013128 (1998)","journal-title":"Journal of Computer Security"},{"issue":"4","key":"8_CR28","doi-asserted-by":"crossref","first-page":"555","DOI":"10.3233\/JCS-2003-11404","volume":"11","author":"O. Pereira","year":"2003","unstructured":"Pereira, O., Quisquater, J.-J.: Some attacks upon authenticated group key agreement protocols. Journal of Computer Security\u00a011(4), 555\u2013580 (2003); Special Issue: 14th Computer Security Foundations Workshop (CSFW14)","journal-title":"Journal of Computer Security"},{"key":"8_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"340","DOI":"10.1007\/3-540-55602-8_176","volume-title":"Automated Deduction - CADE-11","author":"M. Protzen","year":"1992","unstructured":"Protzen, M.: Disproving conjectures. In: Kapur, D. (ed.) CADE 1992. LNCS, vol.\u00a0607, pp. 340\u2013354. Springer, Heidelberg (1992)"},{"key":"8_CR30","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"642","DOI":"10.1007\/3-540-45744-5_52","volume-title":"Automated Reasoning","author":"W. Reif","year":"2001","unstructured":"Reif, W., Schellhorn, G., Thums, A.: Flaw detection in formal specifications. In: Gor\u00e9, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol.\u00a02083, pp. 642\u2013657. Springer, Heidelberg (2001)"},{"issue":"1\/2","key":"8_CR31","doi-asserted-by":"crossref","first-page":"47","DOI":"10.3233\/JCS-2001-91-203","volume":"9","author":"D. Song","year":"2001","unstructured":"Song, D., Berezin, S., Perrig, A.: Athena: A novel approach to efficient automatic security protocol analysis. Journal of Computer Security\u00a09(1\/2), 47\u201374 (2001)","journal-title":"Journal of Computer Security"},{"key":"8_CR32","unstructured":"Steel, G., Bundy, A., Denney, E.: Finding counterexamples to inductive conjectures and discovering security protocol attacks. In: Proceedings of the Foundations of Computer Security Workshop, FLoC (2002), Also available as Informatics Research Report 141 http:\/\/www.inf.ed.ac.uk\/publications\/report\/0141.html"},{"key":"8_CR33","doi-asserted-by":"crossref","unstructured":"Syverson, P., Meadows, C., Cerversato, I.: Dolev-Yao is no better than machiavelli. In: Degano, P. (ed.) Proceedings of the First Workshop on Issues in the Theory of Security, Geneva, Switzerland, pp. 87\u201392 (2000)","DOI":"10.21236\/ADA464936"},{"key":"8_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"240","DOI":"10.1007\/978-3-540-39979-7_16","volume-title":"Formal Techniques for Networked and Distributed Systems - FORTE 2003","author":"M. Tagdhiri","year":"2003","unstructured":"Tagdhiri, M., Jackson, D.: A lightweight formal analysis of a multicast key management scheme. In: K\u00f6nig, H., Heiner, M., Wolisz, A. (eds.) FORTE 2003. LNCS, vol.\u00a02767, pp. 240\u2013256. Springer, Heidelberg (2003)"},{"key":"8_CR35","doi-asserted-by":"crossref","unstructured":"Tanaka, S., Sato, F.: A key distribution and rekeying framework with totally ordered multicast protocols. In: Proceedings of the 15th International Conference on Information Networking, pp. 831\u2013838 (2001)","DOI":"10.1109\/ICOIN.2001.905598"},{"key":"8_CR36","doi-asserted-by":"crossref","unstructured":"Weidenbach, C.: Towards an automatic analysis of security protocols in first-order logic. In: Ganzinger [16], pp. 314\u2013328","DOI":"10.1007\/3-540-48660-7_29"},{"key":"8_CR37","doi-asserted-by":"crossref","unstructured":"Weidenbach, C., et al.: System description: Spass version 1.0.0. In: Ganzinger [16], pp. 378\u2013382","DOI":"10.1007\/3-540-48660-7_34"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-25984-8_8.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,3]],"date-time":"2023-06-03T07:31:17Z","timestamp":1685777477000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-25984-8_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540223450","9783540259848"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-25984-8_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}