{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:06:42Z","timestamp":1725664002264},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540584506"},{"type":"electronic","value":"9783540488033"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/3-540-58450-1_35","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T16:11:54Z","timestamp":1330272714000},"page":"65-80","source":"Crossref","is-referenced-by-count":1,"title":["Providing tractable security analyses in HOL"],"prefix":"10.1007","author":[{"given":"Stephen H.","family":"Brackin","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,8]]},"reference":[{"key":"5_CR1","volume-title":"Technical Report CSE-90-45","author":"J. Alves-Foss","year":"1990","unstructured":"J. Alves-Foss and K. Levitt. A Model of Event Systems in Higher Order Logic: Sequence and Event System Theories. Technical Report CSE-90-45, Division of Computer Science, University of California, Davis, November 1990."},{"key":"5_CR2","volume-title":"Technical Report CSE-90-46","author":"J. Alves-Foss","year":"1990","unstructured":"J. Alves-Foss and K. Levitt. A Security Property in Higher Order Logic: Restrictiveness and Hook-Up Theories. Technical Report CSE-90-46, Division of Computer Science, University of California, Davis, December 1990."},{"key":"5_CR3","doi-asserted-by":"crossref","unstructured":"J. Alves-Foss and K. Levitt. Mechanical Verification of Secure Distributed Systems in Higher Order Logic. In Proceedings of the 1991 International Meeting on Higher Order Logic Theorem Proving and its Applications, pages 263\u2013278, 1991.","DOI":"10.1109\/HOL.1991.596293"},{"key":"5_CR4","first-page":"122","volume-title":"Verification of Secure Distributed Systems in Higher Order Logic: A Modular Approach Using Generic Components","author":"J. Alves-Foss","year":"1991","unstructured":"J. Alves-Foss and K. Levitt. Verification of Secure Distributed Systems in Higher Order Logic: A Modular Approach Using Generic Components. In Proceedings of the Symposium on Security and Privacy, pages 122\u2013135, Oakland, CA, 1991. IEEE."},{"key":"5_CR5","volume-title":"HOL User's Group Workshop","author":"S. Brackin","year":"1993","unstructured":"S. Brackin and S-K Chin. Server-process restrictiveness in HOL. In HOL User's Group Workshop, Vancouver, Canada, August 1993. Springer Verlag."},{"key":"5_CR6","unstructured":"Department of Defense. Trusted Computer System Evaluation Criteria, December 1985. DoD-5200.28-STD."},{"key":"5_CR7","first-page":"11","volume-title":"Proceedings of the Symposium on Security and Privacy","author":"J. A. Goguen","year":"1982","unstructured":"Joseph A. Goguen and Jos\u00e9 Meseguer. Security policy and security models. In Proceedings of the Symposium on Security and Privacy, pages 11\u201320, Oakland, CA, April 1982. IEEE."},{"key":"5_CR8","series-title":"Series in Computer Science","volume-title":"Communicating Sequential Processes","author":"C. A. R. Hoare","year":"1985","unstructured":"C. A. R. Hoare. Communicating Sequential Processes. Series in Computer Science. Prentice-Hall International, Englewood Cliffs, NJ, 1985."},{"key":"5_CR9","first-page":"161","volume-title":"Specifications for multilevel security and a hook-up property","author":"D. McCullough","year":"1987","unstructured":"D. McCullough. Specifications for multilevel security and a hook-up property. In Proceedings of the Symposium on Security and Privacy, pages 161\u2013166, Oakland, CA, April 1987. IEEE."},{"key":"5_CR10","doi-asserted-by":"crossref","unstructured":"D. McCullough. Foundations of Ulysses: The theory of security. Technical Report RADC-TR-87-222, Rome Air Development Center, May 1988.","DOI":"10.21236\/ADA200110"},{"key":"5_CR11","first-page":"177","volume-title":"Noninterference and the composability of security properties","author":"D. McCullough","year":"1988","unstructured":"D. McCullough. Noninterference and the composability of security properties. In Proceedings of the Symposium on Security and Privacy, pages 177\u2013186, Oakland, CA, April 1988. IEEE."},{"key":"5_CR12","volume-title":"Communication and Concurrency","author":"R. Milner","year":"1990","unstructured":"R. Milner. Communication and Concurrency. Prentice-Hall, NY, 1990."},{"key":"5_CR13","volume-title":"Technical Report TM-94-0016","author":"ORA","year":"1994","unstructured":"ORA. Romulus Theories. Technical Report TM-94-0016, Odyssey Research Associates, Ithaca, NY, March 1994."},{"key":"5_CR14","volume-title":"Technical Report TM-94-0017","author":"ORA","year":"1994","unstructured":"ORA. Romulus Library of Models. Technical Report TM-94-0017, Odyssey Research Associates, Ithaca, NY, March 1994."},{"key":"5_CR15","volume-title":"Technical Report TM-94-0018","author":"ORA","year":"1994","unstructured":"ORA. Romulus User's Manual. Technical Report TM-94-0018, Odyssey Research Associates, Ithaca, NY, March 1994."},{"key":"5_CR16","volume-title":"Technical Report TM-94-0019","author":"ORA","year":"1994","unstructured":"ORA. Romulus Overview. Technical Report TM-94-0019, Odyssey Research Associates, Ithaca, NY, March 1994."},{"key":"5_CR17","first-page":"90","volume-title":"An approach to increasing the automation of the verification of security","author":"D. Rosenthal","year":"1988","unstructured":"D. Rosenthal. An approach to increasing the automation of the verification of security. In Proceedings of Computer Security Foundations Workshop, pages 90\u201397, Franconia, NH, June 1988. The MITRE Corporation, M88-37."},{"key":"5_CR18","first-page":"133","volume-title":"Implementing a verification methodology for McCullough security","author":"D. Rosenthal","year":"1989","unstructured":"D. Rosenthal. Implementing a verification methodology for McCullough security. In Proceedings of Computer Security Foundations Workshop II, pages 133\u2013140, Franconia, NH, June 1989. IEEE Computer Society Press."}],"container-title":["Lecture Notes in Computer Science","Higher Order Logic Theorem Proving and Its Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-58450-1_35.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:21:25Z","timestamp":1605648085000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-58450-1_35"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540584506","9783540488033"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/3-540-58450-1_35","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1994]]}}}