{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T01:17:27Z","timestamp":1743124647112,"version":"3.40.3"},"publisher-location":"Cham","reference-count":39,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031870538"},{"type":"electronic","value":"9783031870545"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"DOI":"10.1007\/978-3-031-87054-5_12","type":"book-chapter","created":{"date-parts":[[2025,3,20]],"date-time":"2025-03-20T03:59:02Z","timestamp":1742443142000},"page":"170-186","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Formally Verified Verifiable Group Generators"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0005-9085-4652","authenticated-orcid":false,"given":"Mina A.","family":"Cyrus","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5373-9659","authenticated-orcid":false,"given":"Mukesh","family":"Tiwari","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,3,21]]},"reference":[{"key":"12_CR1","doi-asserted-by":"publisher","unstructured":"Almeida, J.B., et al.: Jasmin: high-assurance and high-speed cryptography. In: Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, CCS 2017, pp. 1807\u20131823. Association for Computing Machinery, New York (2017). https:\/\/doi.org\/10.1145\/3133956.3134078","DOI":"10.1145\/3133956.3134078"},{"key":"12_CR2","doi-asserted-by":"publisher","unstructured":"Almeida, J.B., et al.: Machine-checked proofs for cryptographic standards: indifferentiability of sponge and secure high-assurance implementations of SHA-3. In: Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security, CCS 2019, pp. 1607\u20131622. Association for Computing Machinery, New York (2019). https:\/\/doi.org\/10.1145\/3319535.3363211","DOI":"10.1145\/3319535.3363211"},{"key":"12_CR3","unstructured":"Anand, A., et al.: Certicoq: a verified compiler for coq. In: The Third International Workshop on Coq for Programming Languages (CoqPL) (2017)"},{"key":"12_CR4","doi-asserted-by":"publisher","unstructured":"Annenkov, D., Nielsen, J.B., Spitters, B.: Concert: a smart contract certification framework in coq. In: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (2020). https:\/\/doi.org\/10.1145\/3372885.3373829","DOI":"10.1145\/3372885.3373829"},{"key":"12_CR5","unstructured":"Australian Electoral Commission: Letter to Mr Michael Cordover, LSS4883 Outcome of Internal Review of the Decision to Refuse your FOI Request no. LS4849 (2013). http:\/\/www.aec.gov.au\/information-access\/foi\/2014\/files\/ls4912-1.pdf. Accessed 8 Feb 2022"},{"key":"12_CR6","doi-asserted-by":"crossref","unstructured":"Bayer, S., Groth, J.: Efficient zero-knowledge argument for correctness of a shuffle. In: Annual International Conference on the Theory and Applications of Cryptographic Techniques, pp. 263\u2013280. Springer (2012)","DOI":"10.1007\/978-3-642-29011-4_17"},{"key":"12_CR7","unstructured":"Belenios: Belenios specification (nd). https:\/\/www.belenios.org\/specification.pdf. Accessed 1 Jan 2025"},{"key":"12_CR8","unstructured":"Benaloh, J., Naehrig, M., Pereira, O., Wallach, D.S.: Electionguard: a cryptographic toolkit to enable verifiable elections. Cryptology ePrint Archive (2024)"},{"key":"12_CR9","unstructured":"Beringer, L., Petcher, A., Ye, K.Q., Appel, A.W.: Verified correctness and security of OpenSSL HMAC. In: 24th USENIX Security Symposium (USENIX Security 2015), pp. 207\u2013221. USENIX Association, Washington, D.C. (2015). https:\/\/www.usenix.org\/conference\/usenixsecurity15\/technical-sessions\/presentation\/beringer"},{"key":"12_CR10","doi-asserted-by":"publisher","unstructured":"Blum, M.: Coin flipping by telephone a protocol for solving impossible problems. SIGACT News 15(1), 23\u201327 (1983). https:\/\/doi.org\/10.1145\/1008908.1008911","DOI":"10.1145\/1008908.1008911"},{"issue":"3","key":"12_CR11","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1080\/00029890.1984.11971371","volume":"91","author":"RS Boyer","year":"1984","unstructured":"Boyer, R.S., Moore, J.S.: Proof checking the RSA public key encryption algorithm. Am. Math. Mon. 91(3), 181\u2013189 (1984)","journal-title":"Am. Math. Mon."},{"key":"12_CR12","unstructured":"Boyer, R.S., Moore, J.S.: A Computational Logic. Academic Press (2014)"},{"key":"12_CR13","unstructured":"Burton, D.M.: Elementary Number Theory, 7th edn. McGraw-Hill Education (2010)"},{"key":"12_CR14","doi-asserted-by":"publisher","unstructured":"Chan, H.L., Norrish, M.: A string of pearls: proofs of Fermat\u2019s little theorem. J. Formalized Reason. 6(1), 63\u201387 (2013). https:\/\/doi.org\/10.6092\/issn.1972-5787\/3728. https:\/\/jfr.unibo.it\/article\/view\/3728","DOI":"10.6092\/issn.1972-5787\/3728"},{"key":"12_CR15","doi-asserted-by":"publisher","unstructured":"Chen, Y.F., et al.: Verifying curve25519 software. In: Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security, CCS 2014, pp. 299\u2013309. Association for Computing Machinery, New York (2014). https:\/\/doi.org\/10.1145\/2660267.2660370","DOI":"10.1145\/2660267.2660370"},{"key":"12_CR16","doi-asserted-by":"publisher","unstructured":"Conway, A., Blom, M., Naish, L., Teague, V.: An analysis of new south wales electronic vote counting. In: Proceedings of the Australasian Computer Science Week Multiconference, ACSW 2017. Association for Computing Machinery, New York (2017). https:\/\/doi.org\/10.1145\/3014812.3014837","DOI":"10.1145\/3014812.3014837"},{"key":"12_CR17","doi-asserted-by":"publisher","unstructured":"Erbsen, A., Philipoom, J., Gross, J., Sloan, R., Chlipala, A.: Simple high-level code for cryptographic arithmetic - with proofs, without compromises. In: 2019 IEEE Symposium on Security and Privacy (SP), pp. 1202\u20131219 (2019). https:\/\/doi.org\/10.1109\/SP.2019.00005","DOI":"10.1109\/SP.2019.00005"},{"key":"12_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1007\/978-3-030-51280-4_3","volume-title":"Financial Cryptography and Data Security","author":"P Gaudry","year":"2020","unstructured":"Gaudry, P., Golovnev, A.: Breaking the encryption scheme of the Moscow internet voting system. In: Bonneau, J., Heninger, N. (eds.) FC 2020. LNCS, vol. 12059, pp. 32\u201349. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-51280-4_3"},{"key":"12_CR19","doi-asserted-by":"crossref","unstructured":"Golomb, S.W.: Combinatorial proof of Fermat\u2019s \u201clittle\u201d theorem. Am. Math. Mon. 63(10), 718 (1956)","DOI":"10.2307\/2309563"},{"key":"12_CR20","unstructured":"Haenni, R., Koenig, R.E., Locher, P., Dubuis, E.: Chvote protocol specification. Cryptology ePrint Archive (2017)"},{"key":"12_CR21","doi-asserted-by":"crossref","unstructured":"Haines, T., Gor\u00e9, R., Tiwari, M.: Verified verifiers for verifying elections. In: Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security, pp. 685\u2013702 (2019)","DOI":"10.1145\/3319535.3354247"},{"key":"12_CR22","doi-asserted-by":"crossref","unstructured":"Haines, T., Gor\u00e9, R., Sharma, B.: Did you mix me? Formally verifying verifiable mix nets in electronic voting. In: 2021 IEEE Symposium on Security and Privacy (SP) (2021)","DOI":"10.1109\/SP40001.2021.00033"},{"key":"12_CR23","doi-asserted-by":"publisher","unstructured":"Haines, T., Lewis, S.J., Pereira, O., Teague, V.: How not to prove your election outcome. In: 2020 IEEE Symposium on Security and Privacy (SP), pp. 644\u2013660 (2020). https:\/\/doi.org\/10.1109\/SP40000.2020.00048","DOI":"10.1109\/SP40000.2020.00048"},{"key":"12_CR24","doi-asserted-by":"crossref","unstructured":"Haines, T., Pattinson, D., Tiwari, M.: Verifiable homomorphic tallying for the schulze vote counting scheme. In: Working Conference on Verified Software: Theories, Tools, and Experiments, pp. 36\u201353. Springer (2019)","DOI":"10.1007\/978-3-030-41600-3_4"},{"key":"12_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/978-3-319-22270-7_3","volume-title":"E-Voting and Identity","author":"JA Halderman","year":"2015","unstructured":"Halderman, J.A., Teague, V.: The new south wales iVote System: security failures and verification flaws in a live online election. In: Haenni, R., Koenig, R.E., Wikstr\u00f6m, D. (eds.) VOTELID 2015. LNCS, vol. 9269, pp. 35\u201353. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-22270-7_3"},{"key":"12_CR26","doi-asserted-by":"publisher","unstructured":"Leroy, X.: Formal certification of a compiler back-end or: programming a compiler with a proof assistant. In: Conference Record of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2006, pp. 42\u201354. Association for Computing Machinery, New York (2006). https:\/\/doi.org\/10.1145\/1111037.1111042","DOI":"10.1145\/1111037.1111042"},{"key":"12_CR27","unstructured":"National Institute of Standards and Technology: Digital Signature Standard (DSS) (2013). https:\/\/nvlpubs.nist.gov\/nistpubs\/FIPS\/NIST.FIPS.186-4.pdf. Accessed 8 Feb 2022"},{"key":"12_CR28","unstructured":"National Institute of Standards and Technology: Secure Hash Standard (SHS) (2015). avaliable via https:\/\/nvlpubs.nist.gov\/nistpubs\/FIPS\/NIST.FIPS.180-4.pdf. Accessed 8 Feb 2022"},{"key":"12_CR29","doi-asserted-by":"crossref","unstructured":"Pedersen, T.P.: Non-interactive and information-theoretic secure verifiable secret sharing. In: Annual International Cryptology Conference, pp. 129\u2013140. Springer (1991)","DOI":"10.1007\/3-540-46766-1_9"},{"key":"12_CR30","doi-asserted-by":"publisher","unstructured":"Schnorr, C.P.: Efficient signature generation by smart cards. J. Cryptol. 4(3), 161\u2013174 (1991). https:\/\/doi.org\/10.1007\/BF00196725","DOI":"10.1007\/BF00196725"},{"key":"12_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1007\/978-3-540-71067-7_6","volume-title":"Theorem Proving in Higher Order Logics","author":"K Slind","year":"2008","unstructured":"Slind, K., Norrish, M.: A brief overview of HOL4. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 28\u201332. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-71067-7_6"},{"key":"12_CR32","doi-asserted-by":"publisher","unstructured":"Sozeau, M., Boulier, S., Forster, Y., Tabareau, N., Winterhalter, T.: Coq coq correct! verification of type checking and erasure for coq, in coq. Proc. ACM Program. Lang. 4(POPL) (2019). https:\/\/doi.org\/10.1145\/3371076","DOI":"10.1145\/3371076"},{"key":"12_CR33","unstructured":"Specter, M., Halderman, J.A.: Security analysis of the democracy live online voting system. In: 30th USENIX Security Symposium (USENIX Security 2021), pp. 3077\u20133092. USENIX Association (2021). https:\/\/www.usenix.org\/conference\/usenixsecurity21\/presentation\/specter-security"},{"key":"12_CR34","unstructured":"Specter, M.A., Koppel, J., Weitzner, D.: The ballot is busted before the blockchain: a security analysis of Voatz, the first internet voting application used in U.S. federal elections. In: 29th USENIX Security Symposium (USENIX Security 2020), pp. 1535\u20131553. USENIX Association (2020). https:\/\/www.usenix.org\/conference\/usenixsecurity20\/presentation\/specter"},{"key":"12_CR35","doi-asserted-by":"publisher","unstructured":"Team, T.C.D.: The coq proof assistant, version 8.10.0 (2019). https:\/\/doi.org\/10.5281\/zenodo.3476303","DOI":"10.5281\/zenodo.3476303"},{"key":"12_CR36","doi-asserted-by":"publisher","unstructured":"Team, T.C.D.: The coq proof assistant, version 8.15.0 (2022). https:\/\/doi.org\/10.5281\/zenodo.1003420. https:\/\/zenodo.org\/record\/1003420","DOI":"10.5281\/zenodo.1003420"},{"key":"12_CR37","doi-asserted-by":"crossref","unstructured":"Th\u00e9ry, L., Hanrot, G.: Primality proving with elliptic curves. In: Schneider, K., Brandt, J. (eds.) Theorem Proving in Higher Order Logics, pp. 319\u2013333. Springer, Heidelberg (2007)","DOI":"10.1007\/978-3-540-74591-4_24"},{"key":"12_CR38","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/0890-5401(88)90005-3","volume":"76","author":"C Thierry","year":"1988","unstructured":"Thierry, C., G\u00e9rard, H.: The calculus of constructions. Inf. Comput. 76, 95\u2013120 (1988)","journal-title":"Inf. Comput."},{"key":"12_CR39","doi-asserted-by":"publisher","unstructured":"Zinzindohou\u00e9, J.K., Bhargavan, K., Protzenko, J., Beurdouche, B.: HACL*: a verified modern cryptographic library. In: Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, CCS 2017, pp. 1789\u20131806. Association for Computing Machinery, New York (2017). https:\/\/doi.org\/10.1145\/3133956.3134043","DOI":"10.1145\/3133956.3134043"}],"container-title":["Lecture Notes in Computer Science","Fundamentals of Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-87054-5_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,20]],"date-time":"2025-03-20T03:59:25Z","timestamp":1742443165000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-87054-5_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031870538","9783031870545"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-87054-5_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"21 March 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FSEN","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Fundamentals of Software Engineering","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"V\u00e4ster\u00e5s","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Sweden","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 April 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 April 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fsen2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conf.researchr.org\/home\/fsen-2025","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}