A Formally Verified Lightning Network
- URL: http://arxiv.org/abs/2503.07200v1
- Date: Mon, 10 Mar 2025 11:33:22 GMT
- Title: A Formally Verified Lightning Network
- Abstract summary: We use formal verification to prove that the Lightning Network (LN) always safeguards the funds of honest users.<n>We provide a custom implementation of (a simplification of) LN, express the desired security goals and, for the first time, provide a machine checkable proof that they are upheld under every scenario.
- Score: 0.0
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: In this work we use formal verification to prove that the Lightning Network (LN), the most prominent scaling technique for Bitcoin, always safeguards the funds of honest users. We provide a custom implementation of (a simplification of) LN, express the desired security goals and, for the first time, we provide a machine checkable proof that they are upheld under every scenario, all in an integrated fashion. We build our system using the Why3 platform.
Related papers
- Proof of Source of Funds: Efficient On-chain Provenance of Cryptoassets [5.222265639534245]
We introduce Proof of Source of Funds (PoSoF), a novel cryptographic framework that shifts the burden to the user.<n>PoSoF provides verifiable cryptographic provenance; it guarantees the legitimacy of the funds without leaking the intermediate transaction topology.<n>Our benchmarks demonstrate that fully private, proactive compliance is highly practical.
arXiv Detail & Related papers (2026-06-08T21:07:02Z) - Towards Automating Blockchain Consensus Verification with IsabeLLM [1.9336815376402718]
We present IsabeLLM, a tool that integrates the proof assistant Isabelle with a Large Language Model to assist and automate proofs.<n>We demonstrate the effectiveness of IsabeLLM by using it to develop a novel model of Bitcoin's Proof of Work consensus protocol and verify its correctness.
arXiv Detail & Related papers (2026-01-12T15:35:08Z) - TRUST: A Decentralized Framework for Auditing Large Language Model Reasoning [45.228233498964755]
Large Language Models generate reasoning chains that reveal their decision-making.<n>Existing auditing methods are centralized, opaque, and hard to scale.<n>We propose TRUST, a transparent, decentralized auditing framework.
arXiv Detail & Related papers (2025-10-23T04:16:44Z) - EGNInfoLeaker: Unveiling the Risks of Public Key Reuse and User Identity Leakage in Blockchain [10.349392384230274]
In this paper, we design a system called EGNInfoLeaker.<n>Our study is the first work that uncovers widespread public key reuse across peer-to-peer networks.<n>Going forward, our detection framework provides a foundation for enhancing real-world privacy preservation in decentralized networks.
arXiv Detail & Related papers (2025-07-02T12:07:03Z) - Model Checking the Security of the Lightning Network [0.7366405857677227]
The Lightning Network is a payment channel network built for Bitcoin that is already used in practice.<n>We formalize the protocol in TLA+ and formally specify the security property that honest users are guaranteed to retrieve their correct balance.<n>We make model checking the Lightning Network possible using two refinement steps that we verify using proofs.
arXiv Detail & Related papers (2025-05-21T14:22:34Z) - SoK: Bitcoin Layer Two (L2) [8.405922134866318]
We present the first Systematization of Knowledge (SoK) on constructing Layer Two (L2) solutions for Bitcoin.
Notably, we are the first to incorporate the inscription technology (emerged in mid-2023), along with a series of related innovations.
We find that the inscription-based approaches introduce new functionality (i.e., programability) to Bitcoin systems, whereas existing proof-based solutions primarily address scalability challenges.
arXiv Detail & Related papers (2024-09-04T12:26:33Z) - Towards Credential-based Device Registration in DApps for DePINs with ZKPs [46.08150780379237]
We propose a credential-based device registration (CDR) mechanism that verifies device credentials on the blockchain.
We present a general system model, and technically evaluate CDR using zkSNARKs with Groth16 and Marlin.
arXiv Detail & Related papers (2024-06-27T09:50:10Z) - Payout Races and Congested Channels: A Formal Analysis of Security in the Lightning Network [8.397189036839956]
The Lightning Network is a payment channel network designed to resolve Bitcoin's scalability issues through fast off-chain transactions.
Several vulnerabilities have been manually discovered, but to-date there have been few works systematically analyzing the security of the Lightning Network.
We take a foundational approach to analyzing the security of the Lightning Network with the help of formal methods.
arXiv Detail & Related papers (2024-05-03T14:52:47Z) - SQIAsignHD: SQIsignHD Adaptor Signature [0.6708691048956046]
We introduce $mathsfSQIAsignHD$, a new quantum-resistant adaptor signature scheme based on isogenies of supersingular elliptic curves.
We exploit the idea of the artificial orientation on the supersingular isogeny Diffie-Hellman key exchange protocol, SIDH, to define the underlying hard relation.
arXiv Detail & Related papers (2024-04-13T15:25:28Z) - Enhancing Trust and Privacy in Distributed Networks: A Comprehensive Survey on Blockchain-based Federated Learning [51.13534069758711]
Decentralized approaches like blockchain offer a compelling solution by implementing a consensus mechanism among multiple entities.
Federated Learning (FL) enables participants to collaboratively train models while safeguarding data privacy.
This paper investigates the synergy between blockchain's security features and FL's privacy-preserving model training capabilities.
arXiv Detail & Related papers (2024-03-28T07:08:26Z) - A Universal Identity Backdoor Attack against Speaker Verification based on Siamese Network [13.331857487581637]
We propose a backdoor attack for the speaker verification system.<n>We implant a universal identity in the model that can simulate any enrolled speaker and pass the verification.<n>Our work reveals the vulnerability of the speaker verification system and provides a new perspective to further improve the robustness of the system.
arXiv Detail & Related papers (2023-03-28T14:57:05Z) - FIRST: FrontrunnIng Resilient Smart ConTracts [3.5061201620029876]
In some cases, the inherently transparent and unregulated nature of cryptocurrencies leads to verifiable attacks on users of these applications.
One such attack is frontrunning, where a malicious entity leverages the knowledge of currently unprocessed financial transactions.
We propose FIRST, a framework that prevents frontrunning attacks and is built using cryptographic protocols.
arXiv Detail & Related papers (2022-04-02T23:30:13Z) - You are caught stealing my winning lottery ticket! Making a lottery
ticket claim its ownership [87.13642800792077]
Lottery ticket hypothesis (LTH) emerges as a promising framework to leverage a special sparse subnetwork.
Main resource bottleneck of LTH is however the extraordinary cost to find the sparse mask of the winning ticket.
Our setting adds a new dimension to the recently soaring interest in protecting against the intellectual property infringement of deep models.
arXiv Detail & Related papers (2021-10-30T03:38:38Z) - Certifiers Make Neural Networks Vulnerable to Availability Attacks [70.69104148250614]
We show for the first time that fallback strategies can be deliberately triggered by an adversary.
In addition to naturally occurring abstains for some inputs and perturbations, the adversary can use training-time attacks to deliberately trigger the fallback.
We design two novel availability attacks, which show the practical relevance of these threats.
arXiv Detail & Related papers (2021-08-25T15:49:10Z) - ESCORT: Ethereum Smart COntRacTs Vulnerability Detection using Deep
Neural Network and Transfer Learning [80.85273827468063]
Existing machine learning-based vulnerability detection methods are limited and only inspect whether the smart contract is vulnerable.
We propose ESCORT, the first Deep Neural Network (DNN)-based vulnerability detection framework for smart contracts.
We show that ESCORT achieves an average F1-score of 95% on six vulnerability types and the detection time is 0.02 seconds per contract.
arXiv Detail & Related papers (2021-03-23T15:04:44Z) - Symbolic Reinforcement Learning for Safe RAN Control [62.997667081978825]
We show a Symbolic Reinforcement Learning (SRL) architecture for safe control in Radio Access Network (RAN) applications.
In our tool, a user can select a high-level safety specifications expressed in Linear Temporal Logic (LTL) to shield an RL agent running in a given cellular network.
We demonstrate the user interface (UI) helping the user set intent specifications to the architecture and inspect the difference in allowed and blocked actions.
arXiv Detail & Related papers (2021-03-11T10:56:49Z) - Passport-aware Normalization for Deep Model Protection [122.61289882357022]
We propose a new passport-aware normalization formulation for deep learning models.
It only needs to add another passport-aware branch for IP protection.
It is demonstrated to be robust not only to common attack techniques like fine-tuning and model compression, but also to ambiguity attacks.
arXiv Detail & Related papers (2020-10-29T17:57:12Z) - Regulation conform DLT-operable payment adapter based on trustless -
justified trust combined generalized state channels [77.34726150561087]
Economy of Things (EoT) will be based on software agents running on peer-to-peer trustless networks.
We give an overview of current solutions that differ in their fundamental values and technological possibilities.
We propose to combine the strengths of the crypto based, decentralized trustless elements with established and well regulated means of payment.
arXiv Detail & Related papers (2020-07-03T10:45:55Z)
This list is automatically generated from the titles and abstracts of the papers in this site.
This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.