基于 TLA+ 的闪电网络形式化验证探析
计算机科学中的逻辑
2023-07-06 v1 密码学与安全
分布式、并行与集群计算
摘要
支付通道网络是一种提升基于区块链的加密货币可扩展性的方法。由于支付通道网络用于转移金融价值，其在存在对抗性参与者时的安全性应得到形式化验证。我们形式化了闪电网络（为比特币构建的支付通道网络）的协议，并展示该协议满足预期的安全属性。由于由多个参与者组成的规约的状态空间过大而无法进行模型检测，我们形式化了中间规约，并使用精化链来验证安全属性，其中每次精化或由模型检测或由笔纸证明予以论证。
引用
@article{arxiv.2307.02342,
title = {Towards a Formal Verification of the Lightning Network with TLA+},
author = {Matthias Grundmann and Hannes Hartenstein},
journal= {arXiv preprint arXiv:2307.02342},
year = {2023}
}