{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,12]],"date-time":"2025-10-12T02:20:03Z","timestamp":1760235603771,"version":"build-2065373602"},"reference-count":64,"publisher":"MDPI AG","issue":"17","license":[{"start":{"date-parts":[[2021,9,4]],"date-time":"2021-09-04T00:00:00Z","timestamp":1630713600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Sensors"],"abstract":"<jats:p>Mimblewimble (MW) is a privacy-oriented cryptocurrency technology that provides security and scalability properties that distinguish it from other protocols of its kind. We present and discuss those properties and outline the basis of a model-driven verification approach to address the certification of the correctness of the protocol implementations. In particular, we propose an idealized model that is key in the described verification process, and identify and precisely state the conditions for our model to ensure the verification of the relevant security properties of MW. Since MW is built on top of a consensus protocol, we develop a Z specification of one such protocol and present an excerpt of the {log} prototype after its Z specification. This {log} prototype can be used as an executable model. This allows us to analyze the behavior of the protocol without having to implement it in a low level programming language. Finally, we analyze the Grin and Beam implementations of MW in their current state of development.<\/jats:p>","DOI":"10.3390\/s21175951","type":"journal-article","created":{"date-parts":[[2021,9,6]],"date-time":"2021-09-06T13:18:26Z","timestamp":1630934306000},"page":"5951","update-policy":"https:\/\/doi.org\/10.3390\/mdpi_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["A Formal Analysis of the Mimblewimble Cryptocurrency Protocol"],"prefix":"10.3390","volume":"21","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8742-046X","authenticated-orcid":false,"given":"Adri\u00e1n","family":"Silveira","sequence":"first","affiliation":[{"name":"Facultad de Ingenier\u00eda, Universidad de la Rep\u00fablica, Montevideo 11300, Uruguay"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6863-1082","authenticated-orcid":false,"given":"Gustavo","family":"Betarte","sequence":"additional","affiliation":[{"name":"Facultad de Ingenier\u00eda, Universidad de la Rep\u00fablica, Montevideo 11300, Uruguay"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9163-2609","authenticated-orcid":false,"given":"Maximiliano","family":"Cristi\u00e1","sequence":"additional","affiliation":[{"name":"CIFASIS, Universidad Nacional de Rosario, Rosario 2000, Argentina"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9985-5927","authenticated-orcid":false,"given":"Carlos","family":"Luna","sequence":"additional","affiliation":[{"name":"Facultad de Ingenier\u00eda, Universidad de la Rep\u00fablica, Montevideo 11300, Uruguay"}]}],"member":"1968","published-online":{"date-parts":[[2021,9,4]]},"reference":[{"key":"ref_1","unstructured":"Buterin, V. (2021, August 27). Critical Update Re: DAO Vulnerability. Available online: https:\/\/blog.ethereum.org\/2016\/06\/17\/critical-update-re-dao-vulnerability."},{"key":"ref_2","doi-asserted-by":"crossref","first-page":"61","DOI":"10.32609\/0042-8736-2020-9-61-79","article-title":"Dedollarization and settlements in national currencies: Eurasian and Latin American experience","volume":"9","author":"Mishina","year":"2020","journal-title":"Vopr. Ekon."},{"key":"ref_3","first-page":"1:1","article-title":"Formal Design, Implementation and Verification of Blockchain Languages Using K (Invited Talk)","volume":"Volume 84","author":"Bernardo","year":"2020","journal-title":"Proceedings of the 2nd Workshop on Formal Methods for Blockchains (FMBC 2020)"},{"key":"ref_4","doi-asserted-by":"crossref","unstructured":"Garfatta, I., Klai, K., Gaaloul, W., and Graiet, M. A Survey on Formal Verification for Solidity Smart Contracts. Proceedings of the 2021 Australasian Computer Science Week Multiconference (ACSW\u201921).","DOI":"10.1145\/3437378.3437879"},{"key":"ref_5","doi-asserted-by":"crossref","first-page":"101979","DOI":"10.1016\/j.jairtraman.2020.101979","article-title":"A Linear Programming approach for robust network revenue management in the airline industry","volume":"91","author":"An","year":"2021","journal-title":"J. Air Transp. Manag."},{"key":"ref_6","unstructured":"Jedusor, T. (2021, August 27). MimbleWimble. Available online: https:\/\/scalingbitcoin.org\/papers\/mimblewimble.txt."},{"key":"ref_7","unstructured":"Poelstra, A. (2021, August 27). MimbleWimble. Available online: https:\/\/download.wpsoftware.net\/bitcoin\/wizardry\/mimblewimble.pdf."},{"key":"ref_8","unstructured":"Nakamoto, S. (2021, August 27). Bitcoin: A Peer-to-Peer Electronic Cash System. Available online: https:\/\/bitcoin.org\/bitcoin.pdf."},{"key":"ref_9","unstructured":"Grin (2021, August 27). Introduction to MimbleWimble and Grin. Available online: https:\/\/github.com\/mimblewimble\/grin\/blob\/master\/doc\/intro.md."},{"key":"ref_10","unstructured":"Foundation, B. (2021, August 27). Beam Confidential Cryptocurrency. Available online: https:\/\/beam.mw\/."},{"key":"ref_11","unstructured":"Anderson, J.P. (2021, August 27). Computer Security Technology Planning Study, U.S. Air Force Electronic Systems Division. Available online: https:\/\/apps.dtic.mil\/sti\/citations\/AD0758206."},{"key":"ref_12","unstructured":"LaPadula, L., Bell, D.E., and Lapadula, L.J. (2021, August 27). Secure Computer Systems: Mathematical Foundations, Draft MTR, The MITRE Corporation. Available online: http:\/\/www-personal.umich.edu\/~cja\/LPS12b\/refs\/belllapadula1.pdf."},{"key":"ref_13","unstructured":"Wood, G. (2021, August 27). Ethereum: A Secure Decentralised Generalised Transaction Ledger EIP-150 REVISION (759dccd - 2017-08-07). Available online: https:\/\/ethereum.github.io\/yellowpaper\/paper.pdf."},{"key":"ref_14","doi-asserted-by":"crossref","unstructured":"Sestrem Och\u00f4a, I., Augusto Silva, L., de Mello, G., Garcia, N.M., de Paz Santana, J.F., and Quietinho Leithardt, V.R. (2020). A Cost Analysis of Implementing a Blockchain Architecture in a Smart Grid Scenario Using Sidechains. Sensors, 20.","DOI":"10.3390\/s20030843"},{"key":"ref_15","first-page":"167","article-title":"Evaluation of Logic-Based Smart Contracts for Blockchain Systems","volume":"Volume 9718","author":"Alferes","year":"2016","journal-title":"Proceedings of the RuleML 2016: Rule Technologies. Research, Tools, and Applications-10th International Symposium"},{"key":"ref_16","doi-asserted-by":"crossref","unstructured":"Bhargavan, K., Delignat-Lavaud, A., Fournet, C., Gollamudi, A., Gonthier, G., Kobeissi, N., Kulatova, N., Rastogi, A., Sibut-Pinote, T., and Swamy, N. (2016). Formal Verification of Smart Contracts: Short Paper. Proceedings of the 2016 ACM Workshop on Programming Languages and Analysis for Security (PLAS\u201916), ACM.","DOI":"10.1145\/2993600.2993611"},{"key":"ref_17","unstructured":"Weippl, E., Katzenbeisser, S., Kruegel, C., Myers, A., and Halevi, S. (2016, January 24\u201328). Making Smart Contracts Smarter. Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security, Vienna, Austria."},{"key":"ref_18","first-page":"520","article-title":"Defining the Ethereum Virtual Machine for Interactive Theorem Provers","volume":"Volume 10323","author":"Brenner","year":"2017","journal-title":"Financial Cryptography and Data Security, Proceedings of the FC 2017 International Workshops, WAHC, BITCOIN, VOTING, WTSC, and TA"},{"key":"ref_19","first-page":"243","article-title":"A Semantic Framework for the Security Analysis of Ethereum Smart Contracts","volume":"Volume 10804","author":"Bauer","year":"2018","journal-title":"Proceedings of the Principles of Security and Trust-7th International Conference, POST 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018"},{"key":"ref_20","unstructured":"Andronick, J., and Felty, A.P. (2018, January 8\u20139). Mechanising blockchain consensus. Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018, Los Angeles, CA, USA."},{"key":"ref_21","unstructured":"The Coq Team (2021, August 27). The Coq Proof Assistant Reference Manual. Available online: http:\/\/coq.inria.fr."},{"key":"ref_22","doi-asserted-by":"crossref","unstructured":"Bertot, Y., and Cast\u00e9ran, P. (2004). Interactive Theorem Proving and Program Development: Coq\u2019Art: The Calculus of Inductive Constructions, Springer. Texts in Theoretical Computer Science.","DOI":"10.1007\/978-3-662-07964-5"},{"key":"ref_23","first-page":"2:1","article-title":"Formal Specification and Verification of Solidity Contracts with Events (Short Paper)","volume":"Volume 84","author":"Bernardo","year":"2020","journal-title":"Proceedings of the 2nd Workshop on Formal Methods for Blockchains, FMBC@CAV 2020"},{"key":"ref_24","first-page":"4:1","article-title":"Tezla, an Intermediate Representation for Static Analysis of Michelson Smart Contracts","volume":"Volume 84","author":"Bernardo","year":"2020","journal-title":"Proceedings of the 2nd Workshop on Formal Methods for Blockchains (FMBC 2020)"},{"key":"ref_25","first-page":"5:1","article-title":"A Blockchain Model in Tamarin and Formal Analysis of Hash Time Lock Contract","volume":"Volume 84","author":"Bernardo","year":"2020","journal-title":"Proceedings of the 2nd Workshop on Formal Methods for Blockchains (FMBC 2020)"},{"key":"ref_26","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/3464421","article-title":"A Survey of Smart Contract Formal Specification and Verification","volume":"54","author":"Tolmach","year":"2021","journal-title":"ACM Comput. Surv."},{"key":"ref_27","first-page":"275","article-title":"Automated Cryptographic Analysis of the Pedersen Commitment Scheme","volume":"Volume 10446","author":"Rak","year":"2017","journal-title":"Proceedings of the Computer Network Security-7th International Conference on Mathematical Methods, Models, and Architectures for Computer Network Security, MMM-ACNS 2017"},{"key":"ref_28","first-page":"146","article-title":"EasyCrypt: A Tutorial","volume":"Volume 8604","author":"Aldini","year":"2013","journal-title":"Foundations of Security Analysis and Design VII-FOSAD 2012\/2013 Tutorial Lectures"},{"key":"ref_29","first-page":"657","article-title":"Aggregate Cash Systems: A Cryptographic Investigation of Mimblewimble","volume":"Volume 11476","author":"Ishai","year":"2019","journal-title":"Proceedings of the Advances in Cryptology-EUROCRYPT 2019-38th Annual International Conference on the Theory and Applications of Cryptographic Techniques"},{"key":"ref_30","unstructured":"Betarte, G., Cristi\u00e1, M., Luna, C., Silveira, A., and Zanarini, D. (2019). Set-Based Models for Cryptocurrency Software. arXiv."},{"key":"ref_31","first-page":"3","article-title":"Towards a Formally Verified Implementation of the MimbleWimble Cryptocurrency Protocol","volume":"Volume 12418","author":"Zhou","year":"2020","journal-title":"Proceedings of the Applied Cryptography and Network Security Workshops-ACNS 2020 Satellite Workshops, AIBlock, AIHWS, AIoTS, Cloud S&amp P, SCI; SecMT, and SiMLA"},{"key":"ref_32","unstructured":"Maxwell, G. (2021, August 27). Confidential Transactions Write Up. Available online: https:\/\/web.archive.org\/web\/20200502151159\/https:\/\/people.xiph.org\/~greg\/confidential_values.txt."},{"key":"ref_33","unstructured":"Gibson, A. (2021, August 27). An Investigation into Confidential Transactions. Available online: https:\/\/github.com\/AdamISZ\/ConfidentialTransactionsDoc\/blob\/master\/essayonCT.pdf."},{"key":"ref_34","doi-asserted-by":"crossref","unstructured":"van Tilborg, H.C.A., and Jajodia, S. (2011). Commitment. Encyclopedia of Cryptography and Security, Springer. [2nd ed.].","DOI":"10.1007\/978-1-4419-5906-5"},{"key":"ref_35","doi-asserted-by":"crossref","unstructured":"B\u00fcnz, B., Bootle, J., Boneh, D., Poelstra, A., Wuille, P., and Maxwell, G. (2018, January 20\u201324). Bulletproofs: Short Proofs for Confidential Transactions and More. Proceedings of the 2018 IEEE Symposium on Security and Privacy (SP), San Francisco, CA, USA.","DOI":"10.1109\/SP.2018.00020"},{"key":"ref_36","unstructured":"Maxwell, G. (2021, August 27). CoinJoin: Bitcoin Privacy for the Real World. Available online: https:\/\/bitcointalk.org\/index.php?topic=279249.0."},{"key":"ref_37","first-page":"281","article-title":"The Bitcoin Backbone Protocol: Analysis and Applications","volume":"Volume 9057","author":"Oswald","year":"2015","journal-title":"Proceedings of the Advances in Cryptology-EUROCRYPT 2015-34th Annual International Conference on the Theory and Applications of Cryptographic Techniques"},{"key":"ref_38","doi-asserted-by":"crossref","first-page":"357","DOI":"10.1007\/978-3-319-63688-7_12","article-title":"Ouroboros: A Provably Secure Proof-of-Stake Blockchain Protocol","volume":"Volume 10401","author":"Katz","year":"2017","journal-title":"Proceedings of the Advances in Cryptology-CRYPTO 2017-37th Annual International Cryptology Conference"},{"key":"ref_39","first-page":"170","article-title":"Switch Commitments: A Safety Switch for Confidential Transactions","volume":"Volume 10323","author":"Brenner","year":"2017","journal-title":"Proceedings of the Financial Cryptography and Data Security-FC 2017 International Workshops, WAHC, BITCOIN, VOTING, WTSC, and TA"},{"key":"ref_40","first-page":"10","article-title":"A Public Key Cryptosystem and a Signature Scheme Based on Discrete Logarithms","volume":"Volume 196","author":"Gamal","year":"1984","journal-title":"Proceedings of the Advances in Cryptology, Proceedings of CRYPTO \u201984"},{"key":"ref_41","first-page":"1","article-title":"Dandelion: Redesigning the Bitcoin Network for Anonymity","volume":"1","author":"Fanti","year":"2017","journal-title":"Proc. ACM Meas. Anal. Comput. Syst."},{"key":"ref_42","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/3224424","article-title":"Dandelion++: Lightweight Cryptocurrency Networking with Formal Anonymity Guarantees","volume":"2","author":"Fanti","year":"2018","journal-title":"Proc. ACM Meas. Anal. Comput. Syst."},{"key":"ref_43","unstructured":"Grin (2021, August 27). Dandelion++ in Grin: Privacy-Preserving Transaction Aggregation and Propagation. Available online: https:\/\/github.com\/mimblewimble\/grin\/blob\/master\/doc\/dandelion\/dandelion.md."},{"key":"ref_44","unstructured":"Grin (2021, August 27). Privacy Primer. Available online: https:\/\/github.com\/mimblewimble\/docs\/wiki\/Grin-Privacy-Primer."},{"key":"ref_45","unstructured":"Miers, I. (2021, August 27). Blockchain Privacy: Equal Parts Theory and Practice. Available online: https:\/\/www.zfnd.org\/blog\/blockchain-privacy\/#flashlight."},{"key":"ref_46","unstructured":"Grin Community (2021, August 27). Grin: Open Research Problems. Available online: https:\/\/grin.mw\/open-research-problems."},{"key":"ref_47","unstructured":"Lim, W. (2021, August 27). Ethereum 9 3\/4: Send ERC20 Privately Using Mimblewimble and zk-SNARKs. Available online: https:\/\/ethresear.ch\/t\/ethereum-9-send-erc20-privately-using-mimblewimble-and-zk-snarks\/6217."},{"key":"ref_48","unstructured":"Korsell, E., Mueller, P., and Schumann, Y. (2021, August 27). Alias, White-Paper. Available online: https:\/\/alias.cash\/wp-content\/uploads\/2021\/02\/Alias-Whitepaper.pdf."},{"key":"ref_49","doi-asserted-by":"crossref","first-page":"295","DOI":"10.1007\/s10817-019-09520-4","article-title":"Solving Quantifier-Free First-Order Constraints Over Finite Sets and Binary Relations","volume":"64","author":"Rossi","year":"2020","journal-title":"J. Autom. Reason."},{"key":"ref_50","first-page":"200","article-title":"A New Extraction for Coq","volume":"Volume 2646","author":"Geuvers","year":"2002","journal-title":"Proceedings of the Types for Proofs and Programs, Second International Workshop, TYPES 2002, Berg en Dal"},{"key":"ref_51","doi-asserted-by":"crossref","unstructured":"Zinzindohoue, J.K., Bartzia, E., and Bhargavan, K. (July, January 27). A Verified Extensible Library of Elliptic Curves. Proceedings of the IEEE 29th Computer Security Foundations Symposium, CSF 2016, Lisbon, Portugal.","DOI":"10.1109\/CSF.2016.28"},{"key":"ref_52","unstructured":"D\u00e9n\u00e8s, M., Hritcu, C., Lampropoulos, L., Paraskevopoulou, Z., and Pierce, B. (2021, August 27). QuickChick: Property-Based Testing for Coq. Available online: http:\/\/citeseerx.ist.psu.edu\/viewdoc\/download?doi=10.1.1.718.1395&rep=rep1&type=pdf."},{"key":"ref_53","first-page":"229","article-title":"{log} as a Test Case Generator for the Test Template Framework","volume":"Volume 8137","author":"Hierons","year":"2013","journal-title":"Proceedings of the Software Engineering and Formal Methods-11th International Conference, SEFM 2013"},{"key":"ref_54","doi-asserted-by":"crossref","first-page":"185","DOI":"10.1007\/978-3-319-63046-5_12","article-title":"A Decision Procedure for Restricted Intensional Sets","volume":"Volume 10395","year":"2017","journal-title":"Proceedings of the Automated Deduction-CADE 26-26th International Conference on Automated Deduction"},{"key":"ref_55","unstructured":"Grin (2021, August 27). Grin Source Code Switch Commitments. Available online: https:\/\/github.com\/mimblewimble\/secp256k1-zkp\/blob\/73617d0fcc4f51896cce4f9a1a6977a6958297f8\/src\/modules\/commitment\/main_impl.h#L267."},{"key":"ref_56","unstructured":"Beam (2021, August 27). Beam the Scalable Confidential Cryptocurrency. Available online: https:\/\/docs.beam.mw\/BEAM_Position_Paper_0.3.pdf."},{"key":"ref_57","unstructured":"Beam (2021, August 27). Beam Description. Comparison with Classical MW, Available online: https:\/\/docs.beam.mw\/BEAM_Comparison_with_classical_MW.pdf."},{"key":"ref_58","unstructured":"Beam (2021, August 27). Beam Emission Schedule. Available online: https:\/\/docs.beam.mw\/BEAM_Position_Paper_v0.2.2.pdf."},{"key":"ref_59","unstructured":"(2021, August 27). Beam.Secure Bulletin Board System (SBBS). Available online: https:\/\/github.com\/BeamMW\/beam\/wiki\/Secure-bulletin-board-system-(SBBS)."},{"key":"ref_60","unstructured":"Blanchet, B. (2001, January 11\u201313). An Efficient Cryptographic Protocol Verifier Based on Prolog Rules. Proceedings of the 14th IEEE Computer Security Foundations Workshop (CSFW-14 2001), Cape Breton, NS, Canada."},{"key":"ref_61","doi-asserted-by":"crossref","unstructured":"Blanchet, B. (2018, January 9\u201312). Composition Theorems for CryptoVerif and Application to TLS 1.3. Proceedings of the 31st IEEE Computer Security Foundations Symposium, CSF 2018, Oxford, UK.","DOI":"10.1109\/CSF.2018.00009"},{"key":"ref_62","unstructured":"Tamarin (2021, August 27). Tamarin Prover. Available online: https:\/\/tamarin-prover.github.io."},{"key":"ref_63","doi-asserted-by":"crossref","unstructured":"Grin (2021, August 27). Grin Project Github. Available online: https:\/\/github.com\/mimblewimble\/grin.","DOI":"10.17355\/rkkpt.v27i3.273"},{"key":"ref_64","unstructured":"Beam (2021, August 27). Beam Project Github. Available online: https:\/\/github.com\/BeamMW\/beam."}],"container-title":["Sensors"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.mdpi.com\/1424-8220\/21\/17\/5951\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T06:56:36Z","timestamp":1760165796000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.mdpi.com\/1424-8220\/21\/17\/5951"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,9,4]]},"references-count":64,"journal-issue":{"issue":"17","published-online":{"date-parts":[[2021,9]]}},"alternative-id":["s21175951"],"URL":"https:\/\/doi.org\/10.3390\/s21175951","relation":{},"ISSN":["1424-8220"],"issn-type":[{"type":"electronic","value":"1424-8220"}],"subject":[],"published":{"date-parts":[[2021,9,4]]}}}