Crossing with Confidence: Formal Analysis and Model Checking of Blockchain Bridges

Paper 2026/292

Crossing with Confidence: Formal Analysis and Model Checking of Blockchain Bridges

Pyrros Chaidos

, Input Output, National and Kapodistrian University of Athens

Pooya Farshim

, Input Output

Denis Firsov

, Input Output

Dimitar Jetchev

, Input Output, Microsoft

Aggelos Kiayias

, University of Edinburgh, Input Output

Markulf Kohlweiss

, University of Edinburgh, Input Output

Anca Nitulescu

, Input Output

Abstract

We develop formal code-based security definitions for blockchain bridges and apply them to several bridge architectures deployed in practice. We derive both traditional pen-and-paper proofs and on the other, automated guarantees against bounded counterexamples. The latter is achieved via bounded model checking of our formally specified properties, implemented in Quint, a specification language and model checker closely related to TLA+. Our definitions are expressed in a precise, code-based variant of the Universal Composition (UC) framework. This enables the modular use of hybrid functionalities—even for property-based definitions—and is essential for bounded model checking, where underlying primitives must be idealized. Accordingly, we idealize and model-check all building blocks used in our protocols. Notably, we formulate a novel UC ideal functionality for Advanced Threshold Signatures (ATS) and modelcheck it for attacks to ensure its robustness

Note: small editorial and text formatting update

Metadata

Available format(s): PDF
Category: Cryptographic protocols
Publication info: Preprint.
Keywords: Formal Security Universal Composition Model Checking Blockchain Bridges Advanced Threshold Signatures
Contact author(s): pyrros chaidos @ iohk io
pooya farshim @ iohk io
denis firsov @ iohk io
dimitar jetchev @ iohk io
akiayias @ inf ed ac uk
markulf kohlweiss @ iohk io
anca nitulescu @ iohk io
History: 2026-02-24: last of 2 revisions; 2026-02-17: received; See all versions
Short URL: https://ia.cr/2026/292
License: CC BY

BibTeX

@misc{cryptoeprint:2026/292,
      author = {Pyrros Chaidos and Pooya Farshim and Denis Firsov and Dimitar Jetchev and Aggelos Kiayias and Markulf Kohlweiss and Anca Nitulescu},
      title = {Crossing with Confidence: Formal Analysis and Model Checking of Blockchain Bridges},
      howpublished = {Cryptology {ePrint} Archive, Paper 2026/292},
      year = {2026},
      url = {https://eprint.iacr.org/2026/292}
}