基于时间自动机的比特币合约建模
密码学与安全
2014-07-01 v2
摘要
比特币是一种点对点加密货币系统。自 2008 年推出以来，比特币获得了显著的关注，主要归功于以下特性：(1) 交易费用极低；(2) 不受任何中央机构控制，这意味着无人能“印制”货币以引发通货膨胀。此外，其交易语法允许创建所谓的“合约”，即多个互不信任的参与方共同参与一个协议以联合执行某项金融任务，而该过程的公平性由比特币的特性予以保证。尽管比特币合约在数字经济中具有多种潜在应用，但迄今为止尚未在现实生活中得到广泛应用。这部分是因为它们创建和分析起来十分繁琐，因而使用风险较高。在本文中，我们提出利用最初为硬件和软件系统计算机辅助分析开发的方法（特别是基于时间自动机的方法）来解决这一问题。更具体地说，我们提出了一个在 UPPAAL 模型检测器中使用时间自动机对比特币合约进行建模的框架。我们的方法具有通用性，可用于建模多种合约。作为概念验证，我们利用该框架对近期先前工作中的一些比特币合约进行了建模。随后，我们在 UPPAAL 中自动验证了它们的安全性，发现并修正了一些通过人工分析难以察觉的细微错误。我们希望我们的工作能引起从事形式化建模的研究人员对比特币合约验证问题的关注，并激发更多关于此主题的研究。
引用
@article{arxiv.1405.1861,
title = {Modeling Bitcoin Contracts by Timed Automata},
author = {Marcin Andrychowicz and Stefan Dziembowski and Daniel Malinowski and Łukasz Mazurek},
journal= {arXiv preprint arXiv:1405.1861},
year = {2014}
}