{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,6]],"date-time":"2025-01-06T05:12:31Z","timestamp":1736140351533,"version":"3.32.0"},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540646082"},{"type":"electronic","value":"9783540693390"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0028731","type":"book-chapter","created":{"date-parts":[[2005,12,1]],"date-time":"2005-12-01T06:48:09Z","timestamp":1133419689000},"page":"49-56","source":"Crossref","is-referenced-by-count":1,"title":["A formal method experience at secure computing corporation"],"prefix":"10.1007","author":[{"given":"John","family":"Hoffman","sequence":"first","affiliation":[]},{"given":"Charlie","family":"Payne","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,18]]},"reference":[{"key":"6_CR1","unstructured":"Martin Abadi and Lesli Lamport. Conjoining specifications. Technical Report 118, Digital Equipment Corporation, Systems Research Center, December 1993."},{"key":"6_CR2","unstructured":"W.E. Boebert and R.Y. Kain. \u201cA Practical Alternative to Hierarchical Integrity Policies\u201d. In Proceedings of the 8th National Computer Security Conference, pages 18\u201327, October 1985."},{"key":"6_CR3","unstructured":"National Computer Security Center. Department of Defense Trusted Computer System Evaluation Criteria. Technical report, US National Computer Security Center, NCSC, Fort Meade, Maryland, 1985."},{"key":"6_CR4","doi-asserted-by":"crossref","unstructured":"Michael Carney and Brian Loe. A comparison of methods for implementing adaptive security poli cies. In Seventh USENIX Security Symposium Proceedings, pages 1\u201314, San Antonio, TX, January 1998. USENIX Association.","DOI":"10.21236\/ADA345381"},{"key":"6_CR5","unstructured":"Secure Computing Corporation. DTOS Composability Study. Technical report, 1997. http:\/\/www.securecomputing.com\/randt\/HTML\/technical-docs.html."},{"key":"6_CR6","doi-asserted-by":"crossref","unstructured":"Todd Fine, Thomas Haigh, Richard O'Brien, and Dana Toups. Noninterference and Unwinding for LOCK. In Proceedings of Computer Security Foundations Workshop II, pages 22\u201328, Franconia, NH, Jun 1989. IEEE.","DOI":"10.1109\/CSFW.1989.40583"},{"key":"6_CR7","doi-asserted-by":"crossref","unstructured":"Todd Fine. Constructively Using Noninterference to Analyze Systems. In IEEE Symposium on Security and Privacy, pages 162\u2013169, Oakland, CA, May 1990.","DOI":"10.1109\/RISP.1990.63847"},{"key":"6_CR8","doi-asserted-by":"crossref","unstructured":"Todd Fine. A framework for composition. In Proceedings of the Eleventh Annual Conference on Computer Assurance, pages 199\u2013212, June 1996.","DOI":"10.1109\/CMPASS.1996.507888"},{"key":"6_CR9","doi-asserted-by":"crossref","unstructured":"Todd Fine and Spencer E. Minear. Assuring Distributed Trusted Mach. In Proceedings IEEE Computer Society Symposium on Research in Security and Privacy, pages 206\u2013218, May 1993.","DOI":"10.1109\/RISP.1993.287631"},{"key":"6_CR10","doi-asserted-by":"crossref","unstructured":"John Hoffman. Implementing RBAC on a Type Enforced System. In Proceedings of the Thirteenth Annual Computer Security Applications Conference, pages 158\u2013163, 1997.","DOI":"10.1109\/CSAC.1997.646185"},{"key":"6_CR11","doi-asserted-by":"crossref","unstructured":"John McLean. A general theory of composition for trace sets closed under selective interleaving functions. In Proceedings of the IEEE Symposium on Security and Privacy, Oakland, CA, May 1994.","DOI":"10.1109\/RISP.1994.296590"},{"key":"6_CR12","unstructured":"Spencer E. Minear. Providing policy control over object operations in a mach based system. In Fifth USENIX Security Symposium Proceedings, pages 141\u2013156, Salt Lake City, UT, June 1995. USENIX Association."},{"key":"6_CR13","unstructured":"Owre, Shankar and Rushby. The PVS Specification Language (Beta Release). User Manual, SRI International Computer Science Laboratory, 333 Ravenswood Avenue, Menlo Park, CA 94025-3493, June 1993. http: \/\/www.csl.sri.com\/reports\/pvs-language.dvi, ps. Z."},{"key":"6_CR14","unstructured":"Owre, Shankar, Rushby, Crow and Srivas. A Tutorial Introduction to PVS. User Manual, SRI International Computer Science Laboratory, 333 Ravenswood Avenue, Menlo Park, CA 94025-3493, June 1995. http:\/\/www.cl.sri.com\/sri-csl-fm.html."},{"key":"6_CR15","unstructured":"John Rushby. Noninterference, Transitivity, and Channel-Control Security Policies. Technical Report CSL-92-02, SRI International Computer Science Laboratory, 333 Ravenswood Avenue, Menlo Park, CA 94025-3493, December 1992. http:\/\/www.csl.sri.com\/csl-92-2.html."},{"key":"6_CR16","doi-asserted-by":"crossref","unstructured":"Sami Saydjari. LOCK Trek: Navigating Uncharted Space. In Proceedings of the IEEE Symposium on Security and Privacy, Oakland, CA, 1989.","DOI":"10.1109\/SECPRI.1989.36291"},{"issue":"2","key":"6_CR17","doi-asserted-by":"crossref","first-page":"38","DOI":"10.1109\/2.485845","volume":"29","author":"R. Sandhu","year":"1996","unstructured":"Ravi Sandhu, Edward Coyne, Hal Feinstein, and Charles Youman. Role-based access control models. IEEE Computer, 29(2):38\u201347, February 1996.","journal-title":"IEEE Computer"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0028731","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,6]],"date-time":"2025-01-06T01:45:19Z","timestamp":1736127919000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0028731"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540646082","9783540693390"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/bfb0028731","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1998]]}}}