形式化验证的闪电网络
密码学与安全
2025-03-11 v1 计算机科学中的逻辑
摘要
在这项工作中，我们使用形式化验证来证明闪电网络 (LN)——比特币最突出的扩容技术——始终保护诚实用户的资金。我们提供了 LN（及其简化版本）的自定义实现，表达了预期的安全目标，并首次以集成的方式提供了在所有场景下均能维持这些目标的机器可检验证明。我们使用 Why3 平台构建了我们的系统。
引用
@article{arxiv.2503.07200,
title = {A Formally Verified Lightning Network},
author = {Grzegorz Fabiański and Rafał Stefański and Orfeas Stefanos Thyfronitis Litos},
journal= {arXiv preprint arXiv:2503.07200},
year = {2025}
}