Formalization and security analysis of the Bridgeless protocol

TL;DR

This paper formalizes and proves the security of the Bridgeless protocol, a chain-agnostic token bridging system supporting multiple blockchains, ensuring safety and liveness through formalized subprotocols.

Contribution

It provides a formal security proof for the Bridgeless protocol and details the conditions for its safety and liveness across supported chains.

Findings

Security is formally proven under specified conditions.

Supports multiple chains including EVM, Zano, and Bitcoin.

Defines subprotocols and their safety conditions.

Abstract

This paper formalizes the proves the security of the Bridgeless protocol, a protocol able to bridge tokens between various chains. The Bridgeless protocol is run by a set of validators, responsible for verifying deposit transactions on the source chain and generating the corresponding withdrawals on the target chain. The protocol is designed to be chain-agnostic and the validators interact with each supported chain via a chain client. It currently supports EVM-compatible chains, the Zano, and the Bitcoin chains. The paper formalizes all involved subprotocols and describes the conditions under which the protocol maintains safety and liveness.