{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T14:12:46Z","timestamp":1725631966928},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540615873"},{"type":"electronic","value":"9783540706410"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/bfb0105397","type":"book-chapter","created":{"date-parts":[[2011,11,9]],"date-time":"2011-11-09T21:17:00Z","timestamp":1320873420000},"page":"61-76","source":"Crossref","is-referenced-by-count":8,"title":["Deciding cryptographic protocol adequacy with HOL: The implementation"],"prefix":"10.1007","author":[{"given":"Stephen H.","family":"Brackin","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2007,4,29]]},"reference":[{"key":"5_CR1","doi-asserted-by":"crossref","unstructured":"S. Brackin. Deciding cryptographic protocol adequacy with HOL. In Higher Order Logic Theorem Proving and Its Applications, number 971 in Lecture Notes in Computer Science, pages 90\u2013105, Aspen Grove, UT, September 1995. Springer-Verlag.","DOI":"10.1007\/3-540-60275-5_59"},{"key":"5_CR2","unstructured":"S. Brackin. Automatic formal analyses of cryptographic protocols. To Appear in the 19th National Conference on Information Systems Security, Baltimore, MD, October 1996."},{"key":"5_CR3","doi-asserted-by":"crossref","unstructured":"S. Brackin. A. HOL extension of GNY for automatically analyzing cryptographic protocols. In Proceedings of Computer Security Foundations Workshop IX, Country Kerry, Ireland, June 1996. IEEE.","DOI":"10.1109\/CSFW.1996.503691"},{"key":"5_CR4","unstructured":"S. Brackin. An interface specification language for cryptographic protocols and its translation into HOL. Submitted to the New Security Paradigms Workshop, Arrowhead, CA, September 1996."},{"key":"5_CR5","doi-asserted-by":"crossref","unstructured":"S. Brackin and S-K Chin. Server-process restrictiveness in HOL. In Higher Order Logic Theorem Proving and Its Applications, number 780 in Lecture Notes in Computer Science, pages 454\u2013467, Vancouver, BC, August 1993. Springer-Verlag.","DOI":"10.1007\/3-540-57826-9_155"},{"key":"5_CR6","series-title":"Technical Report","volume-title":"Reasoning with inductively defined relations in the HOL theorem prover","author":"J. Camilleri","year":"1992","unstructured":"J. Camilleri and T. Melham. Reasoning with inductively defined relations in the HOL theorem prover. Technical Report 265, University of Cambridge Computer Laboratory, Cambridge, UK, August 1992."},{"issue":"8","key":"5_CR7","doi-asserted-by":"crossref","first-page":"533","DOI":"10.1145\/358722.358740","volume":"24","author":"D. Denning","year":"1981","unstructured":"D. Denning and G. Sacco. Timestamps in key distribution protocols. CACM, 24(8):533\u2013536, August 1981.","journal-title":"CACM"},{"key":"5_CR8","doi-asserted-by":"crossref","unstructured":"L. Gong. Handling infeasible specifications of cryptographic protocols. In Proceedings of Computer Security Foundations Workshop IV, pages 99\u2013102, Franconia NH, June 1991. IEEE.","DOI":"10.1109\/CSFW.1991.151575"},{"key":"5_CR9","doi-asserted-by":"crossref","unstructured":"L. Gong, R. Needham, and R. Yahalom. Reasoning about belief in cryptographic protocols. In Proceedings of the Symposium on Security and Privacy, pages 234\u2013248, Oakland, CA, May 1990. IEEE.","DOI":"10.1109\/RISP.1990.63854"},{"key":"5_CR10","unstructured":"E. Gunter. Library mutrec. HOL90.7, contrib directory, 1994."},{"issue":"1","key":"5_CR11","first-page":"370","volume":"17","author":"A. Mathuria","year":"1995","unstructured":"A. Mathuria, R. Safavi-Naini, and P. Nickolas. On the automation of GNY logic. Australian Computer Science Communications, 17(1):370\u2013379, 1995.","journal-title":"Australian Computer Science Communications"},{"key":"5_CR12","doi-asserted-by":"crossref","unstructured":"C. Meadows. Using narrowing in the analysis of key management protocols. In Proceedings of the Symposium on Security and Privacy, pages 138\u2013147, Oakland, CA, May 1989. IEEE.","DOI":"10.1109\/SECPRI.1989.36288"},{"key":"5_CR13","doi-asserted-by":"crossref","unstructured":"C. Meadows. A system for the specification and analysis of key management protocols. In Proceedings of the Symposium on Security and Privacy, pages 182\u2013195, Oakland, CA, May 1991. IEEE.","DOI":"10.1109\/RISP.1991.130786"},{"issue":"1","key":"5_CR14","doi-asserted-by":"crossref","first-page":"5","DOI":"10.3233\/JCS-1992-1102","volume":"1","author":"C. Meadows","year":"1992","unstructured":"C. Meadows. Applying formal methods to the analysis of a key management protocol. J. Computer Security, 1(1):5\u201336, 1992.","journal-title":"J. Computer Security"},{"key":"5_CR15","doi-asserted-by":"crossref","unstructured":"J. Millen. The interrogator: A tool for cryptographic protocol analysis. In Proceedings of the Symposium on Security and Privacy, pages 134\u2013141, Oakland, CA, May 1984. IEEE.","DOI":"10.1109\/SP.1984.10003"},{"key":"5_CR16","doi-asserted-by":"crossref","unstructured":"J. Millen. The Interrogator model. In Proceedings of the Symposium on Security and Privacy, pages 251\u2013260, Oakland, CA, May 1995. IEEE.","DOI":"10.1109\/SECPRI.1995.398937"},{"issue":"2","key":"5_CR17","doi-asserted-by":"crossref","first-page":"274","DOI":"10.1109\/TSE.1987.233151","volume":"SE-13","author":"J. Millen","year":"1987","unstructured":"J. Millen, S. Clark, and S. Freedman. The Interrogator: Protocol security analysis. IEEE Trans. on Software Engineering, SE-13(2):274\u2013288, February 1987.","journal-title":"IEEE Trans. on Software Engineering"},{"key":"5_CR18","volume-title":"Applied Cryptography: Protocols, Algorithms, and Source Code in C","author":"B. Schneier","year":"1995","unstructured":"B. Schneier. Applied Cryptography: Protocols, Algorithms, and Source Code in C. John Wiley & Sons, New York, NY, 1995."},{"key":"5_CR19","volume-title":"Formal Specification and Analysis of Cryptographic Protocols","author":"E. Snekkenes","year":"1995","unstructured":"E. Snekkenes. Formal Specification and Analysis of Cryptographic Protocols. PhD thesis, University of Oslo, Norway, January 1995."},{"key":"5_CR20","unstructured":"J. Steiner, C. Neuman, and J. Schiller. An authentication service for open network systems. In Proceedings of the USENIX Winter Conference, pages 191\u2013202, February 1988."},{"key":"5_CR21","doi-asserted-by":"crossref","unstructured":"P. Syverson and P. van Oorschot. On unifying some cryptographic protocol logics. In Proceedings of the Symposium on Security and Privacy, pages 14\u201328, Oakland, CA, 1994. IEEE.","DOI":"10.21236\/ADA465512"},{"key":"5_CR22","doi-asserted-by":"crossref","unstructured":"J. Tardo and K. Alagappan. SPX: Global authentication using public key certificates. In Proceedings of the Symposium on Security and Privacy, pages 232\u2013244, Oakland, CA, 1991. IEEE.","DOI":"10.1109\/RISP.1991.130791"}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0105397","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,12,15]],"date-time":"2021-12-15T22:52:29Z","timestamp":1639608749000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0105397"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540615873","9783540706410"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/bfb0105397","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}