{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:43:33Z","timestamp":1750308213460,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":31,"publisher":"ACM","license":[{"start":{"date-parts":[[2004,10,29]],"date-time":"2004-10-29T00:00:00Z","timestamp":1099008000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2004,10,29]]},"DOI":"10.1145\/1029133.1029145","type":"proceedings-article","created":{"date-parts":[[2005,1,30]],"date-time":"2005-01-30T17:58:48Z","timestamp":1107107928000},"page":"86-95","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Lessons learned using alloy to formally specify MLS-PCA trusted security architecture"],"prefix":"10.1145","author":[{"given":"Brant","family":"Hashii","sequence":"first","affiliation":[{"name":"Northrop Grumman Corporation"}]}],"member":"320","published-online":{"date-parts":[[2004,10,29]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"Common Criteria for Information Technology Security Evaluation Version 2.1 August 1999. Available at http:\/\/www.radium.ncsc.mil\/tpep\/library\/ccitse\/ccitse.html.  Common Criteria for Information Technology Security Evaluation Version 2.1 August 1999. Available at http:\/\/www.radium.ncsc.mil\/tpep\/library\/ccitse\/ccitse.html."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.5555\/876878.879305"},{"key":"e_1_3_2_1_4_1","volume-title":"Fundamentals of grid computing","author":"Berstis Viktors","year":"2002","unstructured":"Viktors Berstis . Fundamentals of grid computing , 2002 . Available at http:\/\/publib-b.boulder.ibm.com\/Redbooks.nsf\/RedbookAbstracts\/redp3613.html?Open. Viktors Berstis. Fundamentals of grid computing, 2002. Available at http:\/\/publib-b.boulder.ibm.com\/Redbooks.nsf\/RedbookAbstracts\/redp3613.html?Open."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/TIT.1976.1055638"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00124891"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.1982.10014"},{"key":"e_1_3_2_1_8_1","volume-title":"Fourth International Workshop on the ACL2 Prover and Its Applications (ACL2-2003)","author":"Greve David","year":"2003","unstructured":"David Greve , Matthew Wilding , and W. Mark Vanfleet . A separation kernel formal security policy . In Fourth International Workshop on the ACL2 Prover and Its Applications (ACL2-2003) , Boulder, CO , July 2003 . Available at http:\/\/hokiepokie.org\/docs\/. David Greve, Matthew Wilding, and W. Mark Vanfleet. A separation kernel formal security policy. In Fourth International Workshop on the ACL2 Prover and Its Applications (ACL2-2003), Boulder, CO, July 2003. Available at http:\/\/hokiepokie.org\/docs\/."},{"key":"e_1_3_2_1_9_1","volume-title":"MIT Lab for Computer Science","author":"Jackson Daniel","year":"2001","unstructured":"Daniel Jackson . Micromodels of Software: Modelling & Analysis with Alloy . MIT Lab for Computer Science , November 2001 . Available at http:\/\/sdg.lcs.mit.edu\/alloy\/book.pdf. Daniel Jackson. Micromodels of Software: Modelling & Analysis with Alloy. MIT Lab for Computer Science, November 2001. Available at http:\/\/sdg.lcs.mit.edu\/alloy\/book.pdf."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/503209.503219"},{"key":"e_1_3_2_1_11_1","first-page":"21","volume-title":"IEEE Computer","author":"Jackson Daniel","year":"1996","unstructured":"Daniel Jackson and Jeannette M. Wing . Lightweight formal methods . IEEE Computer , pages 21 -- 22 , April 1996 . Daniel Jackson and Jeannette M. Wing. Lightweight formal methods. IEEE Computer, pages 21--22, April 1996."},{"key":"e_1_3_2_1_12_1","volume-title":"The CoABS Grid","author":"Martha","year":"2002","unstructured":"Martha L. Kahn and Cynthia Della Torre Cicalese . The CoABS Grid , January 2002 . Presented at Goddard \/ JPL Workshop on Radical Agent Concepts, Tysons Corner, CA. Available at http:\/\/coabs.globalinfotek.com\/public\/downloads\/Grid\/documents\/010904Ka%hnCicaleseNASA.pdf. Martha L. Kahn and Cynthia Della Torre Cicalese. The CoABS Grid, January 2002. Presented at Goddard \/ JPL Workshop on Radical Agent Concepts, Tysons Corner, CA. Available at http:\/\/coabs.globalinfotek.com\/public\/downloads\/Grid\/documents\/010904Ka%hnCicaleseNASA.pdf."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/SECPRI.1989.36276"},{"key":"e_1_3_2_1_14_1","unstructured":"Lockheed Sanders Inc. Hughes Aircraft Motorola and ISX Corporation. RASSP architecture guide rev. b January 1995. Available at http:\/\/www.eda.org\/rassp\/documents\/sanders\/arch_guide_b.pdf.  Lockheed Sanders Inc. Hughes Aircraft Motorola and ISX Corporation. RASSP architecture guide rev. b January 1995. Available at http:\/\/www.eda.org\/rassp\/documents\/sanders\/arch_guide_b.pdf."},{"key":"e_1_3_2_1_15_1","volume-title":"Gemini Computers, Incorporated, Gemini Trusted Network Processor, version 1.01","author":"National Computer Security Center.","year":"1995","unstructured":"National Computer Security Center. Final evaluation report , Gemini Computers, Incorporated, Gemini Trusted Network Processor, version 1.01 , June 1995 . Available at http:\/\/www.geminisecure.com\/resource.htm. National Computer Security Center. Final evaluation report, Gemini Computers, Incorporated, Gemini Trusted Network Processor, version 1.01, June 1995. Available at http:\/\/www.geminisecure.com\/resource.htm."},{"key":"e_1_3_2_1_16_1","volume-title":"January","author":"National Institute of Standards and Technology.","year":"2003","unstructured":"National Institute of Standards and Technology. Special publication 800-57 recommendation for key management part 1: General guideline , January 2003 . Draft , Available at http:\/\/csrc.nist.gov\/CryptoToolkit\/tkkeymgmt.html. National Institute of Standards and Technology. Special publication 800-57 recommendation for key management part 1: General guideline, January 2003. Draft, Available at http:\/\/csrc.nist.gov\/CryptoToolkit\/tkkeymgmt.html."},{"key":"e_1_3_2_1_17_1","volume-title":"EPL entry CSC-EPL -94\/008","author":"National Security Agency.","year":"1994","unstructured":"National Security Agency. GTNP version 1.01, network component M only , EPL entry CSC-EPL -94\/008 , September 1994 . Available at http:\/\/www.radium.ncsc.mil\/tpep\/epl\/entries\/CSC-EPL-94-008.html. National Security Agency. GTNP version 1.01, network component M only, EPL entry CSC-EPL -94\/008, September 1994. Available at http:\/\/www.radium.ncsc.mil\/tpep\/epl\/entries\/CSC-EPL-94-008.html."},{"key":"e_1_3_2_1_18_1","volume-title":"EPL entry CSC-EPL -94\/006","author":"National Security Agency.","year":"1994","unstructured":"National Security Agency. MLS LAN version 2.1, network component MDIA , EPL entry CSC-EPL -94\/006 , September 1994 . Available at http:\/\/www.radium.ncsc.mil\/tpep\/epl\/entries\/CSC-EPL-94-006.html. National Security Agency. MLS LAN version 2.1, network component MDIA, EPL entry CSC-EPL -94\/006, September 1994. Available at http:\/\/www.radium.ncsc.mil\/tpep\/epl\/entries\/CSC-EPL-94-006.html."},{"key":"e_1_3_2_1_19_1","volume-title":"Software considerations in airborne systems and equipment certification","author":"RTCA.","year":"1992","unstructured":"s RTCA. RTCA\/DO-178B : Software considerations in airborne systems and equipment certification , 1992 . Committee SC-167\/Eurocae WG- 12. sRTCA. RTCA\/DO-178B: Software considerations in airborne systems and equipment certification, 1992. Committee SC-167\/Eurocae WG-12."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1067627.806586"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/MC.1983.1654443"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/2.241422"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.5555\/646648.759411"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/383775.383778"},{"issue":"09","key":"e_1_3_2_1_27_1","article-title":"on the line","volume":"85","author":"Tirpak John A.","year":"2002","unstructured":"John A. Tirpak . The F-22 on the line . Air Force Magazine , 85 ( 09 ), 2002 . Available at http:\/\/www.afa.org\/magazine\/Sept2002\/0902raptor.html. John A. Tirpak. The F-22 on the line. Air Force Magazine, 85(09), 2002. Available at http:\/\/www.afa.org\/magazine\/Sept2002\/0902raptor.html.","journal-title":"Air Force Magazine"},{"key":"e_1_3_2_1_28_1","volume-title":"February","author":"Platform Alliance Trusted Computing","year":"2002","unstructured":"Trusted Computing Platform Alliance . Trusted Computing Platform Alliance (TCPA) Main Specification Version 1.1b , February 2002 . Available at http:\/\/www.trustedcomputing.org\/tcpaasp4\/index.asp. Trusted Computing Platform Alliance. Trusted Computing Platform Alliance (TCPA) Main Specification Version 1.1b, February 2002. Available at http:\/\/www.trustedcomputing.org\/tcpaasp4\/index.asp."},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.5555\/938383.938400"},{"key":"e_1_3_2_1_30_1","volume-title":"Joint vision","author":"United States Joint Chiefs of Staff.","year":"2020","unstructured":"United States Joint Chiefs of Staff. Joint vision 2020 , May 2000. Available at http:\/\/www.dtic.mil\/jointvision\/jvpub2.htm. United States Joint Chiefs of Staff. Joint vision 2020, May 2000. Available at http:\/\/www.dtic.mil\/jointvision\/jvpub2.htm."},{"key":"e_1_3_2_1_31_1","volume-title":"December","author":"U.S. Department of Defense.","year":"1985","unstructured":"U.S. Department of Defense. DoD trusted computer system evaluation criteria , December 1985 . Available at http:\/\/www.radium.ncsc.mil\/tpep\/library\/rainbow\/index.html. U.S. Department of Defense. DoD trusted computer system evaluation criteria, December 1985. Available at http:\/\/www.radium.ncsc.mil\/tpep\/library\/rainbow\/index.html."},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.5555\/555298.789912"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.5555\/882488.884163"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.5555\/956415.956456"}],"event":{"name":"CCS04: 11th ACM Conference on Computer and Communications Security 2004","sponsor":["SIGSAC ACM Special Interest Group on Security, Audit, and Control","ACM Association for Computing Machinery"],"location":"Washington DC USA","acronym":"CCS04"},"container-title":["Proceedings of the 2004 ACM workshop on Formal methods in security engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1029133.1029145","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1029133.1029145","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T16:31:07Z","timestamp":1750264267000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1029133.1029145"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004,10,29]]},"references-count":31,"alternative-id":["10.1145\/1029133.1029145","10.1145\/1029133"],"URL":"https:\/\/doi.org\/10.1145\/1029133.1029145","relation":{},"subject":[],"published":{"date-parts":[[2004,10,29]]},"assertion":[{"value":"2004-10-29","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}