{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:19:58Z","timestamp":1750220398289,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":24,"publisher":"ACM","license":[{"start":{"date-parts":[[2021,11,20]],"date-time":"2021-11-20T00:00:00Z","timestamp":1637366400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["HR0011-18-9-0001"],"award-info":[{"award-number":["HR0011-18-9-0001"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100009226","name":"National Security Agency","doi-asserted-by":"publisher","award":["H98230-18-D-0009"],"award-info":[{"award-number":["H98230-18-D-0009"]}],"id":[{"id":"10.13039\/100009226","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2021,11,20]]},"DOI":"10.1145\/3487212.3487340","type":"proceedings-article","created":{"date-parts":[[2021,12,21]],"date-time":"2021-12-21T20:01:45Z","timestamp":1640116905000},"page":"111-117","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":8,"title":["Design and formal verification of a copland-based attestation protocol"],"prefix":"10.1145","author":[{"given":"Adam","family":"Petz","sequence":"first","affiliation":[{"name":"The University of Kansas"}]},{"given":"Grant","family":"Jurgensen","sequence":"additional","affiliation":[{"name":"The University of Kansas"}]},{"given":"Perry","family":"Alexander","sequence":"additional","affiliation":[{"name":"The University of Kansas"}]}],"member":"320","published-online":{"date-parts":[[2021,12,21]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"https:\/\/ku-sldg.github.io\/copland","author":"Copland","year":"2021","unstructured":"Copland website. https:\/\/ku-sldg.github.io\/copland , 2021 . Copland website. https:\/\/ku-sldg.github.io\/copland, 2021."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/DASC.2018.8569752"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/MILCOM.2018.8599862"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10207-011-0124-7"},{"key":"e_1_3_2_1_5_1","volume-title":"Proceedings of the Third Virtual Machine Research and Technology Symposium","author":"Haldar V.","year":"2004","unstructured":"Haldar , V. , Chandra , D. , and Franz , M . Semantic remote attestation - a virtual machine directed approach to trusted computing . In Proceedings of the Third Virtual Machine Research and Technology Symposium ( San Jose, CA , May 2004 ). Haldar, V., Chandra, D., and Franz, M. Semantic remote attestation - a virtual machine directed approach to trusted computing. In Proceedings of the Third Virtual Machine Research and Technology Symposium (San Jose, CA, May 2004)."},{"key":"e_1_3_2_1_6_1","unstructured":"Helble S. Kretz I. Loscocco P. Ramsdell J. Rowe P. and Alexander P. Flexible mechanisms for remote attestation. ACM Transactions on Privacy and Security (to appear).  Helble S. Kretz I. Loscocco P. Ramsdell J. Rowe P. and Alexander P. Flexible mechanisms for remote attestation. ACM Transactions on Privacy and Security (to appear)."},{"key":"e_1_3_2_1_7_1","volume-title":"A copland attestation manager (am) in cakeml. https:\/\/github.com\/ku-sldg\/am-cakeml","author":"Jurgensen G.","year":"2021","unstructured":"Jurgensen , G. , Petz , A. , Alexander , P. , Barclay , T. , Komp , E. , Neises , M. , and Cousino , A . A copland attestation manager (am) in cakeml. https:\/\/github.com\/ku-sldg\/am-cakeml , 2021 . Jurgensen, G., Petz, A., Alexander, P., Barclay, T., Komp, E., Neises, M., and Cousino, A. A copland attestation manager (am) in cakeml. https:\/\/github.com\/ku-sldg\/am-cakeml, 2021."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1743546.1743574"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2013.35"},{"key":"e_1_3_2_1_10_1","first-page":"1429","volume-title":"Proceedings of the 28th USENIX Conference on Security Symposium (USA, 2019), SEC'19, USENIX Association","author":"Nunes I. D. O.","unstructured":"Nunes , I. D. O. , Eldefrawy , K. , Rattanavipanon , N. , Steiner , M. , and Tsudik , G . Vrased: A verified hardware\/software co-design for remote attestation . In Proceedings of the 28th USENIX Conference on Security Symposium (USA, 2019), SEC'19, USENIX Association , pp. 1429 -- 1446 . Nunes, I. D. O., Eldefrawy, K., Rattanavipanon, N., Steiner, M., and Tsudik, G. Vrased: A verified hardware\/software co-design for remote attestation. In Proceedings of the 28th USENIX Conference on Security Symposium (USA, 2019), SEC'19, USENIX Association, pp. 1429--1446."},{"key":"e_1_3_2_1_11_1","first-page":"771","volume-title":"29th USENIX Security Symposium (USENIX Security 20)","author":"Nunes I. D. O.","year":"2020","unstructured":"Nunes , I. D. O. , Eldefrawy , K. , Rattanavipanon , N. , and Tsudik , G . APEX: A verified architecture for proofs of execution on remote devices under full software compromise . In 29th USENIX Security Symposium (USENIX Security 20) ( Aug. 2020 ), USENIX Association , pp. 771 -- 788 . Nunes, I. D. O., Eldefrawy, K., Rattanavipanon, N., and Tsudik, G. APEX: A verified architecture for proofs of execution on remote devices under full software compromise. In 29th USENIX Security Symposium (USENIX Security 20) (Aug. 2020), USENIX Association, pp. 771--788."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/MILCOM.2018.8599735"},{"key":"e_1_3_2_1_13_1","volume-title":"copland-avm, nfm21 release. https:\/\/github.com\/ku-sldg\/copland-avm\/releases\/tag\/v1.0","author":"Petz A.","year":"2020","unstructured":"Petz , A. copland-avm, nfm21 release. https:\/\/github.com\/ku-sldg\/copland-avm\/releases\/tag\/v1.0 , 2020 . Petz, A. copland-avm, nfm21 release. https:\/\/github.com\/ku-sldg\/copland-avm\/releases\/tag\/v1.0, 2020."},{"key":"e_1_3_2_1_14_1","volume-title":"TN","author":"Petz A.","year":"2019","unstructured":"Petz , A. , and Alexander , P . A copland attestation manager. In Hot Topics in Science of Security (HoTSoS'19) (Nashville , TN , April 8-11 2019 ). Petz, A., and Alexander, P. A copland attestation manager. In Hot Topics in Science of Security (HoTSoS'19) (Nashville, TN, April 8-11 2019)."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-76384-8_17"},{"key":"e_1_3_2_1_16_1","volume-title":"haskell-am. https:\/\/github.com\/ku-sldg\/haskell-am","author":"Petz A.","year":"2020","unstructured":"Petz , A. , and Komp , E . haskell-am. https:\/\/github.com\/ku-sldg\/haskell-am , 2020 . Petz, A., and Komp, E. haskell-am. https:\/\/github.com\/ku-sldg\/haskell-am, 2020."},{"key":"e_1_3_2_1_17_1","volume-title":"Czech Republic","author":"Ramsdell J.","year":"2019","unstructured":"Ramsdell , J. , Rowe , P. D. , Alexander , P. , Helble , S. , Loscocco , P. , Pendergrass , J. A. , and Petz , A . Orchestrating layered attestations. In Principles of Security and Trust (POST'19) (Prague , Czech Republic , April 8-11 2019 ). Ramsdell, J., Rowe, P. D., Alexander, P., Helble, S., Loscocco, P., Pendergrass, J. A., and Petz, A. Orchestrating layered attestations. In Principles of Security and Trust (POST'19) (Prague, Czech Republic, April 8-11 2019)."},{"key":"e_1_3_2_1_18_1","volume-title":"Chase: A model finder for finitary geometric logic. https:\/\/github.com\/ramsdell\/chase","author":"Ramsdell J. D.","year":"2020","unstructured":"Ramsdell , J. D. Chase: A model finder for finitary geometric logic. https:\/\/github.com\/ramsdell\/chase , 2020 . Ramsdell, J. D. Chase: A model finder for finitary geometric logic. https:\/\/github.com\/ramsdell\/chase, 2020."},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3479394.3479418"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-45572-3_7"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-46263-9_10"},{"key":"e_1_3_2_1_22_1","volume-title":"ICFEM 2020, Singapore, Singapore, March 1-3, 2021, Proceedings","volume":"12531","author":"Sardar M. U.","year":"2020","unstructured":"Sardar , M. U. , Faqeh , R. , and Fetzer , C . Formal foundations for intel SGX data center attestation primitives. In Formal Methods and Software Engineering - 22nd International Conference on Formal Engineering Methods , ICFEM 2020, Singapore, Singapore, March 1-3, 2021, Proceedings ( 2020 ), S. Lin, Z. Hou, and B. P. Mahony, Eds. , vol. 12531 of Lecture Notes in Computer Science, Springer, pp. 268--283. Sardar, M. U., Faqeh, R., and Fetzer, C. Formal foundations for intel SGX data center attestation primitives. In Formal Methods and Software Engineering - 22nd International Conference on Formal Engineering Methods, ICFEM 2020, Singapore, Singapore, March 1-3, 2021, Proceedings (2020), S. Lin, Z. Hou, and B. P. Mahony, Eds., vol. 12531 of Lecture Notes in Computer Science, Springer, pp. 268--283."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2021.3087421"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/DSD51259.2020.00099"}],"event":{"name":"MEMOCODE '21: 19th ACM-IEEE International Conference on Formal Methods and Models for System Design","sponsor":["SIGBED ACM Special Interest Group on Embedded Systems","SIGDA ACM Special Interest Group on Design Automation","IEEE CAS","IEEE CEDA"],"location":"Virtual Event China","acronym":"MEMOCODE '21"},"container-title":["Proceedings of the 19th ACM-IEEE International Conference on Formal Methods and Models for System Design"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3487212.3487340","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3487212.3487340","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3487212.3487340","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:18:47Z","timestamp":1750191527000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3487212.3487340"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,11,20]]},"references-count":24,"alternative-id":["10.1145\/3487212.3487340","10.1145\/3487212"],"URL":"https:\/\/doi.org\/10.1145\/3487212.3487340","relation":{},"subject":[],"published":{"date-parts":[[2021,11,20]]},"assertion":[{"value":"2021-12-21","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}