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...
Autores principales: | , , , |
---|---|
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 |