{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T05:40:08Z","timestamp":1743140408005,"version":"3.40.3"},"publisher-location":"Cham","reference-count":41,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030616373"},{"type":"electronic","value":"9783030616380"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"DOI":"10.1007\/978-3-030-61638-0_1","type":"book-chapter","created":{"date-parts":[[2020,10,13]],"date-time":"2020-10-13T23:08:28Z","timestamp":1602630508000},"page":"3-23","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Towards a Formally Verified Implementation of the MimbleWimble Cryptocurrency Protocol"],"prefix":"10.1007","author":[{"given":"Gustavo","family":"Betarte","sequence":"first","affiliation":[]},{"given":"Maximiliano","family":"Cristi\u00e1","sequence":"additional","affiliation":[]},{"given":"Carlos","family":"Luna","sequence":"additional","affiliation":[]},{"given":"Adri\u00e1n","family":"Silveira","sequence":"additional","affiliation":[]},{"given":"Dante","family":"Zanarini","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2020,10,14]]},"reference":[{"key":"1_CR1","doi-asserted-by":"publisher","DOI":"10.21236\/AD0772806","volume-title":"Computer Security technology planning study","author":"J Anderson","year":"1972","unstructured":"Anderson, J.: Computer Security technology planning study. Technical report, Deputy for Command and Management System, USA (1972)"},{"key":"1_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/978-3-319-10082-1_6","volume-title":"Foundations of Security Analysis and Design VII","author":"G Barthe","year":"2014","unstructured":"Barthe, G., Dupressoir, F., Gr\u00e9goire, B., Kunz, C., Schmidt, B., Strub, P.-Y.: EasyCrypt: a tutorial. In: Aldini, A., Lopez, J., Martinelli, F. (eds.) FOSAD 2012-2013. LNCS, vol. 8604, pp. 146\u2013166. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-10082-1_6"},{"key":"1_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/978-3-319-08970-6_6","volume-title":"Interactive Theorem Proving","author":"E-I Bartzia","year":"2014","unstructured":"Bartzia, E.-I., Strub, P.-Y.: A formal library for elliptic curves in the coq proof assistant. In: Klein, G., Gamboa, R. (eds.) ITP 2014. LNCS, vol. 8558, pp. 77\u201392. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08970-6_6"},{"key":"1_CR4","unstructured":"Bell, D.E., LaPadula, L.J.: Secure computer systems: Mathematical foundations. Technical report MTR-2547, vol. 1, MITRE Corp., Bedford, MA (1973)"},{"key":"1_CR5","unstructured":"Bertot, Y., Cast\u00e9ran, P., (informaticien) Huet, G., Paulin-Mohring, C.: Interactive theorem proving and program development: Coq\u2019Art : the calculus of inductive constructions. Texts in theoretical computer science. Springer, Berlin, New York (2004). Donn\u00e9es compl\u00e9mentaires http:\/\/coq.inria.fr"},{"key":"1_CR6","unstructured":"Betarte, G., Cristi\u00e1, M., Luna, C., Silveira, A., Zanarini, D.: Set-based models for cryptocurrency software. CoRR, abs\/1908.00591 (2019)"},{"key":"1_CR7","doi-asserted-by":"crossref","unstructured":"Betarte, G., Cristi\u00e1, M., Luna, C., Silveira, A., Zanarini, D.: Towards a formally verified implementation of the mimblewimble cryptocurrency protocol. CoRR, abs\/1907.01688 (2019)","DOI":"10.1007\/978-3-030-61638-0_1"},{"key":"1_CR8","doi-asserted-by":"crossref","unstructured":"Bhargavan, K., et al.: Formal verification of smart contracts: short paper. In: Proceedings of the 2016 ACM Workshop on Programming Languages and Analysis for Security, PLAS 2016, pp. 91\u201396. ACM, New York (2016)","DOI":"10.1145\/2993600.2993611"},{"key":"1_CR9","doi-asserted-by":"crossref","unstructured":"Blanchet, B.: CryptoVerif: a computationally sound mechanized prover for cryptographic protocols. In Dagstuhl seminar \u201cFormal Protocol Verification Applied\u201d, October 2007","DOI":"10.1109\/SP.2006.1"},{"key":"1_CR10","unstructured":"Blanchet, B.: An efficient cryptographic protocol verifier based on prolog rules. In: 14th IEEE Computer Security Foundations Workshop (CSFW-14 2001), 11\u201313 June 2001, Cape Breton, Nova Scotia, Canada, pp. 82\u201396. IEEE Computer Society (2001)"},{"key":"1_CR11","unstructured":"Buterin, V.: Critical update re: Dao vulnerability, June 2016"},{"key":"1_CR12","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1007\/978-3-319-63046-5_12","volume-title":"Automated Deduction \u2013 CADE 26","author":"M Cristi\u00e1","year":"2017","unstructured":"Cristi\u00e1, M., Rossi, G.: A decision procedure for restricted intensional sets. In: de Moura, L. (ed.) CADE 2017. LNCS (LNAI), vol. 10395, pp. 185\u2013201. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63046-5_12"},{"key":"1_CR13","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1007\/s10817-019-09520-4","volume":"64","author":"M Cristi\u00e1","year":"2019","unstructured":"Cristi\u00e1, M., Rossi, G.: Solving quantifier-free first-order constraints over finite sets and binary relations. J. Automated Reasoning 64, 295\u2013330 (2019). https:\/\/doi.org\/10.1007\/s10817-019-09520-4","journal-title":"J. Automated Reasoning"},{"key":"1_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1007\/978-3-642-40561-7_16","volume-title":"Software Engineering and Formal Methods","author":"M Cristi\u00e1","year":"2013","unstructured":"Cristi\u00e1, M., Rossi, G., Frydman, C.: log as a test case generator for the test template framework. In: Hierons, R.M., Merayo, M.G., Bravetti, M. (eds.) SEFM 2013. LNCS, vol. 8137, pp. 229\u2013243. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-40561-7_16"},{"key":"1_CR15","unstructured":"D\u00e9n\u00e8s, M., Hritcu, C., Lampropoulos, L., Paraskevopoulou, Z., Pierce, B.: Quickchick: Property-based testing for coq. In: The Coq Workshop (2014)"},{"key":"1_CR16","unstructured":"Korsell, E., Mueller, P., Schumann, Y.: Spectrecoin. https:\/\/spectreproject.io\/Spectrecoin_White-Paper.pdf , June 2019"},{"key":"1_CR17","doi-asserted-by":"crossref","unstructured":"Fanti, G.C., et al.: Dandelion++: lightweight cryptocurrency networking with formal anonymity guarantees. CoRR, abs\/1805.11060 (2018)","DOI":"10.1145\/3219617.3219620"},{"key":"1_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"657","DOI":"10.1007\/978-3-030-17653-2_22","volume-title":"Advances in Cryptology \u2013 EUROCRYPT 2019","author":"G Fuchsbauer","year":"2019","unstructured":"Fuchsbauer, G., Orr\u00f9, M., Seurin, Y.: Aggregate cash systems: a cryptographic investigation of mimblewimble. In: Ishai, Y., Rijmen, V. (eds.) EUROCRYPT 2019. LNCS, vol. 11476, pp. 657\u2013689. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17653-2_22"},{"key":"1_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/978-3-662-46803-6_10","volume-title":"Advances in Cryptology - EUROCRYPT 2015","author":"J Garay","year":"2015","unstructured":"Garay, J., Kiayias, A., Leonardos, N.: The bitcoin backbone protocol: analysis and applications. In: Oswald, E., Fischlin, M. (eds.) EUROCRYPT 2015. LNCS, vol. 9057, pp. 281\u2013310. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46803-6_10"},{"key":"1_CR20","unstructured":"Gibson, A.: An investigation into confidential transactions (2018). https:\/\/github.com\/AdamISZ\/ConfidentialTransactionsDoc\/blob\/master\/essayonCT.pdf"},{"key":"1_CR21","unstructured":"Grin Community. Grin: Open Research Problems (2020). https:\/\/grin.mw\/open-research-problems"},{"key":"1_CR22","unstructured":"Grin Team. Privacy Primer, November 2018. https:\/\/github.com\/mimblewimble\/docs\/wiki\/Grin-Privacy-Primer"},{"key":"1_CR23","unstructured":"Grin Team. Dandelion++ in Grin: Privacy-Preserving Transaction Aggregation and Propagation, July 2019. https:\/\/github.com\/mimblewimble\/grin\/blob\/master\/doc\/dandelion\/dandelion.md"},{"key":"1_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/978-3-319-89722-6_10","volume-title":"Principles of Security and Trust","author":"I Grishchenko","year":"2018","unstructured":"Grishchenko, I., Maffei, M., Schneidewind, C.: A semantic framework for the security analysis of ethereum smart contracts. In: Bauer, L., K\u00fcsters, R. (eds.) POST 2018. LNCS, vol. 10804, pp. 243\u2013269. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89722-6_10"},{"key":"1_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"520","DOI":"10.1007\/978-3-319-70278-0_33","volume-title":"Financial Cryptography and Data Security","author":"Y Hirai","year":"2017","unstructured":"Hirai, Y.: Defining the ethereum virtual machine for interactive theorem provers. In: Brenner, M., et al. (eds.) FC 2017. LNCS, vol. 10323, pp. 520\u2013535. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-70278-0_33"},{"key":"1_CR26","unstructured":"Miers, I.: Blockchain Privacy: Equal Parts Theory and Practice, February 2019. https:\/\/www.zfnd.org\/blog\/blockchain-privacy\/#flashlight"},{"key":"1_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/978-3-319-42019-6_11","volume-title":"Rule Technologies. Research, Tools, and Applications","author":"F Idelberger","year":"2016","unstructured":"Idelberger, F., Governatori, G., Riveret, R., Sartor, G.: Evaluation of logic-based smart contracts for blockchain systems. In: Alferes, J.J.J., Bertossi, L., Governatori, G., Fodor, P., Roman, D. (eds.) RuleML 2016. LNCS, vol. 9718, pp. 167\u2013183. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-42019-6_11"},{"key":"1_CR28","unstructured":"Jedusor, T.: Introduction to MimbleWimble and Grin (2016). https:\/\/github.com\/mimblewimble\/grin\/blob\/master\/doc\/intro.md"},{"key":"1_CR29","unstructured":"Jedusor, T.: Mimblewimble (2016). scalingbitcoin.org\/papers\/mimblewimble.txt"},{"key":"1_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1007\/978-3-319-63688-7_12","volume-title":"Advances in Cryptology \u2013 CRYPTO 2017","author":"A Kiayias","year":"2017","unstructured":"Kiayias, A., Russell, A., David, B., Oliynykov, R.: Ouroboros: a provably secure proof-of-stake blockchain protocol. In: Katz, J., Shacham, H. (eds.) CRYPTO 2017. LNCS, vol. 10401, pp. 357\u2013388. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63688-7_12"},{"key":"1_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/3-540-39185-1_12","volume-title":"Types for Proofs and Programs","author":"P Letouzey","year":"2003","unstructured":"Letouzey, P.: A new extraction for coq. In: Geuvers, H., Wiedijk, F. (eds.) TYPES 2002. LNCS, vol. 2646, pp. 200\u2013219. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/3-540-39185-1_12"},{"key":"1_CR32","unstructured":"Luu, L., Chu, D., Olickel, H., Saxena, P., Hobor, A.: Making smart contracts smarter. In: Weippl, E., Katzenbeisser, S. Kruegel, C., Myers, A., Halevi, S. (eds.) Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security, Vienna, Austria, 24\u201328 October, 2016, pp. 254\u2013269. ACM (2016)"},{"key":"1_CR33","unstructured":"Maxwell, G.: Confidential transactions write up (2020). https:\/\/people.xiph.org\/~greg\/confidential_values.txt"},{"key":"1_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/978-3-319-65127-9_22","volume-title":"Computer Network Security","author":"R Metere","year":"2017","unstructured":"Metere, R., Dong, C.: Automated cryptographic analysis of the pedersen commitment scheme. In: Rak, J., Bay, J., Kotenko, I., Popyack, L., Skormin, V., Szczypiorski, K. (eds.) MMM-ACNS 2017. LNCS, vol. 10446, pp. 275\u2013287. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-65127-9_22"},{"key":"1_CR35","unstructured":"Nakamoto, S.: Bitcoin: A peer-to-peer electronic cash system, March 2009. Cryptography Mailing list at https:\/\/metzdowd.com"},{"key":"1_CR36","doi-asserted-by":"crossref","unstructured":"P\u00eerlea, G., Sergey, I.: Mechanising blockchain consensus. In: Proceedings of CPP 2018, pp. 78\u201390. ACM, New York (2018)","DOI":"10.1145\/3176245.3167086"},{"key":"1_CR37","unstructured":"Poelstra, A.: Mimblewimble, October 2016. https:\/\/download.wpsoftware.net\/bitcoin\/wizardry\/mimblewimble.pdf"},{"key":"1_CR38","unstructured":"The Coq Dev. Team. The Coq Proof Assistant Reference Manual - V. 8.9.0 (2019)"},{"key":"1_CR39","doi-asserted-by":"crossref","unstructured":"Venkatakrishnan, S.B., Fanti, G.C., Viswanath, P.: Dandelion: Redesigning the bitcoin network for anonymity. CoRR, abs\/1701.04439 (2017)","DOI":"10.1145\/3078505.3078528"},{"key":"1_CR40","unstructured":"Wanseob-Lim. Ethereum 9 3\/4: Send ERC20 privately using Mimblewimble and zk-SNARKs, September 2019. https:\/\/ethresear.ch\/t\/ethereum-9-send-erc20-privately-using-mimblewimble-and-zk-snarks\/6217"},{"key":"1_CR41","unstructured":"Wood, G.: Ethereum: A secure decentralised generalised transaction ledger eip-150 revision (759dccd - 2017\u201308-07) (2017). Accessed 03 Jan 2018"}],"container-title":["Lecture Notes in Computer Science","Applied Cryptography and Network Security Workshops"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-61638-0_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,8]],"date-time":"2021-04-08T16:46:24Z","timestamp":1617900384000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-61638-0_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030616373","9783030616380"],"references-count":41,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-61638-0_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"14 October 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ACNS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Applied Cryptography and Network Security","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Rome","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19 October 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 October 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"acns2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/sites.google.com\/di.uniroma1.it\/ACNS2020","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"214","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"46","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"21% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3.7","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"10","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"No","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Due to the Corona pandemic the conference was held virtually.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}