{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T23:45:29Z","timestamp":1742946329591,"version":"3.40.3"},"publisher-location":"Boston, MA","reference-count":13,"publisher":"Springer US","isbn-type":[{"type":"print","value":"9781441959058"},{"type":"electronic","value":"9781441959065"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-1-4419-5906-5_859","type":"book-chapter","created":{"date-parts":[[2011,10,27]],"date-time":"2011-10-27T13:53:10Z","timestamp":1319723590000},"page":"495-498","source":"Crossref","is-referenced-by-count":0,"title":["Formal Methods for the Orange Book"],"prefix":"10.1007","author":[{"given":"Jonathan K.","family":"Millen","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"859_CR1_859","doi-asserted-by":"crossref","DOI":"10.21236\/AD0772806","volume-title":"Computer security technology planning study","author":"JP Anderson","year":"1972","unstructured":"Anderson JP (1972) Computer security technology planning study. ESDTR-73-51, Air Force Electronic Systems Division, Hanscom AFB, Bedford, MA"},{"key":"859_CR2_859","volume-title":"Secure computer system: unified exposition and multics interpretation","author":"DE Bell","year":"1975","unstructured":"Bell DE, La Padula LJ (1975) Secure computer system: unified exposition and multics interpretation. ESDTR-75-306. The Mitre Corporation, Bedford, MA"},{"issue":"4","key":"859_CR3_859","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1145\/1012497.1012505","volume":"10","author":"DM Berry","year":"1985","unstructured":"Berry DM (1985) An Ina Jo proof manager for the formal development method. ACM SIGSOFT Software Eng Notes 10(4): 19\u201325","journal-title":"ACM SIGSOFT Software Eng Notes"},{"key":"859_CR4_859","volume-title":"Department of Defense Trusted Computer System. Evaluation Criteria","author":"Department of Defense","year":"1985","unstructured":"Department of Defense (1985) Department of Defense Trusted Computer System. Evaluation Criteria. DOD 5200.28-STD, National Computer Security Center, Fort Meade, MD"},{"key":"859_CR5_859","unstructured":"Good DI, Akers RL, Smith LM (1988) Report on Gypsy 2.05, Computational Logic, Inc., Austin, TX"},{"key":"859_CR6_859","volume-title":"Proceedings of the 10th National Computer Security Conference","author":"M Kaufmann","year":"1987","unstructured":"Kaufmann M, Young WD (1987) Comparing gypsy and the Boyer-Moore logic for specifying secure systems. In: Proceedings of the 10th National Computer Security Conference, Baltimore MD"},{"issue":"3","key":"859_CR7_859","doi-asserted-by":"crossref","first-page":"256","DOI":"10.1145\/357369.357374","volume":"1","author":"RA Kemmerer","year":"1983","unstructured":"Kemmerer RA (1983) Shared resource matrix methodology: an approach to identifying storage and timing channels. ACM Trans Comput Syst 1(3):256\u2013277","journal-title":"ACM Trans Comput Syst"},{"key":"859_CR8_859","volume-title":"Trusted network interpretation of the trusted computer system evaluation criteria","author":"National Computer Security Center","year":"1987","unstructured":"National Computer Security Center (1987) Trusted network interpretation of the trusted computer system evaluation criteria. NCSC-TG-005"},{"key":"859_CR9_859","volume-title":"A guide to understanding security modeling in trusted systems","author":"National Computer Security Center","year":"1992","unstructured":"National Computer Security Center (1992) A guide to understanding security modeling in trusted systems. NCSC-TG-010"},{"key":"859_CR10_859","unstructured":"National Computer Security Center, Guidelines for formal verification systems. NCSC-TG-014-89"},{"key":"859_CR11_859","volume-title":"A guide to understanding covert channel analysis of trusted systems","author":"National Computer Security Center","year":"1993","unstructured":"National Computer Security Center (1993) A guide to understanding covert channel analysis of trusted systems. NCSC-TG-030"},{"key":"859_CR12_859","volume-title":"An introduction to formal specification and verification using EHDM. SRI International","author":"S Owre","year":"1991","unstructured":"Owre S, Rushby J, von Henke F (1991) An introduction to formal specification and verification using EHDM. SRI International. SRI-CSL-91-2"},{"issue":"5","key":"859_CR13_859","doi-asserted-by":"crossref","first-page":"330","DOI":"10.1145\/355602.361309","volume":"15","author":"DL Parnas","year":"1972","unstructured":"Parnas DL (1972) A technique for software module specification with examples. Comm ACM 15(5):330\u2013336","journal-title":"Comm ACM"}],"container-title":["Encyclopedia of Cryptography and Security"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-1-4419-5906-5_859","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,6,2]],"date-time":"2020-06-02T00:39:02Z","timestamp":1591058342000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-1-4419-5906-5_859"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9781441959058","9781441959065"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/978-1-4419-5906-5_859","relation":{},"subject":[],"published":{"date-parts":[[2011]]}}}