Paper 2026/983 Original: eprint.iacr.org/2026/983 ↗
A formal analysis of FLEX and FLEX2
Abstract
This paper formalizes the cryptographic core of the FLEX protocol and its enhanced variation FLEX2 . The analysis formalizes a minimal ledger abstraction, capturing Taproot, CSV timelocks, and reorg bounds, and defines ideal functionalities implemented as transaction-DAG and state machines. Main contributions include proving on-chain enforceability, CDS secrecy, soundness, leakage-bounded privacy, and universal composability realization under standard assumptions.
Metadata
- Available format(s)
PDF- Category
- Cryptographic protocols
- Publication info
- Preprint.
- History
- 2026-05-21: last updated
- 2026-05-18: published
- Short URL
- https://ia.cr/2026/983
- License
- https://creativecommons.org/licenses/by/4.0/
BibTeX
@misc{cryptoeprint:2026/983,
author = {Ramses Fernandez},
title = {A formal analysis of FLEX and FLEX2},
howpublished = {Cryptology {ePrint} Archive, Paper 2026/983},
year = {2026},
url = {https://eprint.iacr.org/2026/983}
}