{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T23:15:41Z","timestamp":1763507741429,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":22,"publisher":"ACM","license":[{"start":{"date-parts":[[2019,11,6]],"date-time":"2019-11-06T00:00:00Z","timestamp":1572998400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"Portuguese Foundation for Science and Technology (FCT)","award":["SFRH\/BSAB\/143018\/2018","FCT-PD\/BD\/113967\/201","PTDC\/CCI-INF\/31698\/2017"],"award-info":[{"award-number":["SFRH\/BSAB\/143018\/2018","FCT-PD\/BD\/113967\/201","PTDC\/CCI-INF\/31698\/2017"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2019,11,6]]},"DOI":"10.1145\/3319535.3354228","type":"proceedings-article","created":{"date-parts":[[2019,11,7]],"date-time":"2019-11-07T13:08:32Z","timestamp":1573132112000},"page":"63-78","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":19,"title":["A Machine-Checked Proof of Security for AWS Key Management Service"],"prefix":"10.1145","author":[{"given":"Jos\u00e9 Bacelar","family":"Almeida","sequence":"first","affiliation":[{"name":"University of Minho and INESC TEC, Braga, Portugal"}]},{"given":"Manuel","family":"Barbosa","sequence":"additional","affiliation":[{"name":"University of Porto (FCUP) and INESC TEC, Porto, Portugal"}]},{"given":"Gilles","family":"Barthe","sequence":"additional","affiliation":[{"name":"IMDEA Software Institute and MPI-SP, Madrid, Spain"}]},{"given":"Matthew","family":"Campagna","sequence":"additional","affiliation":[{"name":"Amazon Web Services, Seattle, WA, USA"}]},{"given":"Ernie","family":"Cohen","sequence":"additional","affiliation":[{"name":"Amazon Web Services, New York, NY, USA"}]},{"given":"Benjamin","family":"Gregoire","sequence":"additional","affiliation":[{"name":"Inria, Sophia-Antipolis, France"}]},{"given":"Vitor","family":"Pereira","sequence":"additional","affiliation":[{"name":"University of Porto (FCUP) and INESC TEC, Porto, Portugal"}]},{"given":"Bernardo","family":"Portela","sequence":"additional","affiliation":[{"name":"University of Porto (FCUP) and INESC TEC, Porto, Portugal"}]},{"given":"Pierre-Yves","family":"Strub","sequence":"additional","affiliation":[{"name":"\u00c9cole Polytechnique, Palaiseau, France"}]},{"given":"Serdar","family":"Tasiran","sequence":"additional","affiliation":[{"name":"Amazon Web Services, New York, NY, USA"}]}],"member":"320","published-online":{"date-parts":[[2019,11,6]]},"reference":[{"key":"e_1_3_2_2_1_1","volume-title":"DHIES: An Encryption Scheme Based On The Diffie-Hellman Problem. Contributions to IEEE P1363a.(Sept.","author":"Abdalla Michel","year":"1998","unstructured":"Michel Abdalla , Mihir Bellare , and Phillip Rogaway . 1998 . DHIES: An Encryption Scheme Based On The Diffie-Hellman Problem. Contributions to IEEE P1363a.(Sept. 1998). Michel Abdalla, Mihir Bellare, and Phillip Rogaway. 1998. DHIES: An Encryption Scheme Based On The Diffie-Hellman Problem. Contributions to IEEE P1363a.(Sept. 1998)."},{"volume-title":"CT-RSA 2001 (LNCS)","author":"Abdalla Michel","key":"e_1_3_2_2_2_1","unstructured":"Michel Abdalla , Mihir Bellare , and Phillip Rogaway . 2001. The Oracle Diffie-Hellman Assumptions and an Analysis of DHIES . In CT-RSA 2001 (LNCS) , David Naccache (Ed.), Vol. 2020 . Springer , Heidelberg , 143--158. https:\/\/doi.org\/10.1007\/3--540--45353--9_12 10.1007\/3--540--45353--9_12 Michel Abdalla, Mihir Bellare, and Phillip Rogaway. 2001. The Oracle Diffie-Hellman Assumptions and an Analysis of DHIES. In CT-RSA 2001 (LNCS), David Naccache (Ed.), Vol. 2020. Springer, Heidelberg, 143--158. https:\/\/doi.org\/10.1007\/3--540--45353--9_12"},{"volume-title":"Thomas Peyrin (Ed.)","author":"Almeida Jos\u00e9 Bacelar","key":"e_1_3_2_2_3_1","unstructured":"Jos\u00e9 Bacelar Almeida , Manuel Barbosa , Gilles Barthe , and Fran\u00e7ois Dupressoir . 2016. Verifiable Side-Channel Security of Cryptographic Implementations: Constant-Time MEE-CBC. InFSE 2016 (LNCS) , Thomas Peyrin (Ed.) , Vol. 9783 . Springer , Heidelberg , 163--184. https:\/\/doi.org\/10.1007\/978--3--662--52993--5_9 10.1007\/978--3--662--52993--5_9 Jos\u00e9 Bacelar Almeida, Manuel Barbosa, Gilles Barthe, and Fran\u00e7ois Dupressoir. 2016. Verifiable Side-Channel Security of Cryptographic Implementations: Constant-Time MEE-CBC. InFSE 2016 (LNCS), Thomas Peyrin (Ed.), Vol. 9783. Springer, Heidelberg, 163--184. https:\/\/doi.org\/10.1007\/978--3--662--52993--5_9"},{"key":"e_1_3_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3134017"},{"key":"e_1_3_2_2_5_1","volume-title":"AWS Key Management Service Crypto-graphic Details. (August","author":"Amazon Web","year":"2018","unstructured":"Amazon Web Services (AWS). 2018. AWS Key Management Service Crypto-graphic Details. (August 2018 ). https:\/\/d1.awsstatic.com\/whitepapers\/KMS-Cryptographic-Details.pdf. Amazon Web Services (AWS). 2018. AWS Key Management Service Crypto-graphic Details. (August 2018). https:\/\/d1.awsstatic.com\/whitepapers\/KMS-Cryptographic-Details.pdf."},{"volume-title":"Foundations of Security Analysis and Design VII - FOSAD 2012\/2013 Tutorial Lectures (Lecture Notes in Computer Science), Alessandro Aldini, Javier L\u00f3pez","author":"Barthe Gilles","key":"e_1_3_2_2_6_1","unstructured":"Gilles Barthe , Fran\u00e7ois Dupressoir , Benjamin Gr\u00e9goire , C\u00e9sar Kunz , Benedikt Schmidt , and Pierre-Yves Strub . 2013. EasyCrypt: A Tutorial . In Foundations of Security Analysis and Design VII - FOSAD 2012\/2013 Tutorial Lectures (Lecture Notes in Computer Science), Alessandro Aldini, Javier L\u00f3pez , and Fabio Martinelli(Eds.), Vol. 8604 . Springer , 146--166. https:\/\/doi.org\/10.1007\/978--3--319--10082--1_6 10.1007\/978--3--319--10082--1_6 Gilles Barthe, Fran\u00e7ois Dupressoir, Benjamin Gr\u00e9goire, C\u00e9sar Kunz, Benedikt Schmidt, and Pierre-Yves Strub. 2013. EasyCrypt: A Tutorial. In Foundations of Security Analysis and Design VII - FOSAD 2012\/2013 Tutorial Lectures (Lecture Notes in Computer Science), Alessandro Aldini, Javier L\u00f3pez, and Fabio Martinelli(Eds.), Vol. 8604. Springer, 146--166. https:\/\/doi.org\/10.1007\/978--3--319--10082--1_6"},{"key":"e_1_3_2_2_7_1","volume-title":"Computer-Aided Security Proofs for the Working Cryptographer. In CRYPTO 2011 (LNCS), Phillip Rogaway (Ed.)","volume":"6841","author":"Barthe Gilles","year":"2011","unstructured":"Gilles Barthe , Benjamin Gr\u00e9goire , Sylvain Heraud , and Santiago Zanella B\u00e9guelin . 2011 . Computer-Aided Security Proofs for the Working Cryptographer. In CRYPTO 2011 (LNCS), Phillip Rogaway (Ed.) , Vol. 6841 . Springer, Heidelberg, 71--90. https:\/\/doi.org\/10.1007\/978--3--642--22792--9_5 10.1007\/978--3--642--22792--9_5 Gilles Barthe, Benjamin Gr\u00e9goire, Sylvain Heraud, and Santiago Zanella B\u00e9guelin. 2011. Computer-Aided Security Proofs for the Working Cryptographer. In CRYPTO 2011 (LNCS), Phillip Rogaway (Ed.), Vol. 6841. Springer, Heidelberg, 71--90. https:\/\/doi.org\/10.1007\/978--3--642--22792--9_5"},{"key":"e_1_3_2_2_8_1","volume-title":"Randomness Reuse in Multi-recipient Encryption Schemeas. In PKC 2003 (LNCS), Yvo Desmedt(Ed.)","volume":"2567","author":"Bellare Mihir","year":"2003","unstructured":"Mihir Bellare , Alexandra Boldyreva , and Jessica Staddon . 2003 . Randomness Reuse in Multi-recipient Encryption Schemeas. In PKC 2003 (LNCS), Yvo Desmedt(Ed.) , Vol. 2567 . Springer, Heidelberg, 85--99. https:\/\/doi.org\/10.1007\/3--540--36288--6_7 10.1007\/3--540--36288--6_7 Mihir Bellare, Alexandra Boldyreva, and Jessica Staddon. 2003. Randomness Reuse in Multi-recipient Encryption Schemeas. In PKC 2003 (LNCS), Yvo Desmedt(Ed.), Vol. 2567. Springer, Heidelberg, 85--99. https:\/\/doi.org\/10.1007\/3--540--36288--6_7"},{"key":"e_1_3_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2006.1"},{"key":"e_1_3_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2018.00009"},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2008.12"},{"key":"e_1_3_2_2_12_1","volume-title":"ACM CCS 10, Ehab Al-Shaer,Angelos D","author":"Bortolozzo Matteo","year":"1866","unstructured":"Matteo Bortolozzo , Matteo Centenaro , Riccardo Focardi , and Graham Steel . 2010. Attacking and fixing PKCS#11 security tokens . In ACM CCS 10, Ehab Al-Shaer,Angelos D . Keromytis, and Vitaly Shmatikov (Eds.). ACM Press , 260--269. https:\/\/doi.org\/10.1145\/ 1866 307.1866337 10.1145\/1866307.1866337 Matteo Bortolozzo, Matteo Centenaro, Riccardo Focardi, and Graham Steel. 2010. Attacking and fixing PKCS#11 security tokens. In ACM CCS 10, Ehab Al-Shaer,Angelos D. Keromytis, and Vitaly Shmatikov (Eds.). ACM Press, 260--269. https:\/\/doi.org\/10.1145\/1866307.1866337"},{"key":"e_1_3_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2009.7"},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.2001.959888"},{"key":"e_1_3_2_2_15_1","volume-title":"Universally Composable Security with Global Setup. In TCC 2007 (LNCS), Salil P. Vadhan(Ed.)","volume":"4392","author":"Canetti Ran","year":"2007","unstructured":"Ran Canetti , Yevgeniy Dodis , Rafael Pass , and Shabsi Walfish . 2007 . Universally Composable Security with Global Setup. In TCC 2007 (LNCS), Salil P. Vadhan(Ed.) , Vol. 4392 . Springer, Heidelberg, 61--85. https:\/\/doi.org\/10.1007\/978--3--540--70936--7_4 10.1007\/978--3--540--70936--7_4 Ran Canetti, Yevgeniy Dodis, Rafael Pass, and Shabsi Walfish. 2007. Universally Composable Security with Global Setup. In TCC 2007 (LNCS), Salil P. Vadhan(Ed.), Vol. 4392. Springer, Heidelberg, 61--85. https:\/\/doi.org\/10.1007\/978--3--540--70936--7_4"},{"key":"e_1_3_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2008.16"},{"key":"e_1_3_2_2_17_1","volume-title":"Universally Composable Key-Management. In ESORICS 2013 (LNCS), Jason Crampton, Sushil Jajodia, and Keith Mayes (Eds.)","volume":"8134","author":"Kremer Steve","year":"2013","unstructured":"Steve Kremer , Robert K\u00fcnnemann , and Graham Steel . 2013 . Universally Composable Key-Management. In ESORICS 2013 (LNCS), Jason Crampton, Sushil Jajodia, and Keith Mayes (Eds.) , Vol. 8134 . Springer, Heidelberg, 327--344. https:\/\/doi.org\/10.1007\/978--3--642--40203--6_19 10.1007\/978--3--642--40203--6_19 Steve Kremer, Robert K\u00fcnnemann, and Graham Steel. 2013. Universally Composable Key-Management. In ESORICS 2013 (LNCS), Jason Crampton, Sushil Jajodia, and Keith Mayes (Eds.), Vol. 8134. Springer, Heidelberg, 327--344. https:\/\/doi.org\/10.1007\/978--3--642--40203--6_19"},{"key":"e_1_3_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2011.25"},{"volume-title":"Proceedings of the 2008 International Symposium on Software Testing and Analysis (ISSTA '08)","author":"Papi Matthew M.","key":"e_1_3_2_2_19_1","unstructured":"Matthew M. Papi , Mahmood Ali , Telmo Luis Correa , Jr., Jeff H. Perkins , and Michael D. Ernst . 2008. Practical Pluggable Types for Java . In Proceedings of the 2008 International Symposium on Software Testing and Analysis (ISSTA '08) . ACM,New York, NY, USA, 201--212. https:\/\/doi.org\/10.1145\/1390630.1390656 10.1145\/1390630.1390656 Matthew M. Papi, Mahmood Ali, Telmo Luis Correa, Jr., Jeff H. Perkins, and Michael D. Ernst. 2008. Practical Pluggable Types for Java. In Proceedings of the 2008 International Symposium on Software Testing and Analysis (ISSTA '08). ACM,New York, NY, USA, 201--212. https:\/\/doi.org\/10.1145\/1390630.1390656"},{"volume-title":"Progress in Cryptology- VIETCRYPT 06 (LNCS), Phong Q","author":"Rogaway Phillip","key":"e_1_3_2_2_20_1","unstructured":"Phillip Rogaway . 2006. Formalizing Human Ignorance . In Progress in Cryptology- VIETCRYPT 06 (LNCS), Phong Q . Nguyen (Ed.), Vol. 4341 . Springer , Heidelberg ,211--228. Phillip Rogaway. 2006. Formalizing Human Ignorance. In Progress in Cryptology- VIETCRYPT 06 (LNCS), Phong Q. Nguyen (Ed.), Vol. 4341. Springer, Heidelberg,211--228."},{"key":"e_1_3_2_2_21_1","unstructured":"Victor Shoup. 2001. A Proposal for an ISO Standard for Public Key Encryption(version 2.1). (2001). https:\/\/www.shoup.net\/papers\/iso-2_1.pdf.  Victor Shoup. 2001. A Proposal for an ISO Standard for Public Key Encryption(version 2.1). (2001). https:\/\/www.shoup.net\/papers\/iso-2_1.pdf."},{"key":"e_1_3_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-53018-4_11"}],"event":{"name":"CCS '19: 2019 ACM SIGSAC Conference on Computer and Communications Security","sponsor":["SIGSAC ACM Special Interest Group on Security, Audit, and Control"],"location":"London United Kingdom","acronym":"CCS '19"},"container-title":["Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3319535.3354228","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3319535.3354228","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:24:03Z","timestamp":1750202643000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3319535.3354228"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,11,6]]},"references-count":22,"alternative-id":["10.1145\/3319535.3354228","10.1145\/3319535"],"URL":"https:\/\/doi.org\/10.1145\/3319535.3354228","relation":{},"subject":[],"published":{"date-parts":[[2019,11,6]]},"assertion":[{"value":"2019-11-06","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}