{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:03:36Z","timestamp":1725663816390},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540578260"},{"type":"electronic","value":"9783540483465"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/3-540-57826-9_155","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T13:26:50Z","timestamp":1330262810000},"page":"450-463","source":"Crossref","is-referenced-by-count":3,"title":["Server-process restrictiveness in HOL"],"prefix":"10.1007","author":[{"given":"Stephen H.","family":"Brackin","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shiu-Kai","family":"Chin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,5,31]]},"reference":[{"key":"35_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":"35_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":"35_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":"35_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":"35_CR5","unstructured":"S. H. Brackin and S-K Chin. Technical Report (in progress)."},{"key":"35_CR6","unstructured":"J. Camilleri and T. Melham. Reasoning with Inductively Defined Relations in the HOL Theorem Prover. Technical Report 265, University of Cambridge Computer Laboratory, August 1992."},{"key":"35_CR7","unstructured":"Department of Defense. Trusted Computer System Evaluation Criteria, December 1985. DoD-5200.28-STD."},{"key":"35_CR8","unstructured":"M. J. C. Gordon. The HOL System Description. Cambridge Research Centre, SRI International."},{"key":"35_CR9","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":"35_CR10","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":"35_CR11","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":"35_CR12","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."},{"issue":"6","key":"35_CR13","doi-asserted-by":"crossref","first-page":"563","DOI":"10.1109\/32.55085","volume":"16","author":"D. McCullough","year":"1990","unstructured":"D. McCullough. A hookup theorem for multilevel security. IEEE Transactions on Software Engineering, 16(6):563\u2013568, June 1990.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"35_CR14","doi-asserted-by":"crossref","unstructured":"T. F. Melham. Automating Recursive Type Definitions in Higher Order Logic. Technical Report 146, University of Cambridge Computer Laboratory, January 1989.","DOI":"10.1007\/978-1-4612-3658-0_9"},{"key":"35_CR15","volume-title":"Communication and Concurrency","author":"R. Milner","year":"1990","unstructured":"R. Milner. Communication and Concurrency. Prentice-Hall, New York, 1990."},{"key":"35_CR16","unstructured":"ORA. Romulus: A computer security properties modeling environment, final report \u2014 volume 1: Overview. Technical report, ORA, June 1990."},{"key":"35_CR17","unstructured":"ORA. Romulus, Release 2.0. Odyssey Research Associates, December 1992."},{"key":"35_CR18","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":"35_CR19","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."},{"key":"35_CR20","first-page":"91","volume-title":"Security models for priority buffering and interrupt handling","author":"D. Rosenthal","year":"1990","unstructured":"D. Rosenthal. Security models for priority buffering and interrupt handling. In Proceedings of Computer Security Foundations Workshop III, pages 91\u201397, Franconia NH, June 1990. IEEE Computer Society Press."},{"key":"35_CR21","first-page":"27","volume-title":"Modeling Restrictive Processes That Involve Blocking Requests","author":"D. Rosenthal","year":"1993","unstructured":"D. Rosenthal. Modeling Restrictive Processes That Involve Blocking Requests. In Proceedings of Computer Security Foundations Workshop VI, pages 27\u201338, Franconia NH, June 1993. 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-57826-9_155.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:14:32Z","timestamp":1605647672000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-57826-9_155"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540578260","9783540483465"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/3-540-57826-9_155","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1994]]}}}