Cargando…

A Formal Analysis of the Mimblewimble Cryptocurrency Protocol †

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...

Descripción completa

Detalles Bibliográficos
Autores principales: Silveira, Adrián, Betarte, Gustavo, Cristiá, Maximiliano, Luna, Carlos
Formato: Online Artículo Texto
Lenguaje:English
Publicado: MDPI 2021
Materias:
Acceso en línea:https://www.ncbi.nlm.nih.gov/pmc/articles/PMC8434605/
https://www.ncbi.nlm.nih.gov/pubmed/34502842
http://dx.doi.org/10.3390/s21175951
_version_ 1783751639548559360
author Silveira, Adrián
Betarte, Gustavo
Cristiá, Maximiliano
Luna, Carlos
author_facet Silveira, Adrián
Betarte, Gustavo
Cristiá, Maximiliano
Luna, Carlos
author_sort Silveira, Adrián
collection PubMed
description 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.
format Online
Article
Text
id pubmed-8434605
institution National Center for Biotechnology Information
language English
publishDate 2021
publisher MDPI
record_format MEDLINE/PubMed
spelling pubmed-84346052021-09-12 A Formal Analysis of the Mimblewimble Cryptocurrency Protocol † Silveira, Adrián Betarte, Gustavo Cristiá, Maximiliano Luna, Carlos Sensors (Basel) Article 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. MDPI 2021-09-04 /pmc/articles/PMC8434605/ /pubmed/34502842 http://dx.doi.org/10.3390/s21175951 Text en © 2021 by the authors. https://creativecommons.org/licenses/by/4.0/Licensee MDPI, Basel, Switzerland. This article is an open access article distributed under the terms and conditions of the Creative Commons Attribution (CC BY) license (https://creativecommons.org/licenses/by/4.0/).
spellingShingle Article
Silveira, Adrián
Betarte, Gustavo
Cristiá, Maximiliano
Luna, Carlos
A Formal Analysis of the Mimblewimble Cryptocurrency Protocol †
title A Formal Analysis of the Mimblewimble Cryptocurrency Protocol †
title_full A Formal Analysis of the Mimblewimble Cryptocurrency Protocol †
title_fullStr A Formal Analysis of the Mimblewimble Cryptocurrency Protocol †
title_full_unstemmed A Formal Analysis of the Mimblewimble Cryptocurrency Protocol †
title_short A Formal Analysis of the Mimblewimble Cryptocurrency Protocol †
title_sort formal analysis of the mimblewimble cryptocurrency protocol †
topic Article
url https://www.ncbi.nlm.nih.gov/pmc/articles/PMC8434605/
https://www.ncbi.nlm.nih.gov/pubmed/34502842
http://dx.doi.org/10.3390/s21175951
work_keys_str_mv AT silveiraadrian aformalanalysisofthemimblewimblecryptocurrencyprotocol
AT betartegustavo aformalanalysisofthemimblewimblecryptocurrencyprotocol
AT cristiamaximiliano aformalanalysisofthemimblewimblecryptocurrencyprotocol
AT lunacarlos aformalanalysisofthemimblewimblecryptocurrencyprotocol
AT silveiraadrian formalanalysisofthemimblewimblecryptocurrencyprotocol
AT betartegustavo formalanalysisofthemimblewimblecryptocurrencyprotocol
AT cristiamaximiliano formalanalysisofthemimblewimblecryptocurrencyprotocol
AT lunacarlos formalanalysisofthemimblewimblecryptocurrencyprotocol