{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,23]],"date-time":"2025-12-23T00:28:49Z","timestamp":1766449729901,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":30,"publisher":"ACM","license":[{"start":{"date-parts":[[2017,10,30]],"date-time":"2017-10-30T00:00:00Z","timestamp":1509321600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100004663","name":"Ministry of Science and Technology, Taiwan","doi-asserted-by":"publisher","award":["103-2221-E-001-020-MY3,105-2221-E-001-014-MY3"],"award-info":[{"award-number":["103-2221-E-001-020-MY3,105-2221-E-001-014-MY3"]}],"id":[{"id":"10.13039\/501100004663","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2017,10,30]]},"DOI":"10.1145\/3133956.3134076","type":"proceedings-article","created":{"date-parts":[[2017,10,27]],"date-time":"2017-10-27T12:48:18Z","timestamp":1509108498000},"page":"1973-1987","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":16,"title":["Certified Verification of Algebraic Properties on Low-Level Mathematical Constructs in Cryptographic Programs"],"prefix":"10.1145","author":[{"given":"Ming-Hsien","family":"Tsai","sequence":"first","affiliation":[{"name":"Academia Sinica, Taipei, Taiwan Roc"}]},{"given":"Bow-Yaw","family":"Wang","sequence":"additional","affiliation":[{"name":"Academia Sinica, Taipei, Taiwan Roc"}]},{"given":"Bo-Yin","family":"Yang","sequence":"additional","affiliation":[{"name":"Academia Sinica, Taipei, Taiwan Roc"}]}],"member":"320","published-online":{"date-parts":[[2017,10,30]]},"reference":[{"key":"e_1_3_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11334-013-0195-x"},{"key":"e_1_3_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-77505-8_27"},{"key":"e_1_3_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2011.07.003"},{"key":"e_1_3_2_2_4_1","doi-asserted-by":"publisher","unstructured":"B. Alpern M. N. Wegman and F. K. Zadeck. 1988. Detecting Equality of Variables in Programs. In POPL. ACM New York NY USA 1--11. 10.1145\/73560.73561","DOI":"10.1145\/73560.73561"},{"key":"e_1_3_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2701415"},{"key":"e_1_3_2_2_6_1","volume-title":"Verified Correctness and Security of OpenSSL HMAC. In USENIX Security Symposium","author":"Beringer Lennart","year":"2015","unstructured":"Lennart Beringer, Adam Petcher, Katherine Q. Ye, and Andrew W. Appel. 2015. Verified Correctness and Security of OpenSSL HMAC. In USENIX Security Symposium 2015. USENIX Association, 207--221."},{"key":"e_1_3_2_2_7_1","unstructured":"Daniel J. Bernstein. 2005. Cache Timing Attacks on AES. (2005). https:\/\/cr.yp.to\/ antiforgery\/cachetiming-20050414.pdf."},{"key":"e_1_3_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/11745853_14"},{"key":"e_1_3_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-23951-9_9"},{"key":"e_1_3_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/s13389-012-0027-1"},{"key":"e_1_3_2_2_11_1","volume-title":"Bernstein and Peter Schwabe","author":"Daniel","year":"2016","unstructured":"Daniel J. Bernstein and Peter Schwabe. 2016. gfverif: Fast and Easy Verification of Finite-Field Arithmetic. (2016). http:\/\/gfverif.cryptojedi.org."},{"key":"e_1_3_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5"},{"key":"e_1_3_2_2_13_1","volume-title":"Vale: Verifying High-Performance Cryptographic Assembly Code. In USENIX Security Symposium","author":"Bond B.","year":"2017","unstructured":"B. Bond, C. Hawblitzel, M. Kapritsos, K. R. M. Leino, J. R. Lorch, B. Parno, A. Rane, S. Setty, and L. Thompson. 2017. Vale: Verifying High-Performance Cryptographic Assembly Code. In USENIX Security Symposium 2017. USENIX Association, 917--934."},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","unstructured":"Yu-Fang Chen Chang-Hong Hsu Hsin-Hung Lin Peter Schwabe Ming-Hsien Tsai Bow-Yaw Wang Bo-Yin Yang and Shang-Yi Yang. 2014. Verifying Curve25519 Software. In CCS. ACM 299--309. https:\/\/doi.org\/10.1145\/2660267. 2660370","DOI":"10.1145\/2660267"},{"key":"e_1_3_2_2_15_1","volume-title":"A Course in Computational Algebraic Number Theory","author":"Cohen Henri","unstructured":"Henri Cohen. 1996. A Course in Computational Algebraic Number Theory (3rd ed.). GTM, Vol. 138. Springer.","edition":"3"},{"key":"e_1_3_2_2_16_1","unstructured":"The Sage Developers. 2017. SageMath the Sage Mathematics Software System. (2017). http:\/\/www.sagemath.org."},{"key":"e_1_3_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63390-9_7"},{"key":"e_1_3_2_2_18_1","unstructured":"everest 2016. Project Everest. https:\/\/project-everest.github.io. (2016). Accessed: 2017-05--19."},{"key":"e_1_3_2_2_19_1","unstructured":"fiat 2015. Fiat-Crypto. https:\/\/github.com\/mit-plv\/fiat-crypto. (2015). Accessed: 2017-05--19."},{"key":"e_1_3_2_2_20_1","volume-title":"Johnson","author":"Garey Michael R.","year":"1979","unstructured":"Michael R. Garey and David S. Johnson. 1979. Computers and Intractability: A Guide to the Theory of NP-Completeness. W. H. Freeman and company."},{"key":"e_1_3_2_2_21_1","volume-title":"A Singular Introduction to Commutative Algebra","author":"Greuel Gert-Martin","unstructured":"Gert-Martin Greuel and Gerhard Pfister. 2008. A Singular Introduction to Commutative Algebra (2nd ed.). Springer.","edition":"2"},{"key":"e_1_3_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73595-3_5"},{"key":"e_1_3_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_3_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45146-4_14"},{"key":"e_1_3_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1090\/S0025-5718-1987-0866113-7"},{"key":"e_1_3_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978--3--319-03545--1_5"},{"key":"e_1_3_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71209-1_44"},{"key":"e_1_3_2_2_28_1","unstructured":"Lo\u00efc Pottier. 2008. Connecting Gr\u00f6bner Bases Programs with Coq to do Proofs in Algebra Geometry and Arithmetics. In Knowledge Exchange: Automated Provers and Proof Assistants G. Sutcliffe P. Rudnicki R. Schmidt B. Konev and S. Schulz (Eds.). 418."},{"key":"e_1_3_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/MSP.2016.125"},{"key":"e_1_3_2_2_31_1","unstructured":"Wikipedia. 2017. Curve25519. https:\/\/en.wikipedia.org\/wiki\/Curve25519. (2017). Accessed: 2017-05-19."}],"event":{"name":"CCS '17: 2017 ACM SIGSAC Conference on Computer and Communications Security","sponsor":["SIGSAC ACM Special Interest Group on Security, Audit, and Control"],"location":"Dallas Texas USA","acronym":"CCS '17"},"container-title":["Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3133956.3134076","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3133956.3134076","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:11:03Z","timestamp":1750212663000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3133956.3134076"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,10,30]]},"references-count":30,"alternative-id":["10.1145\/3133956.3134076","10.1145\/3133956"],"URL":"https:\/\/doi.org\/10.1145\/3133956.3134076","relation":{},"subject":[],"published":{"date-parts":[[2017,10,30]]},"assertion":[{"value":"2017-10-30","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}