{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,2]],"date-time":"2026-01-02T05:48:23Z","timestamp":1767332903940,"version":"3.48.0"},"reference-count":21,"publisher":"IEEE","license":[{"start":{"date-parts":[[2025,10,6]],"date-time":"2025-10-06T00:00:00Z","timestamp":1759708800000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2025,10,6]],"date-time":"2025-10-06T00:00:00Z","timestamp":1759708800000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025,10,6]]},"DOI":"10.1109\/milcom64451.2025.11310477","type":"proceedings-article","created":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T18:35:33Z","timestamp":1767292533000},"page":"1037-1043","source":"Crossref","is-referenced-by-count":0,"title":["Leveraging Formal Methods to Strengthen Cyber-Resilience in Authorization to Operate"],"prefix":"10.1109","author":[{"given":"Alice","family":"Lee","sequence":"first","affiliation":[{"name":"Secure Resilient Systems & Technology,MIT Lincoln Laboratory,Lexington,MA"}]},{"given":"Jack","family":"Cheng","sequence":"additional","affiliation":[{"name":"Secure Resilient Systems & Technology,MIT Lincoln Laboratory,Lexington,MA"}]},{"given":"Tim","family":"Braje","sequence":"additional","affiliation":[{"name":"Secure Resilient Systems & Technology,MIT Lincoln Laboratory,Lexington,MA"}]},{"given":"Noah","family":"Luther","sequence":"additional","affiliation":[{"name":"Secure Resilient Systems & Technology,MIT Lincoln Laboratory,Lexington,MA"}]},{"given":"Ian","family":"McQuoid","sequence":"additional","affiliation":[{"name":"Secure Resilient Systems & Technology,MIT Lincoln Laboratory,Lexington,MA"}]},{"given":"Gruia-Catalin","family":"Roman","sequence":"additional","affiliation":[{"name":"University of New Mexico,Department of Computer Science,Albuquerque,NM"}]},{"given":"Joseph Dan","family":"Trujillo","sequence":"additional","affiliation":[{"name":"Space Vehicles Directorate,Air Force Research Laboratory,Albuquerque,NM"}]},{"given":"Richard","family":"Skowyra","sequence":"additional","affiliation":[{"name":"Secure Resilient Systems & Technology,MIT Lincoln Laboratory,Lexington,MA"}]},{"given":"Samuel","family":"Mergendahl","sequence":"additional","affiliation":[{"name":"Secure Resilient Systems & Technology,MIT Lincoln Laboratory,Lexington,MA"}]}],"member":"263","reference":[{"year":"2020","key":"ref1","article-title":"Security and privacy controls for information systems and organizations"},{"key":"ref2","article-title":"Holding the high ground: Defending satellites from cyber attack","author":"Skowyra","year":"2023","journal-title":"AFCEA Signal Magazine"},{"volume-title":"DoD Instruction 8510.01, Office of the DoD Chief Information Officer","year":"2022","key":"ref3"},{"volume-title":"FAR 15.203 Requests for proposals, Federal Acquisition Regulation","year":"2025","key":"ref4"},{"volume-title":"digital.gov","key":"ref5","article-title":"An introduction to ATOs"},{"key":"ref6","article-title":"core flight system (cfs)"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1145\/2560537"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3134043"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1145\/2517349.2522720"},{"key":"ref11","first-page":"183","article-title":"Specifying concurrent systems with tla+","author":"Lamport","year":"1999","journal-title":"Calculational System Design"},{"volume-title":"Software Abstractions: logic, language, and analysis","year":"2012","author":"Jackson","key":"ref12"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1109\/32.588521"},{"article-title":"The case for memory safe roadmaps","volume-title":"Tech. Rep","year":"2023","key":"ref14"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-06773-0_5"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-17244-1_6"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1145\/3586037"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/9153.001.0001"},{"article-title":"Systems modeling language","volume-title":"OMG","year":"2006","key":"ref19"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.14722\/spacesec.2024.23057"},{"key":"ref21","article-title":"About cmmc"}],"event":{"name":"MILCOM 2025 - 2025 IEEE Military Communications Conference (MILCOM)","start":{"date-parts":[[2025,10,6]]},"location":"Los Angeles, CA, USA","end":{"date-parts":[[2025,10,10]]}},"container-title":["MILCOM 2025 - 2025 IEEE Military Communications Conference (MILCOM)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx8\/11309822\/11309347\/11310477.pdf?arnumber=11310477","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,1,2]],"date-time":"2026-01-02T05:47:03Z","timestamp":1767332823000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/11310477\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,6]]},"references-count":21,"URL":"https:\/\/doi.org\/10.1109\/milcom64451.2025.11310477","relation":{},"subject":[],"published":{"date-parts":[[2025,10,6]]}}}