MimbleWimble (MW) is a privacy-oriented cryptocurrency technology which 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 sufficient conditions for our model to ensure the verification of 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 generated from the Z specification. This $\{log\}$ prototype can be used as an executable model where simulations can be run. 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.
翻译：MimbleWimble (MW) 是一种以隐私为导向的加密货币技术,它提供安全和可缩放性特性,将其与其他协议区分开来。我们介绍和讨论这些特性,并概述一种示范驱动的核查方法的基础,以解决证明议定书执行的正确性的问题。特别是,我们提出了一个理想化的模式,这是描述的核查过程的关键,并查明和确切地说明我们模型的足够条件,以确保核查MW的有关安全特性。由于MW是在协商一致的协议协议之上建立的,我们为其中一项协议制定了Z规格,并摘录了从Z规格中生成的$ ⁇ log ⁇ $原型。这个$ ⁇ log ⁇ $的原型可以用作模拟运行的可执行模型。这使我们能够分析协议的行为,而不必用低水平的编程语言来实施。最后,我们分析了MW在目前发展状态中的Grin和Baam执行情况。
相关内容
微信扫码咨询专知VIP会员