A Model-Driven Analysis of Mimblewimble Security Properties and its Protocol Implementations

Adrián Silveira; Gustavo Betarte; Maximiliano Cristiá; Carlos Luna

doi:10.36561/ING.24.10

Authors

Adrián Silveira Universidad de la República, Uruguay https://orcid.org/0000-0001-8742-046X
Gustavo Betarte Universidad de la República, Uruguay https://orcid.org/0000-0002-6863-1082
Maximiliano Cristiá Univesidad Nacional de Rosario, Argentina https://orcid.org/0000-0001-9163-2609
Carlos Luna Universidad de la República, Uruguay https://orcid.org/0000-0002-9985-5927

DOI:

https://doi.org/10.36561/ING.24.10

Keywords:

Security, Formal verification, Mimblewimble, Idealized model, Cryptocurrency

Abstract

Mimblewimble is a privacy-oriented cryptocurrency technology that provides security and scalability properties that distinguish it from other protocols. Mimblewimble’s cryptographic approach is based on Elliptic Curve Cryptography which allows verifying a transaction without revealing any information about the transactional amount or the parties involved. Mimblewimble combines Confidential transactions, CoinJoin, and cut-through to achieve a higher level of privacy, security, and scalability. In this work, we present and discuss these security 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. Then, we identify and precisely state the conditions for our model to ensure the verification of relevant security properties of Mimblewimble. In addition, we analyze the Grin and Beam implementations of Mimblewimble in their current state of development. We present detailed connections between our model and their implementations regarding the Mimblewimble structure and its security properties.

Downloads

Download data is not yet available.

References

Beam. Beam description. Comparison with classical MW, 2018. Available online: https://docs.beam.mw/BEAM_Comparison_with_classical_MW.pdf (accessed

on May 29, 2023).

C. Boyd, K. Gjøsteen, and S. Wu. A Blockchain Model in Tamarin and Formal Analysis of Hash Time Lock Contract. In Bruno Bernardo and Diego Marmsoler, editors, 2nd Workshop on Formal Methods for Blockchains (FMBC 2020), volume 84 of OpenAccess Series in Informatics (OASIcs), pages 5:1–5:13, Dagstuhl, Germany, 2020. Schloss Dagstuhl–Leibniz-Zentrum für Informatik.

Vitalik Buterin. Critical update re: Dao vulnerability, 2017. Available online: https://blog.ethereum.org/2016/06/17/critical-update-re-dao-vulnerability (accessed on May 29, 2023).

B. Bünz, J. Bootle, D. Boneh, A. Poelstra, P. Wuille, and G. Maxwell. Bulletproofs: Short proofs for confidential transactions and more. In 2018 IEEE Symposium on Security and Privacy (SP), pages 315–334, May 2018.

Claude Crépeau. Commitment. In Henk C. A. van Tilborg and Sushil Jajodia, editors, Encyclopedia of Cryptography and Security, 2nd Ed, pages 224–227. Springer, 2011.

Beam Foundation. Beam confidential cryptocurrency, 2020. Available online: https://beam.mw/ (accessed on May 29, 2023).

Grin. Introduction to MimbleWimble and Grin, 2016. Available online: https://github.com/mimblewimble/grin/blob/master/doc/intro.md (accessed on May 29, 2023).

F. Idelberger, G. Governatori, R. Riveret, and G. Sartor. Evaluation of logic-based smart contracts for blockchain systems. In J. Alferes, L. Bertossi, G. Governatori, P. Fodor, and D. Roman, editors, Rule Technologies. Research, Tools, and Applications - 10th International Symposium, RuleML 2016, Stony Brook, NY, USA, July 6-9, 2016. Proceedings, volume 9718 of LNCS, pages 167–183. Springer, 2016.

T. Jedusor. Mimblewimble, 2016. Available online: https://scalingbitcoin.org/papers/mimblewimble.txt (accessed on May 29, 2023).

G. Maxwell. Coinjoin: Bitcoin privacy for the real world, 2013. Available online: https://bitcointalk.org/index.php?topic=279249.0 (accessed on May 29, 2023).

G. Maxwell. Confidential transactions write up, 2020. Available online: https://web.archive.org/web/20200502151159/, https://people.xiph.org/~greg/confidential_values.txt (accessed on May 29, 2023)

Ian Miers, Christina Garman, Matthew Green, and Aviel D. Rubin. Zerocoin: Anonymous distributed e-cash from bitcoin. In 2013 IEEE Symposium on Security and Privacy, pages 397– 411, 2013.

A. Poelstra. Mimblewimble, 2016. Available online: https://download.wpsoftware.net/bitcoin/wizardry/mimblewimble.pdf (accessed on May 29, 2023).

Grigore Rosu. Formal Design, Implementation and Verification of Blockchain Languages Using K (Invited Talk). In Bruno Bernardo and Diego Marmsoler, editors, 2nd Workshop on Formal Methods for Blockchains (FMBC 2020), volume 84 of OpenAccess Series in Informatics (OASIcs), pages 1:1–1:1, Dagstuhl, Germany, 2020. Schloss Dagstuhl–Leibniz-Zentrum für Informatik.

Tim Ruffing, Sri Aravinda Thyagarajan, Viktoria Ronge, and Dominique Schröder. Burning zerocoins for fun and for profit: A cryptographic denial-of-spending attack on the zerocoin protocol. Cryptology ePrint Archive, Paper 2018/612, 2018. https://eprint.iacr.org/2018/612.

Adrián Silveira, Gustavo Betarte, Maximiliano Cristiá, and Carlos Luna. A formal analysis of the mimblewimble cryptocurrency protocol. Sensors, 21(17), 2021.