Table of Contents
Fetching ...

Atomic Transfer Graphs: Secure-by-design Protocols for Heterogeneous Blockchain Ecosystems

Stephan Dübler, Federico Badaloni, Pedro Moreno-Sanchez, Clara Schneidewind

TL;DR

This work addresses fragmentation in blockchain ecosystems by introducing Atomic Transfer Graphs ($ATG$) as a unifying specification for transfers and security guarantees. It develops a transfer-tree intermediate representation ($xtree$) and a building block called Conditional Timelock Contracts ($CTLC$) to realize ATGs on heterogeneous transfer agreement mechanisms ($TAM$). The authors provide a formal symbolic security model, prove end-to-end security and correctness, and demonstrate practical CTLC implementations on Ethereum and Bitcoin, plus off-chain payment-channel integrations. By enabling secure-by-design cross-chain and off-chain applications (e.g., multi-hop payments, atomic swaps, crowdfunding) across TAMs, the framework offers a scalable, generic approach to protocol synthesis in heterogeneous blockchain environments. Overall, this framework unifies diverse transfer tasks under a single security- and performance-conscious design paradigm with broad applicability.

Abstract

The heterogeneity of the blockchain landscape has motivated the design of blockchain protocols tailored to specific blockchains and applications that, hence, require custom security proofs. We observe that many blockchain protocols share common security and functionality goals, which can be captured by an atomic transfer graph (ATG) describing the structure of desired transfers. Based on this observation, we contribute a framework for generating secure-by-design protocols that realize these goals. The resulting protocols build upon Conditional Timelock Contracts (CTLCs), a novel minimal smart contract functionality that can be implemented in a large variety of cryptocurrencies with a restricted scripting language (e.g., Bitcoin), and payment channels. We show how ATGs, in addition to enabling novel applications, capture the security and functionality goals of existing applications, including many examples from payment channel networks and complex multi-party cross-currency swaps among Ethereum-style cryptocurrencies. Our framework is the first to provide generic and provably secure protocols for all these use cases while matching or improving the performance of existing use-case-specific protocols.

Atomic Transfer Graphs: Secure-by-design Protocols for Heterogeneous Blockchain Ecosystems

TL;DR

This work addresses fragmentation in blockchain ecosystems by introducing Atomic Transfer Graphs () as a unifying specification for transfers and security guarantees. It develops a transfer-tree intermediate representation () and a building block called Conditional Timelock Contracts () to realize ATGs on heterogeneous transfer agreement mechanisms (). The authors provide a formal symbolic security model, prove end-to-end security and correctness, and demonstrate practical CTLC implementations on Ethereum and Bitcoin, plus off-chain payment-channel integrations. By enabling secure-by-design cross-chain and off-chain applications (e.g., multi-hop payments, atomic swaps, crowdfunding) across TAMs, the framework offers a scalable, generic approach to protocol synthesis in heterogeneous blockchain environments. Overall, this framework unifies diverse transfer tasks under a single security- and performance-conscious design paradigm with broad applicability.

Abstract

The heterogeneity of the blockchain landscape has motivated the design of blockchain protocols tailored to specific blockchains and applications that, hence, require custom security proofs. We observe that many blockchain protocols share common security and functionality goals, which can be captured by an atomic transfer graph (ATG) describing the structure of desired transfers. Based on this observation, we contribute a framework for generating secure-by-design protocols that realize these goals. The resulting protocols build upon Conditional Timelock Contracts (CTLCs), a novel minimal smart contract functionality that can be implemented in a large variety of cryptocurrencies with a restricted scripting language (e.g., Bitcoin), and payment channels. We show how ATGs, in addition to enabling novel applications, capture the security and functionality goals of existing applications, including many examples from payment channel networks and complex multi-party cross-currency swaps among Ethereum-style cryptocurrencies. Our framework is the first to provide generic and provably secure protocols for all these use cases while matching or improving the performance of existing use-case-specific protocols.

Paper Structure

This paper contains 70 sections, 31 theorems, 372 equations, 11 figures, 3 tables.

Key Result

Theorem 2.1

Let $\mathcal{T}\xspace$ be an xtree resulting from unfolding graph $\mathcal{D}\xspace = (\mathcal{N}\xspace, \mathcal{A}\xspace)$. All outcomes $\omega \in \mathcal{O}^{\mathcal{T}}_{B}$ of $\mathcal{T}\xspace$ for honest user $B \in \mathcal{N}\xspace$ satisfy that if they contain an arc $(B, X)

Figures (11)

  • Figure 1: Applications covered by our work can be specified as an ATG (gray box on top) and then, using our framework, synthesized into a protocol involving different transfer agreement mechanisms (e.g., blockchains or PCs). In ATGs, square boxes represent users, and arcs represent transfers. Round, colored boxes indicate PCs, and hexagons indicate a blockchain.
  • Figure 2: Two-party atomic swap protocol.
  • Figure 3: A two-party atomic swap as a round-based game. The black arrow indicates the current round. Players eligible to make a move are indicated by a square. Arrows with a black border indicate pulled edges; arrows without borders indicate available edges, and grayed-out arrows indicate disabled edges. The top picture depicts the game during an honest execution, and the lower picture depicts the game during an execution involving malicious user A.
  • Figure 4: Tree unfolding of the three-party graph in the top right. Edge numbers are given in pre-order and just serve to identify the edges. Duplicated edges are depicted in the same color. Player A is enclosed in a square to indicate that they will be the first player to make a move in the game.
  • Figure 5: Honest execution of the game tree in \ref{['fig:three-party-tree']}. Execution states are depicted with the symbols in \ref{['fig:two-party-game']}.
  • ...and 6 more figures

Theorems & Definitions (81)

  • Theorem 2.1: Xtree Security (informal)
  • Theorem 2.2: Protocol Security (Informal)
  • Definition 3.1: Tree unfolding
  • Definition 3.2: Outcome Set
  • Theorem 3.3: Security of Tree Unfolding
  • Theorem 3.4: Correctness of Tree Unfolding
  • Definition 4.1: Xtree to CTLC conversion
  • Theorem 4.2: Protocol Security
  • Theorem 4.3: Protocol Correctness
  • Definition D.1
  • ...and 71 more