{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,6]],"date-time":"2026-06-06T03:48:26Z","timestamp":1780717706601,"version":"3.54.1"},"publisher-location":"New York, NY, USA","reference-count":37,"publisher":"ACM","license":[{"start":{"date-parts":[[2014,11,3]],"date-time":"2014-11-03T00:00:00Z","timestamp":1414972800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100003246","name":"Nederlandse Organisatie voor Wetenschappelijk Onderzoek","doi-asserted-by":"publisher","award":["Veni 2013 project 13114"],"award-info":[{"award-number":["Veni 2013 project 13114"]}],"id":[{"id":"10.13039\/501100003246","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001869","name":"Academia Sinica","doi-asserted-by":"publisher","award":["IIS Specialty Project and Career Advancement Award of BY Yang"],"award-info":[{"award-number":["IIS Specialty Project and Career Advancement Award of BY Yang"]}],"id":[{"id":"10.13039\/501100001869","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100004663","name":"Ministry of Science and Technology, Taiwan","doi-asserted-by":"publisher","award":["102-2221-E-001-018\/-017 103-2221-E-001-019\/020-MY3"],"award-info":[{"award-number":["102-2221-E-001-018\/-017 103-2221-E-001-019\/020-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":[[2014,11,3]]},"DOI":"10.1145\/2660267.2660370","type":"proceedings-article","created":{"date-parts":[[2014,11,11]],"date-time":"2014-11-11T13:40:05Z","timestamp":1415713205000},"page":"299-309","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":37,"title":["Verifying Curve25519 Software"],"prefix":"10.1145","author":[{"given":"Yu-Fang","family":"Chen","sequence":"first","affiliation":[{"name":"Academia Sinica, Taipei, Taiwan Roc"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Chang-Hong","family":"Hsu","sequence":"additional","affiliation":[{"name":"University of Michigan, Ann Arbor, MI, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Hsin-Hung","family":"Lin","sequence":"additional","affiliation":[{"name":"Kyushu University, Fukuoka, Japan"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Peter","family":"Schwabe","sequence":"additional","affiliation":[{"name":"Radboud University Nijmegen, Nijmegen, Netherlands"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ming-Hsien","family":"Tsai","sequence":"additional","affiliation":[{"name":"Academia Sinica, Taipei, Taiwan Roc"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Bow-Yaw","family":"Wang","sequence":"additional","affiliation":[{"name":"Academia Sinica, Taipei, Taiwan Roc"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Bo-Yin","family":"Yang","sequence":"additional","affiliation":[{"name":"Academia Sinica, Taipei, Taiwan Roc"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Shang-Yi","family":"Yang","sequence":"additional","affiliation":[{"name":"Academia Sinica, Taipei, Taiwan Roc"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2014,11,3]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11334-013-0195-x"},{"key":"e_1_3_2_1_2_1","series-title":"Lecture Notes in Computer Science","first-page":"346","volume-title":"Advances in Computer Science -- ASIAN","author":"Affeldt R.","year":"2006","unstructured":"R. Affeldt and N. Marti . An approach to formal verification of arithmetic functions in assembly . In M. Okada and I. Satoh, editors, Advances in Computer Science -- ASIAN 2006 , volume 4435 of Lecture Notes in Computer Science , pages 346 -- 360 . Springer-Verlag Berlin Heidelberg , 2007. https:\/\/staff.aist.go.jp\/reynald.affeldt\/documents\/affeldt-asian2006.pdf. R. Affeldt and N. Marti. An approach to formal verification of arithmetic functions in assembly. In M. Okada and I. Satoh, editors, Advances in Computer Science -- ASIAN 2006, volume 4435 of Lecture Notes in Computer Science, pages 346--360. Springer-Verlag Berlin Heidelberg, 2007. https:\/\/staff.aist.go.jp\/reynald.affeldt\/documents\/affeldt-asian2006.pdf."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2011.07.003"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2508859.2516652"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/73560.73561"},{"key":"e_1_3_2_1_6_1","volume-title":"Handbook of Elliptic and Hyperelliptic Curve Cryptography","author":"Avanzi R.","year":"2006","unstructured":"R. Avanzi , H. Cohen , C. Doche , G. Frey , T. Lange , K. Nguyen , and F. Vercauteren . Handbook of Elliptic and Hyperelliptic Curve Cryptography . Chapman & Hall\/CRC , 2006 . R. Avanzi, H. Cohen, C. Doche, G. Frey, T. Lange, K. Nguyen, and F. Vercauteren. Handbook of Elliptic and Hyperelliptic Curve Cryptography. Chapman & Hall\/CRC, 2006."},{"key":"e_1_3_2_1_7_1","volume-title":"Universite de Vincennes-Saint Denis { Paris VIII","author":"Bartzia E.-I.","year":"2011","unstructured":"E.-I. Bartzia . Formalisation des courbes elliptiques en coq. Master's thesis , Universite de Vincennes-Saint Denis { Paris VIII , 2011 . http:\/\/pierre-yves.strub.nu\/research\/ec\/. E.-I. Bartzia. Formalisation des courbes elliptiques en coq. Master's thesis, Universite de Vincennes-Saint Denis { Paris VIII, 2011. http:\/\/pierre-yves.strub.nu\/research\/ec\/."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40349-1_17"},{"key":"e_1_3_2_1_9_1","unstructured":"D. J. Bernstein. qhasm: tools to help write high-speed software. http:\/\/cr.yp.to\/qhasm.html.  D. J. Bernstein. qhasm: tools to help write high-speed software. http:\/\/cr.yp.to\/qhasm.html."},{"key":"e_1_3_2_1_10_1","unstructured":"D. J. Bernstein. Supercop: System for unified performance evaluation related to cryptographic operations and primitives. http:\/\/bench.cr.yp.to\/supercop.html. Published as part of ECRYPT II VAMPIRE Lab.  D. J. Bernstein. Supercop: System for unified performance evaluation related to cryptographic operations and primitives. http:\/\/bench.cr.yp.to\/supercop.html. Published as part of ECRYPT II VAMPIRE Lab."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/11745853_14"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03356-8_19"},{"key":"e_1_3_2_1_13_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"124","DOI":"10.1007\/978-3-642-23951-9_9","volume-title":"Cryptographic Hardware and Embedded Systems -- CHES","author":"Bernstein D. J.","year":"2011","unstructured":"D. J. Bernstein , N. Duif , T. Lange , P. Schwabe , and B.-Y. Yang . High-speed high-security signatures . In B. Preneel and T. Takagi, editors, Cryptographic Hardware and Embedded Systems -- CHES 2011 , volume 6917 of Lecture Notes in Computer Science , pages 124 -- 142 . Springer-Verlag Berlin Heidelberg , 2011. see also full version {14}. D. J. Bernstein, N. Duif, T. Lange, P. Schwabe, and B.-Y. Yang. High-speed high-security signatures. In B. Preneel and T. Takagi, editors, Cryptographic Hardware and Embedded Systems -- CHES 2011, volume 6917 of Lecture Notes in Computer Science, pages 124--142. Springer-Verlag Berlin Heidelberg, 2011. see also full version {14}."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/s13389-012-0027-1"},{"key":"e_1_3_2_1_15_1","unstructured":"D. J. Bernstein and T. L. (editors). eBACS: ECRYPT Benchmarking of Cryptographic Systems. http:\/\/bench.cr.yp.to (accessed May 17 2014).  D. J. Bernstein and T. L. (editors). eBACS: ECRYPT Benchmarking of Cryptographic Systems. http:\/\/bench.cr.yp.to (accessed May 17 2014)."},{"key":"e_1_3_2_1_16_1","unstructured":"D. J. Bernstein and T. L. (editors). Explicit-formulas database. http:\/\/www.hyperelliptic.org\/EFD\/ (accessed May 17 2014).  D. J. Bernstein and T. L. (editors). Explicit-formulas database. http:\/\/www.hyperelliptic.org\/EFD\/ (accessed May 17 2014)."},{"key":"e_1_3_2_1_17_1","volume-title":"TweetNaCl: A crypto library in 100 tweets","author":"Bernstein D. J.","year":"2013","unstructured":"D. J. Bernstein , W. Janssen , T. Lange , and P. Schwabe . TweetNaCl: A crypto library in 100 tweets , 2013 . http:\/\/cryptojedi.org\/papers\/#tweetnacl. D. J. Bernstein, W. Janssen, T. Lange, and P. Schwabe. TweetNaCl: A crypto library in 100 tweets, 2013. http:\/\/cryptojedi.org\/papers\/#tweetnacl."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33481-8_9"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development Coq'Art: The Calculus of Inductive Constructions","author":"Bertot Y.","year":"2004","unstructured":"Y. Bertot and P. Cast--eran . Interactive Theorem Proving and Program Development Coq'Art: The Calculus of Inductive Constructions . EATCS. Springer , 2004 . Y. Bertot and P. Cast--eran. Interactive Theorem Proving and Program Development Coq'Art: The Calculus of Inductive Constructions. EATCS. Springer, 2004."},{"key":"e_1_3_2_1_20_1","volume-title":"miTLS: A verified reference TLS implementation","author":"Bhargavan K.","year":"2014","unstructured":"K. Bhargavan , A. Delignat-Lavaud , C. Fournet , M. Kohlweiss , A. Pironti , P.-Y. Strub , and S. Zanella-Beguelin . miTLS: A verified reference TLS implementation , 2014 . http:\/\/www.mitls.org\/wsgi\/home. K. Bhargavan, A. Delignat-Lavaud, C. Fournet, M. Kohlweiss, A. Pironti, P.-Y. Strub, and S. Zanella-Beguelin. miTLS: A verified reference TLS implementation, 2014. http:\/\/www.mitls.org\/wsgi\/home."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2013.37"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-27954-6_11"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00768-2_16"},{"key":"e_1_3_2_1_24_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1007\/978-3-642-55220-5_11","volume-title":"Advances in Cryptology -- EUROCRYPT","author":"Costello C.","year":"2014","unstructured":"C. Costello , H. Hisil , and B. Smith . Faster compact diffie--hellman: Endomorphisms on the x-line . In P. Q. Nguyen and E. Oswald, editors, Advances in Cryptology -- EUROCRYPT 2014 , volume 8441 of Lecture Notes in Computer Science , pages 183 -- 200 . Springer-Verlag Berlin Heidelberg , 2014. http:\/\/eprint.iacr.org\/2013\/692\/. C. Costello, H. Hisil, and B. Smith. Faster compact diffie--hellman: Endomorphisms on the x-line. In P. Q. Nguyen and E. Oswald, editors, Advances in Cryptology -- EUROCRYPT 2014, volume 8441 of Lecture Notes in Computer Science, pages 183--200. Springer-Verlag Berlin Heidelberg, 2014. http:\/\/eprint.iacr.org\/2013\/692\/."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2007.01.015"},{"key":"e_1_3_2_1_26_1","unstructured":"M. Gordon. CryptVer project. http:\/\/www.cl.cam.ac.uk\/~mjcg\/proposals\/CryptVer\/.  M. Gordon. CryptVer project. http:\/\/www.cl.cam.ac.uk\/~mjcg\/proposals\/CryptVer\/."},{"key":"e_1_3_2_1_27_1","volume-title":"Guide to Elliptic Curve Cryptography","author":"Hankerson D.","year":"2004","unstructured":"D. Hankerson , A. Menezes , and S. A. Vanstone . Guide to Elliptic Curve Cryptography . Springer-Verlag New York , 2004 . D. Hankerson, A. Menezes, and S. A. Vanstone. Guide to Elliptic Curve Cryptography. Springer-Verlag New York, 2004."},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-34961-4_43"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/11734727_14"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1090\/S0025-5718-1987-0866113-7"},{"key":"e_1_3_2_1_32_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"568","DOI":"10.1007\/978-3-540-71209-1_44","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Myreen M. O.","year":"2007","unstructured":"M. O. Myreen and M. J. C. Gordon . Hoare logic for realistically modelled machine code . In O. Grumberg and M. Huth, editors, Tools and Algorithms for the Construction and Analysis of Systems , volume 4424 of Lecture Notes in Computer Science , pages 568 -- 582 . Springer-Verlag Berlin Heidelberg , 2007 . http: \/\/www.cl.cam.ac.uk\/~mom22\/mc-hoare-logic.pdf. M. O. Myreen and M. J. C. Gordon. Hoare logic for realistically modelled machine code. In O. Grumberg and M. Huth, editors, Tools and Algorithms for the Construction and Analysis of Systems, volume 4424 of Lecture Notes in Computer Science, pages 568--582. Springer-Verlag Berlin Heidelberg, 2007. http: \/\/www.cl.cam.ac.uk\/~mom22\/mc-hoare-logic.pdf."},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40349-1_18"},{"key":"e_1_3_2_1_34_1","volume-title":"News article on CSO","author":"Ragan S.","year":"2014","unstructured":"S. Ragan . Bugcrowd launches funding drive to audit popenssl. News article on CSO , 2014 . http:\/\/www.csoonline.com\/article\/2145020\/security-industry\/ bugcrowd-launches-funding-drive-to-audit-openssl. html (accessed May 17, 2014). S. Ragan. Bugcrowd launches funding drive to audit popenssl. News article on CSO, 2014. http:\/\/www.csoonline.com\/article\/2145020\/security-industry\/ bugcrowd-launches-funding-drive-to-audit-openssl. html (accessed May 17, 2014)."},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/73560.73562"},{"key":"e_1_3_2_1_36_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1007\/978-3-540-74591-4_24","volume-title":"Theorem Proving in Higher Order Logics","author":"Thery L.","year":"2007","unstructured":"L. Thery and G. Hanrot . Primality proving with elliptic curves . In K. Schneider and J. Brandt, editors, Theorem Proving in Higher Order Logics , volume 4732 of Lecture Notes in Computer Science , pages 319 -- 333 . Springer-Verlag Berlin Heidelberg , 2007 . http:\/\/hal.inria.fr\/docs\/00\/14\/06\/58\/PDF\/paper.pdf. L. Thery and G. Hanrot. Primality proving with elliptic curves. In K. Schneider and J. Brandt, editors, Theorem Proving in Higher Order Logics, volume 4732 of Lecture Notes in Computer Science, pages 319--333. Springer-Verlag Berlin Heidelberg, 2007. http:\/\/hal.inria.fr\/docs\/00\/14\/06\/58\/PDF\/paper.pdf."},{"key":"e_1_3_2_1_37_1","volume-title":"IsTrueCryptAuditedYet? http:\/\/istruecryptauditedyet.com\/ (accessed","author":"White K.","year":"2014","unstructured":"K. White and M. Green . IsTrueCryptAuditedYet? http:\/\/istruecryptauditedyet.com\/ (accessed May 17, 2014 ). K. White and M. Green. IsTrueCryptAuditedYet? http:\/\/istruecryptauditedyet.com\/ (accessed May 17, 2014)."}],"event":{"name":"CCS'14: 2014 ACM SIGSAC Conference on Computer and Communications Security","location":"Scottsdale Arizona USA","acronym":"CCS'14","sponsor":["SIGSAC ACM Special Interest Group on Security, Audit, and Control"]},"container-title":["Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2660267.2660370","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2660267.2660370","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T06:13:40Z","timestamp":1750227220000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2660267.2660370"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,11,3]]},"references-count":37,"alternative-id":["10.1145\/2660267.2660370","10.1145\/2660267"],"URL":"https:\/\/doi.org\/10.1145\/2660267.2660370","relation":{},"subject":[],"published":{"date-parts":[[2014,11,3]]},"assertion":[{"value":"2014-11-03","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}