{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,22]],"date-time":"2025-12-22T22:14:51Z","timestamp":1766441691458,"version":"3.48.0"},"publisher-location":"New York, NY, USA","reference-count":16,"publisher":"ACM","funder":[{"name":"National Science and Technology Council, Taiwan","award":["NSTC-113-2634-F-001-002-MBK"],"award-info":[{"award-number":["NSTC-113-2634-F-001-002-MBK"]}]},{"name":"National Science and Technology Council, Taiwan","award":["113-2634-F-011-002-MBK"],"award-info":[{"award-number":["113-2634-F-011-002-MBK"]}]},{"name":"National Science and Technology Council, Taiwan","award":["113-2221-E-001-023-MY3"],"award-info":[{"award-number":["113-2221-E-001-023-MY3"]}]},{"name":"National Science and Technology Council, Taiwan","award":["111-2221-E-001-014-MY3"],"award-info":[{"award-number":["111-2221-E-001-014-MY3"]}]},{"name":"Academia Sinica","award":["AS-GCP-114-M01"],"award-info":[{"award-number":["AS-GCP-114-M01"]}]},{"name":"Funda\u00e7\u00e3o para a Ci\u00eancia e Tecnologia (FCT), Portugal","award":["2024.04803.BD"],"award-info":[{"award-number":["2024.04803.BD"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2025,11,19]]},"DOI":"10.1145\/3719027.3744814","type":"proceedings-article","created":{"date-parts":[[2025,11,22]],"date-time":"2025-11-22T23:32:38Z","timestamp":1763854358000},"page":"1409-1423","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Jazzline: Composable CryptoLine Functional Correctness Proofs for Jasmin Programs"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0011-7455","authenticated-orcid":false,"given":"Jos\u00e9 Bacelar","family":"Almeida","sequence":"first","affiliation":[{"name":"University of Minho and INESC TEC, Braga, Portugal"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6848-5564","authenticated-orcid":false,"given":"Manuel","family":"Barbosa","sequence":"additional","affiliation":[{"name":"Universidade do Porto (FCUP) and INESC TEC, Porto, Portugal and Max Planck Institute for Security and Privacy, Bochum, Germany"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3853-1777","authenticated-orcid":false,"given":"Gilles","family":"Barthe","sequence":"additional","affiliation":[{"name":"Max Planck Institute for Security and Privacy, Bochum, Germany and IMDEA Software Institute, Madrid, Spain"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9058-2005","authenticated-orcid":false,"given":"Lionel","family":"Blatter","sequence":"additional","affiliation":[{"name":"Max Planck Institute for Security and Privacy, Bochum, Germany"}]},{"ORCID":"https:\/\/orcid.org\/0009-0005-6458-1419","authenticated-orcid":false,"given":"Gustavo","family":"Delerue","sequence":"additional","affiliation":[{"name":"Universidade do Porto (FCUP), Porto, Portugal"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5236-260X","authenticated-orcid":false,"given":"Jo\u00e3o Diogo","family":"Duarte","sequence":"additional","affiliation":[{"name":"Universidade do Porto (FCUP) & INESC TEC, Porto, Portugal"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6650-9924","authenticated-orcid":false,"given":"Benjamin","family":"Gregoire","sequence":"additional","affiliation":[{"name":"Inria Sophia-Antipolis, Sophia Antipolis, France"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7395-3070","authenticated-orcid":false,"given":"Tiago","family":"Oliveira","sequence":"additional","affiliation":[{"name":"Sandbox AQ, Palo Alto, USA"}]},{"ORCID":"https:\/\/orcid.org\/0009-0008-8350-6870","authenticated-orcid":false,"given":"Miguel","family":"Quaresma","sequence":"additional","affiliation":[{"name":"MPI for Security and Privacy, Bochum, Germany"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8196-7875","authenticated-orcid":false,"given":"Pierre-Yves","family":"Strub","sequence":"additional","affiliation":[{"name":"PQShield, Paris, France"}]},{"ORCID":"https:\/\/orcid.org\/0009-0001-7621-7981","authenticated-orcid":false,"given":"Ming-Hsien","family":"Tsai","sequence":"additional","affiliation":[{"name":"National Taiwan University of Science and Technology, Taipei, Taiwan"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5757-545X","authenticated-orcid":false,"given":"Bow-Yaw","family":"Wang","sequence":"additional","affiliation":[{"name":"Academia Sinica, Taipei, Taiwan"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9362-5282","authenticated-orcid":false,"given":"Bo-Yin","family":"Yang","sequence":"additional","affiliation":[{"name":"Academia Sinica, Taipei, Taiwan"}]}],"member":"320","published-online":{"date-parts":[[2025,11,22]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.46586\/tches.v2023.i3.164-193"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3319535.3363211"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-68379-4_12"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2701415"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40001.2021.00008"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.62056\/a3qj89n4e"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22792-9_5"},{"key":"e_1_3_2_1_8_1","unstructured":"Deirdre Connolly Peter Schwabe and Bas Westerbaan. 2024. X-Wing: general-purpose hybrid post-quantum KEM. Internet-Draft draft-connolly-cfrg-xwing-kem-06. Internet Engineering Task Force. https:\/\/datatracker.ietf.org\/doc\/draft-connolly-cfrg-xwing-kem\/06\/ Work in Progress."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2019.00005"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3319535.3354199"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591272"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","unstructured":"Adam Langley Mike Hamburg and Sean Turner. 2016. Elliptic Curves for Security. RFC 7748. https:\/\/doi.org\/10.17487\/RFC7748","DOI":"10.17487\/RFC7748"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","unstructured":"National Institute of Standards and Technology. 2024. FIPS 203 - Module-Lattice-Based Key-Encapsulation Mechanism Standard. https:\/\/doi.org\/10.6028\/NIST.FIPS.203","DOI":"10.6028\/NIST.FIPS.203"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3134076"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3576915.3616603"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3134043"}],"event":{"name":"CCS '25: ACM SIGSAC Conference on Computer and Communications Security","sponsor":["SIGSAC ACM Special Interest Group on Security, Audit, and Control"],"location":"Taipei Taiwan","acronym":"CCS '25"},"container-title":["Proceedings of the 2025 ACM SIGSAC Conference on Computer and Communications Security"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3719027.3744814","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,12,22]],"date-time":"2025-12-22T22:08:21Z","timestamp":1766441301000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3719027.3744814"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,11,19]]},"references-count":16,"alternative-id":["10.1145\/3719027.3744814","10.1145\/3719027"],"URL":"https:\/\/doi.org\/10.1145\/3719027.3744814","relation":{},"subject":[],"published":{"date-parts":[[2025,11,19]]},"assertion":[{"value":"2025-11-22","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}