MimbleWimble加密货币协议的形式化分析
A Formal Analysis of the MimbleWimble Cryptocurrency Protocol
摘要：
MimbleWimble（MW）是一种面向隐私的加密货币技术，它提供了与其他同类协议不同的安全性和可扩展性。我们提出并讨论了这些属性，并概述了模型驱动的验证方法，以解决协议实现的正确性认证的基础。特别是，我们提出了一个理想化的模型，这是在所描述的验证过程中的关键，并确定和精确状态的充分条件，我们的模型，以确保验证相关的安全属性的MW。由于MW是建立在共识协议之上的，我们开发了一个这样的协议的Z规范，并从Z规范生成的$\{log\}$原型的摘录。该$\{log\}$原型可用作可运行模拟的可执行模型。这使我们能够分析协议的行为，而不必在低级程序设计语言中实现它。最后，我们分析了MW的Grin和Beam实现的当前发展状况。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
