Paper 2026/292 Original: eprint.iacr.org/2026/292 ↗
Crossing with Confidence: Formal Analysis and Model Checking of Blockchain Bridges
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
Metadata
- Available format(s)
PDF- Category
- Cryptographic protocols
- Publication info
- Preprint.
- History
- 2026-02-24: last updated
- 2026-02-17: published
- Short URL
- https://ia.cr/2026/292
- License
- https://creativecommons.org/licenses/by/4.0/
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}
}