english Icono del idioma   español Icono del idioma  

Please use this identifier to cite or link to this item: https://hdl.handle.net/20.500.12008/32492 How to cite
Title: A formal analysis of the mimblewimble cryptocurrency protocol with a security approach
Authors: Silveira Lapenne, Adrián Gerardo
Obtained title: Magíster en Informática
University or service that grants the title: Universidad de la República (Uruguay). Facultad de Ingeniería
Tutor: Carlos, Luna
Betarte, Gustavo
Type: Tesis de maestría
Keywords: Cryptocurrency, Mimblewimble, Idealized model, Formal verification, Security
Issue Date: 2022
Abstract: A cryptocurrency is a digital currency that can be exchanged online for goods and services. Cryptocurrencies are deployed over public blockchains which have the transactions duplicated and distributed across the nodes of a computer network. This decentralized mechanism is devised in order to achieve reliability in a network consisting of unreliable nodes. Privacy, anonymity and security have become crucial in this context. For that reason, formal and mathematical approaches are gaining popularity in order to guarantee the correctness of the cryptocurrency implementations. Mimblewimble is a privacy-oriented cryptocurrency technology which provides security and scalability properties that distinguish it from other protocols of its kind. It was proposed by an anonymous developer, who posted a link to a text file on the IRC channel by the name Tom Elvis Jedusor (french name for Voldemort) in mid-2016. Mimblewimble’s cryptographic approach is based on Elliptic Curve Cryptography which allows to verify 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 and security, as well as, scalability. In this thesis, 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. The main components of our idealized model are transactions, blocks and chain. 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.
Publisher: Udelar.FI.
ISSN: 1688-2792
Citation: Silveira Lapenne, A. A formal analysis of the mimblewimble cryptocurrency protocol with a security approach [en línea] Tesis de maestría. Montevideo : Udelar. FI. INCO : PEDECIBA. Área Informática, 2022.
License: Licencia Creative Commons Atribución - No Comercial - Sin Derivadas (CC - By-NC-ND 4.0)
Appears in Collections:Tesis de posgrado - Instituto de Computación

Files in This Item:
File Description SizeFormat  
SIL22.pdfTesis de maestría926 kBAdobe PDFView/Open


This item is licensed under a Creative Commons License Creative Commons