MimbleWimble加密货币协议的形式化分析
密码学与安全
2021-04-05 v1 软件工程
摘要
MimbleWimble(MW)是一种以隐私为导向的加密货币技术,其提供的安全性和扩展性属性使其区别于其他同类协议。我们提出并讨论这些属性,并概述一种模型驱动验证方法的基础,以解决协议实现正确性的认证问题。特别地,我们提出一个在所述的验证过程中关键的理想化模型,并明确识别并精确表述我们的模型为确保MW相关安全属性验证所需充分条件。由于MW构建于共识协议之上,我们开发了此类协议之一的Z规格说明,并给出由Z规格说明生成的原型片段。该原型可用作可执行模型以运行仿真。这使我们能够在无需以低级编程语言实现协议的情况下分析其行为。最后,我们分析当前开发状态下的Grin和Beam的MW实现。
引用
@article{arxiv.2104.00822,
title = {A Formal Analysis of the MimbleWimble Cryptocurrency Protocol},
author = {Adrián Silveira and Gustavo Betarte and Maximiliano Cristiá and Carlos Luna},
journal= {arXiv preprint arXiv:2104.00822},
year = {2021}
}