{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T22:02:38Z","timestamp":1743026558057,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540631040"},{"type":"electronic","value":"9783540691402"}],"license":[{"start":{"date-parts":[[1997,1,1]],"date-time":"1997-01-01T00:00:00Z","timestamp":852076800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1997]]},"DOI":"10.1007\/3-540-63104-6_12","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T23:03:43Z","timestamp":1330297423000},"page":"87-100","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":14,"title":["Automatic verification of cryptographic protocols with SETHEO"],"prefix":"10.1007","author":[{"given":"Johann","family":"Schumann","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,8]]},"reference":[{"key":"12_CR1","doi-asserted-by":"crossref","unstructured":"M. Abadi and M. R. Tuttle. A Semantics for a Logic of Authentication. In Proc. of the Tenth Annual ACM Symp. on Principles of Distributed Computing, pages 201\u2013216. ACM press, 1991.","DOI":"10.1145\/112600.112618"},{"key":"12_CR2","unstructured":"S. H. Brackin. A HOL Extension of GNY for Automatically Analyzing Cryptographic Protocols. In Proc. IEEE Computer Security Foundations Workshop IX. IEEE, 1996."},{"key":"12_CR3","doi-asserted-by":"crossref","unstructured":"M. Burrows, M. Abadi, and R. Needham. A Logic of Authentication. In ACM Operating Systems Review 23(5)\/Proceedings of the Twelfth ACM Symposium on Operating Systems Principles, 1989.","DOI":"10.1145\/74851.74852"},{"issue":"1","key":"12_CR4","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1145\/77648.77649","volume":"8","author":"M. Burrows","year":"1990","unstructured":"M. Burrows, M. Abadi, and R. Needham. A Logic of Authentication. ACM Transactions on Computer Systems, 8(1):18\u201336, 1990.","journal-title":"ACM Transactions on Computer Systems"},{"key":"12_CR5","unstructured":"D. Craigen and M. Saaltink. Using EVES to Analyze Authentication Protocols. Technical Report TR-96-5508-05, ORA Canada, 1996."},{"key":"12_CR6","unstructured":"J. Geiger. Formale Methoden zur Verifikation kryptographischer Protokolle. Fortgeschrittenenpraktikum, Institut f\u00fcr Informatik, Technische Universit\u00e4t M\u00fcnchen, 1995. in German."},{"key":"12_CR7","first-page":"778","volume":"12","author":"C. Goller","year":"1994","unstructured":"Chr. Goller, R. Letz, K. Mayr, and J. Schumann. SETHEO V3.2: Recent Developments (System Abstract). In Proc. CADE 12, pages 778\u2013782, 1994.","journal-title":"Proc. CADE"},{"key":"12_CR8","first-page":"234","volume-title":"Reasoning about belief in cryptographic protocols","author":"L. Gong","year":"1990","unstructured":"L. Gong, R. Needham, and R. Yahalom. Reasoning about belief in cryptographic protocols. In Proc. of IEEE Symposium on Security and Privacy, Oakland, Ca., USA, pages 234\u2013248. IEEE, 1990."},{"key":"12_CR9","doi-asserted-by":"crossref","unstructured":"M. J. C. Gordon. HOL: A proof generating system for higher-order logic. In G. Birtwistle and P. A. Subrahmanyam, editors, VLSI Specification, Verification and Synthesis, pages 73\u2013128. Kluwer, 1988.","DOI":"10.1007\/978-1-4613-2007-4_3"},{"key":"12_CR10","doi-asserted-by":"crossref","unstructured":"V. Kessler and G. Wedel. AUTLOG \u2014 An Advanced Logic of Authentication. In Proc. IEEE Computer Security Foundations Workshop IV, pages 90\u201399. IEEE, 1994.","DOI":"10.1109\/CSFW.1994.315944"},{"key":"12_CR11","unstructured":"D. Kindred and J. Wing. Fast, automatic checking of security protocols. In 2nd USENIX Workshop on Electronic Commerce, pages 41\u201352, 1996."},{"key":"12_CR12","doi-asserted-by":"crossref","unstructured":"R. Letz, K. Mayr, and C. Goller. Controlled Integration of the Cut Rule into Connection Tableau Calculi. Journal Automated Reasoning, (13):297\u2013337, 1994.","DOI":"10.1007\/BF00881947"},{"issue":"2","key":"12_CR13","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1007\/BF00244282","volume":"8","author":"R. Letz","year":"1992","unstructured":"R. Letz, J. Schumann, S. Bayerl, and W. Bibel. SETHEO: A High-Performance Theorem Prover. Journal Automated Reasoning, 8(2):183\u2013212, 1992.","journal-title":"Journal Automated Reasoning"},{"key":"12_CR14","unstructured":"D. W. Loveland. Automated Theorem Proving: a Logical Basis. North-Holland, 1978."},{"key":"12_CR15","doi-asserted-by":"crossref","unstructured":"W. W. McCune and L. Wos. Experiments in Automated Deduction with Condensed Detachment. Technical report, Argonne National Laboratory, 1991.","DOI":"10.1007\/3-540-55602-8_167"},{"key":"12_CR16","doi-asserted-by":"crossref","unstructured":"C. A. Meadows. Formal verification of Cryptographic Protocols: A Survey. In Proc. AsiaCrypt, 1994.","DOI":"10.21236\/ADA464292"},{"key":"12_CR17","doi-asserted-by":"crossref","unstructured":"J. Millen, S. Clark, and S. Freedman. The interrogator protocol security analysis. IEEE Trans. Software Engineering, SE-13(2), 1987.","DOI":"10.1109\/TSE.1987.233151"},{"key":"12_CR18","unstructured":"J. K. Millen. CAPSL: Common Authentication Protocol Specification Language. http:\/\/www.mitre.org\/research\/capsl\/, 1996."},{"key":"12_CR19","unstructured":"M. Moser, O. Ibens, R. Letz, J. Steinbach, Chr. Goller, J. Schumann, and K. Mayr. The Model Elimination Provers SETHEO and E-SETHEO. Special issue of the Journal of Automated Reasoning, 1997. (to appear)."},{"key":"12_CR20","doi-asserted-by":"crossref","unstructured":"P. G. Neumann. Computer Related Risks. ACM Press, 1995.","DOI":"10.1016\/0142-0496(95)80220-7"},{"key":"12_CR21","doi-asserted-by":"crossref","unstructured":"J. Schumann. DELTA \u2014 A Bottom-up Preprocessor for Top-Down Theorem Provers, System Abstract. In Proc. CADE 12, Springer, 1994.","DOI":"10.1007\/3-540-58156-1_58"},{"key":"12_CR22","doi-asserted-by":"crossref","unstructured":"P. F. Syverson and P. van Oorschot. On Unifying Some Cryptographic Protocol Logics. In Proc. of the IEEE Comp. Soc. Sympos. on Research in Security and Privacy, pages 14\u201328, 1994.","DOI":"10.21236\/ADA465512"},{"key":"12_CR23","unstructured":"Klaus Wagner. SIL: Ein SETHEO-basiertes Werkzeug zur Analyse kryptographischer Protokolle. Fortgeschrittenenpraktikum, Technische Universit\u00e4t M\u00fcnchen, 1997. in German."},{"key":"12_CR24","doi-asserted-by":"crossref","unstructured":"Andreas Wolf and Johann Schumann. ILF-SETHEO: Processing Model Elimination Proofs for Natural Language Output (System Description). In Proc. CADE 14, 1997.","DOI":"10.1007\/3-540-63104-6_8"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction\u2014CADE-14"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-63104-6_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,21]],"date-time":"2025-03-21T23:36:26Z","timestamp":1742600186000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-63104-6_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540631040","9783540691402"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/3-540-63104-6_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1997]]},"assertion":[{"value":"8 June 2005","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}