{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,20]],"date-time":"2026-08-20T15:37:26Z","timestamp":1787240246270,"version":"build-2736575974"},"publisher-location":"New York, NY, USA","reference-count":36,"publisher":"ACM","license":[{"start":{"date-parts":[[2021,11,12]],"date-time":"2021-11-12T00:00:00Z","timestamp":1636675200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100008530","name":"European Regional Development Fund","doi-asserted-by":"publisher","award":["POR FESR 2014-2020 Azione 1.1.4 DGR 822\/2020 ? ID 10288513"],"award-info":[{"award-number":["POR FESR 2014-2020 Azione 1.1.4 DGR 822\/2020 ? ID 10288513"]}],"id":[{"id":"10.13039\/501100008530","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2021,11,12]]},"DOI":"10.1145\/3460120.3484785","type":"proceedings-article","created":{"date-parts":[[2021,11,13]],"date-time":"2021-11-13T12:05:34Z","timestamp":1636805134000},"page":"412-428","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":8,"title":["A Formally Verified Configuration for Hardware Security Modules in the Cloud"],"prefix":"10.1145","author":[{"given":"Riccardo","family":"Focardi","sequence":"first","affiliation":[{"name":"Ca' Foscari University, Venice, Italy"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Flaminia L.","family":"Luccio","sequence":"additional","affiliation":[{"name":"Ca' Foscari University, Venice, Italy"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2021,11,13]]},"reference":[{"key":"e_1_3_2_2_1_1","volume-title":"Type-Based Analysis of Generic Key Management APIs. In 2013 IEEE 26th Computer Security Foundations Symposium","author":"P. Ad","year":"2013","unstructured":"P. Ad a o, R. Focardi, and F. L. Luccio. 2013. Type-Based Analysis of Generic Key Management APIs. In 2013 IEEE 26th Computer Security Foundations Symposium, New Orleans, LA, USA, June 26--28, 2013. 97--111."},{"key":"e_1_3_2_2_2_1","volume-title":"2021 a. AWS CloudHSM. Accessed","year":"2021","unstructured":"Amazon. 2021 a. AWS CloudHSM. Accessed in May 2021 at https:\/\/aws.amazon.com\/cloudhsm\/."},{"key":"e_1_3_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/3--540--44810--1_17"},{"key":"e_1_3_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44709-1_19"},{"key":"e_1_3_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/2.955101"},{"key":"e_1_3_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1866307.1866337"},{"key":"e_1_3_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-130479"},{"key":"e_1_3_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978--3--642-04444--1_4"},{"key":"e_1_3_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/3--540--36400--5_42"},{"key":"e_1_3_2_2_10_1","volume-title":"2003 a. The Design and Analysis of Cryptographic APIs for Security Devices. Master's thesis","author":"Clulow J.","unstructured":"J. Clulow. 2003 a. The Design and Analysis of Cryptographic APIs for Security Devices. Master's thesis. University of Natal, Durban."},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45238-6_32"},{"key":"e_1_3_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2014.07.010"},{"key":"e_1_3_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.14722\/ndss.2019.23394"},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3372297.3423354"},{"key":"e_1_3_2_2_15_1","volume-title":"29th USENIX Security Symposium (USENIX'20)","author":"Cremers C.","unstructured":"C. Cremers, B. Kiesl, and N. Medinger. 2020 b. A Formal Analysis of IEEE 802.11textquoterights WPA2: Countering the Kracks Caused by Cracking the Counters. In 29th USENIX Security Symposium (USENIX'20). USENIX Association, 1--17. https:\/\/www.usenix.org\/conference\/usenixsecurity20\/presentation\/cremers"},{"key":"e_1_3_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2019.00012"},{"key":"e_1_3_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-2009-0394"},{"key":"e_1_3_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/TIT.1983.1056650"},{"key":"e_1_3_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF49147.2020.00029"},{"key":"e_1_3_2_2_20_1","volume-title":"Cloud: Tamarin model. https:\/\/github.com\/secgroup\/CloudHSM-model .","author":"Focardi R.","year":"2021","unstructured":"R. Focardi and F. L. Luccio. 2021. A Formally Verified Configuration for Hardware Security Modules in the Cloud: Tamarin model. https:\/\/github.com\/secgroup\/CloudHSM-model ."},{"key":"e_1_3_2_2_21_1","doi-asserted-by":"crossref","unstructured":"R. Focardi F. L. Luccio and G. Steel. 2011. An Introduction to Security API Analysis. In Foundations of Security Analysis and Design VI - FOSAD Tutorial Lectures. 35--65.","DOI":"10.1007\/978-3-642-23082-0_2"},{"key":"e_1_3_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978--3--642--29420--4_9"},{"key":"e_1_3_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.5555\/3241094.3241166"},{"key":"e_1_3_2_2_24_1","volume-title":"Formal Analysis of Diffie-Hellman Protocols. In 29th USENIX Security Symposium (USENIX'20)","author":"Girol G.","year":"1857","unstructured":"G. Girol, L. Hirschi, Sasse R., D. Jackson, C. Cremers, and D. Basin. 2020. A Spectral Analysis of Noise: A Comprehensive, Automated, Formal Analysis of Diffie-Hellman Protocols. In 29th USENIX Security Symposium (USENIX'20). USENIX Association, 1857--1874. https:\/\/www.usenix.org\/conference\/usenixsecurity20\/presentation\/girol"},{"key":"e_1_3_2_2_25_1","volume-title":"Accessed","author":"Cloud","year":"2021","unstructured":"Google. 2021. Cloud HSM. Accessed in May 2021 at https:\/\/cloud.google.com\/kms\/docs\/hsm ."},{"key":"e_1_3_2_2_26_1","volume-title":"2021 a. Cloud HSM. Accessed","author":"IBM.","year":"2021","unstructured":"IBM. 2021 a. Cloud HSM. Accessed in May 2021 at https:\/\/cloud.ibm.com\/catalog\/infrastructure\/hardware-security-module ."},{"key":"e_1_3_2_2_27_1","volume-title":"2021 b. Cloud HSM documentation: Managing key rings. Accessed","author":"IBM.","year":"2021","unstructured":"IBM. 2021 b. Cloud HSM documentation: Managing key rings. Accessed in September 2021 at https:\/\/cloud.ibm.com\/docs\/hs-crypto?topic=hs-crypto-managing-key-rings ."},{"key":"e_1_3_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978--3--662--46666--7_12"},{"key":"e_1_3_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167--4048(92)90222-D"},{"key":"e_1_3_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978--3--642--39799--8_48"},{"key":"e_1_3_2_2_31_1","volume-title":"Azure Dedicated HSM. Accessed","year":"2021","unstructured":"Microsoft. 2021. Azure Dedicated HSM. Accessed in September 2021 at https:\/\/azure.microsoft.com\/en-us\/services\/azure-dedicated-hsm\/."},{"key":"e_1_3_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978--3--319--70972--7_8"},{"key":"e_1_3_2_2_33_1","unstructured":"G. Steel. 2014. Proposal: Authenticated Attributes for Key Wrap in PKCS#11. Available at https:\/\/lists.oasis-open.org\/archives\/pkcs11\/201408\/msg00006\/pkcs11-authenticated-encryption-key-transport.pdf ."},{"key":"e_1_3_2_2_34_1","volume-title":"Accessed","author":"Cloud","year":"2021","unstructured":"Utimaco. 2021. Cloud HSM. Accessed in May 2021 at https:\/\/hsm.utimaco.com\/products-hardware-security-modules\/form-factor\/cloud-hsm-as-a-service\/."},{"key":"e_1_3_2_2_35_1","volume-title":"Proceedings of the 22th USENIX Security Symposium (USENIX'13)","author":"Verdult R.","year":"2013","unstructured":"R. Verdult, F.D. Garcia, and B. Ege. 2013. Dismantling Megamos Crypto: Wirelessly Lockpicking a Vehicle Immobilizer. In Proceedings of the 22th USENIX Security Symposium (USENIX'13), Washington, DC, USA, August 14--16, 2013, Samuel T. King (Ed.). USENIX Association, 703--718. https:\/\/www.usenix.org\/conference\/usenixsecurity15\/technical-sessions\/presentation\/verdult"},{"key":"e_1_3_2_2_36_1","volume-title":"Technical Report UCAM-CL-TR-644. University of Cambridge. https:\/\/www.cl.cam.ac.uk\/techreports\/UCAM-CL-TR-644.pdf.","author":"Youn P.","year":"2005","unstructured":"P. Youn, B. Adida, M. Bond, J. Clulow, J. Herzog, A. Lin, R. Rivest, and R. Anderson. 2005. Robbing the bank with a theorem prover. Technical Report UCAM-CL-TR-644. University of Cambridge. https:\/\/www.cl.cam.ac.uk\/techreports\/UCAM-CL-TR-644.pdf."}],"event":{"name":"CCS '21: 2021 ACM SIGSAC Conference on Computer and Communications Security","location":"Virtual Event Republic of Korea","acronym":"CCS '21","sponsor":["SIGSAC ACM Special Interest Group on Security, Audit, and Control"]},"container-title":["Proceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3460120.3484785","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3460120.3484785","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T20:51:39Z","timestamp":1763499099000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3460120.3484785"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,11,12]]},"references-count":36,"alternative-id":["10.1145\/3460120.3484785","10.1145\/3460120"],"URL":"https:\/\/doi.org\/10.1145\/3460120.3484785","relation":{},"subject":[],"published":{"date-parts":[[2021,11,12]]},"assertion":[{"value":"2021-11-13","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}