7 Search Results for "Bracciali, Andrea"


Document
Foundations of Fiat-Denominated Loans Collateralized by Cryptocurrencies

Authors: Pavel Hubáček, Jan Václavek, and Michelle Yeo

Published in: LIPIcs, Volume 361, 29th International Conference on Principles of Distributed Systems (OPODIS 2025)


Abstract
The rising importance of cryptocurrencies as financial assets pushed their applicability from an object of speculation closer to standard financial instruments such as loans. In this work, we initiate the study of secure protocols that enable fiat-denominated loans collateralized by cryptocurrencies such as Bitcoin. We provide limited-custodial protocols for such loans relying only on trusted arbitration and provide their game-theoretical analysis. We also highlight various interesting directions for future research.

Cite as

Pavel Hubáček, Jan Václavek, and Michelle Yeo. Foundations of Fiat-Denominated Loans Collateralized by Cryptocurrencies. In 29th International Conference on Principles of Distributed Systems (OPODIS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 361, pp. 6:1-6:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)


Copy BibTex To Clipboard

@InProceedings{hubacek_et_al:LIPIcs.OPODIS.2025.6,
  author =	{Hub\'{a}\v{c}ek, Pavel and V\'{a}clavek, Jan and Yeo, Michelle},
  title =	{{Foundations of Fiat-Denominated Loans Collateralized by Cryptocurrencies}},
  booktitle =	{29th International Conference on Principles of Distributed Systems (OPODIS 2025)},
  pages =	{6:1--6:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-409-3},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{361},
  editor =	{Arusoaie, Andrei and Onica, Emanuel and Spear, Michael and Tucci-Piergiovanni, Sara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.OPODIS.2025.6},
  URN =		{urn:nbn:de:0030-drops-251796},
  doi =		{10.4230/LIPIcs.OPODIS.2025.6},
  annote =	{Keywords: Blockchains, Cryptocurrencies, DeFi, Loans, Mechanism design, Subgame Perfect Equilibrium, Rational analysis}
}
Document
pod: An Optimal-Latency, Censorship-Free, and Accountable Generalized Consensus Layer

Authors: Orestis Alpos, Bernardo David, Jakov Mitrovski, Odysseas Sofikitis, and Dionysis Zindros

Published in: LIPIcs, Volume 356, 39th International Symposium on Distributed Computing (DISC 2025)


Abstract
This work addresses the inherent issues of high latency in blockchains and low scalability in traditional consensus protocols. We present pod, a novel notion of consensus whose first priority is to achieve the physically-optimal latency of 2δ, or one round-trip, i.e., requiring only one network trip (duration δ) for writing a transaction and one for reading it. To accomplish this, we first eliminate inter-replica communication. Instead, clients send transactions directly to all replicas, which independently process transactions and append them to local logs. Replicas assign a timestamp and a sequence number to each transaction in their logs, allowing clients to extract valuable metadata about the transactions and the system state. Later on, clients retrieve these logs and extract transactions (and associated metadata) from them. Necessarily, this construction achieves weaker properties than a total-order broadcast protocol, due to existing lower bounds. Our work models the primitive of pod and defines its security properties. We then show pod-core, a protocol that satisfies properties such as transaction confirmation within 2δ, censorship resistance against Byzantine replicas, and accountability for safety violations. We show that single-shot auctions can be realized using the pod notion and observe that it is also sufficient for other popular applications.

Cite as

Orestis Alpos, Bernardo David, Jakov Mitrovski, Odysseas Sofikitis, and Dionysis Zindros. pod: An Optimal-Latency, Censorship-Free, and Accountable Generalized Consensus Layer. In 39th International Symposium on Distributed Computing (DISC 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 356, pp. 4:1-4:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)


Copy BibTex To Clipboard

@InProceedings{alpos_et_al:LIPIcs.DISC.2025.4,
  author =	{Alpos, Orestis and David, Bernardo and Mitrovski, Jakov and Sofikitis, Odysseas and Zindros, Dionysis},
  title =	{{pod: An Optimal-Latency, Censorship-Free, and Accountable Generalized Consensus Layer}},
  booktitle =	{39th International Symposium on Distributed Computing (DISC 2025)},
  pages =	{4:1--4:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-402-4},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{356},
  editor =	{Kowalski, Dariusz R.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2025.4},
  URN =		{urn:nbn:de:0030-drops-248219},
  doi =		{10.4230/LIPIcs.DISC.2025.4},
  annote =	{Keywords: consensus, censorship resistance, accountability, auctions}
}
Document
4-Swap: Achieving Grief-Free and Bribery-Safe Atomic Swaps Using Four Transactions

Authors: Kirti Singh, Vinay J. Ribeiro, and Susmita Mandal

Published in: LIPIcs, Volume 354, 7th Conference on Advances in Financial Technologies (AFT 2025)


Abstract
Cross-chain asset exchange is crucial for blockchain interoperability. Existing solutions rely on trusted third parties and risk asset loss, or use decentralized alternatives like atomic swaps, which suffer from grief attacks. Griefing occurs when a party prematurely exits, locking the counterparty’s assets until a timelock expires. Hedged Atomic Swaps mitigate griefing by introducing a penalty premium; however, they increase the number of transactions from four (as in Tier Nolan’s swap) to six, which in turn introduces new griefing risks. Grief-Free (GF) Swap reduces this to five transactions by consolidating assets and premiums on a single chain. However, no existing protocol achieves grief-free asset exchange in just four transactions. This paper presents 4-Swap, the first cross-chain atomic swap protocol that is both grief-free and bribery-safe, while completing asset exchange in just four transactions. By combining the griefing premium and principal into a single transaction per chain, 4-Swap reduces on-chain transactions, leading to faster execution compared to previous grief-free solutions. It is fully compatible with Bitcoin and operates without the need for any new opcodes. A game-theoretic analysis shows that rational participants have no incentive to deviate from the protocol, ensuring robust compliance and security.

Cite as

Kirti Singh, Vinay J. Ribeiro, and Susmita Mandal. 4-Swap: Achieving Grief-Free and Bribery-Safe Atomic Swaps Using Four Transactions. In 7th Conference on Advances in Financial Technologies (AFT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 354, pp. 32:1-32:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)


Copy BibTex To Clipboard

@InProceedings{singh_et_al:LIPIcs.AFT.2025.32,
  author =	{Singh, Kirti and Ribeiro, Vinay J. and Mandal, Susmita},
  title =	{{4-Swap: Achieving Grief-Free and Bribery-Safe Atomic Swaps Using Four Transactions}},
  booktitle =	{7th Conference on Advances in Financial Technologies (AFT 2025)},
  pages =	{32:1--32:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-400-0},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{354},
  editor =	{Avarikioti, Zeta and Christin, Nicolas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.AFT.2025.32},
  URN =		{urn:nbn:de:0030-drops-247514},
  doi =		{10.4230/LIPIcs.AFT.2025.32},
  annote =	{Keywords: Atomic Swaps, Griefing, Bribery, HTLC}
}
Document
Money in Motion: Micro‑Velocity and Usage of Ethereum’s Liquid Staking Tokens

Authors: Benjamin Kraner, Luca Pennella, Nicolò Vallarano, and Claudio J. Tessone

Published in: LIPIcs, Volume 354, 7th Conference on Advances in Financial Technologies (AFT 2025)


Abstract
We introduce a micro-velocity framework for analysing the on-chain circulation of Lido’s liquid-staking tokens, stETH, and its wrapped ERC-20 form, wstETH. By reconstructing full transfer and share-based accounting histories, we compute address-level velocities and decompose them into behavioural components. Despite their growing importance, the micro-level monetary dynamics of LSTs remain largely unexplored. Our data reveal persistently high velocity for both tokens, reflecting intensive reuse within DeFi. Yet activity is highly concentrated: a small cohort of large addresses, likely institutional accounts, are responsible for most turnover, while the rest of the users remain largely passive. We also observe a gradual transition in user behavior, characterized by a shift toward wstETH, the non-rebasing variant of stETH. This shift appears to align with DeFi composability trends, as wstETH is more frequently deployed across protocols such as AAVE, Spark, Balancer, and SkyMoney. To make the study fully reproducible, we release (i) an open-source pipeline that indexes event logs and historical contract state, and (ii) two public datasets containing every Transfer and TransferShares record for stETH and wstETH through 2024-11-08. This is the first large-scale empirical characterisation of liquid-staking token circulation. Our approach offers a scalable template for monitoring staking asset flows and provides new, open-access resources to the research community.

Cite as

Benjamin Kraner, Luca Pennella, Nicolò Vallarano, and Claudio J. Tessone. Money in Motion: Micro‑Velocity and Usage of Ethereum’s Liquid Staking Tokens. In 7th Conference on Advances in Financial Technologies (AFT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 354, pp. 9:1-9:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)


Copy BibTex To Clipboard

@InProceedings{kraner_et_al:LIPIcs.AFT.2025.9,
  author =	{Kraner, Benjamin and Pennella, Luca and Vallarano, Nicol\`{o} and Tessone, Claudio J.},
  title =	{{Money in Motion: Micro‑Velocity and Usage of Ethereum’s Liquid Staking Tokens}},
  booktitle =	{7th Conference on Advances in Financial Technologies (AFT 2025)},
  pages =	{9:1--9:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-400-0},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{354},
  editor =	{Avarikioti, Zeta and Christin, Nicolas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.AFT.2025.9},
  URN =		{urn:nbn:de:0030-drops-247285},
  doi =		{10.4230/LIPIcs.AFT.2025.9},
  annote =	{Keywords: DeFi, Ethereum, Proof-of-Stake, Liquid Staking, Money Velocity, Inflation}
}
Document
Program Logics for Ledgers

Authors: Orestis Melkonian, Wouter Swierstra, and James Chapman

Published in: OASIcs, Volume 129, 6th International Workshop on Formal Methods for Blockchains (FMBC 2025)


Abstract
Distributed ledgers nowadays manage substantial monetary funds in the form of cryptocurrencies such as Bitcoin, Ethereum, and Cardano. For such ledgers to be safe, operations that add new entries must be cryptographically sound - but it is less clear how to reason effectively about such ever-growing linear data structures. This paper demonstrates how distributed ledgers may be viewed as computer programs, that, when executed, transfer funds between various parties. As a result, familiar program logics, such as Hoare logic, are applied in a novel setting. Borrowing ideas from concurrent separation logic, this enables modular reasoning principles over arbitrary fragments of any ledger. All of our results have been mechanised in the Agda proof assistant.

Cite as

Orestis Melkonian, Wouter Swierstra, and James Chapman. Program Logics for Ledgers. In 6th International Workshop on Formal Methods for Blockchains (FMBC 2025). Open Access Series in Informatics (OASIcs), Volume 129, pp. 10:1-10:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)


Copy BibTex To Clipboard

@InProceedings{melkonian_et_al:OASIcs.FMBC.2025.10,
  author =	{Melkonian, Orestis and Swierstra, Wouter and Chapman, James},
  title =	{{Program Logics for Ledgers}},
  booktitle =	{6th International Workshop on Formal Methods for Blockchains (FMBC 2025)},
  pages =	{10:1--10:22},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-371-3},
  ISSN =	{2190-6807},
  year =	{2025},
  volume =	{129},
  editor =	{Marmsoler, Diego and Xu, Meng},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2025.10},
  URN =		{urn:nbn:de:0030-drops-230370},
  doi =		{10.4230/OASIcs.FMBC.2025.10},
  annote =	{Keywords: blockchain, distributed ledgers, UTxO separation logic, program semantics, formal verification, Agda}
}
Document
Formal Verification of a Fail-Safe Cross-Chain Bridge

Authors: Filip Marić, Bernhard Scholz, and Pavle Subotić

Published in: OASIcs, Volume 129, 6th International Workshop on Formal Methods for Blockchains (FMBC 2025)


Abstract
Cross-chain bridges are financial services that interconnect blockchains. High monetary values flow through these bridges, and their security must be safeguarded. However, designing real-world cross-chain bridges is a difficult endeavor. Due to blockchain’s closed-world nature, tokens cannot be transferred from a sender to a receiver chain; on the contrary, they need complex logic that maintains an equilibrium on both chains, even if either the chains or the bridge fail. This paper formally verifies a model of a novel fail-safe cross-chain bridge to ensure correctness. We define formal requirements and prove the bridge is safe using the Isabelle/HOL proof assistant.

Cite as

Filip Marić, Bernhard Scholz, and Pavle Subotić. Formal Verification of a Fail-Safe Cross-Chain Bridge. In 6th International Workshop on Formal Methods for Blockchains (FMBC 2025). Open Access Series in Informatics (OASIcs), Volume 129, pp. 8:1-8:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)


Copy BibTex To Clipboard

@InProceedings{maric_et_al:OASIcs.FMBC.2025.8,
  author =	{Mari\'{c}, Filip and Scholz, Bernhard and Suboti\'{c}, Pavle},
  title =	{{Formal Verification of a Fail-Safe Cross-Chain Bridge}},
  booktitle =	{6th International Workshop on Formal Methods for Blockchains (FMBC 2025)},
  pages =	{8:1--8:18},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-371-3},
  ISSN =	{2190-6807},
  year =	{2025},
  volume =	{129},
  editor =	{Marmsoler, Diego and Xu, Meng},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2025.8},
  URN =		{urn:nbn:de:0030-drops-230342},
  doi =		{10.4230/OASIcs.FMBC.2025.8},
  annote =	{Keywords: Cross-Chain Bridge, Formal Verification, Logic, Security}
}
Document
Decentralization in Open Quorum Systems: Limitative Results for Ripple and Stellar

Authors: Andrea Bracciali, Davide Grossi, and Ronald de Haan

Published in: OASIcs, Volume 82, 2nd International Conference on Blockchain Economics, Security and Protocols (Tokenomics 2020)


Abstract
Decentralisation is one of the promises introduced by blockchain technologies: fair and secure interaction amongst peers with no dominant positions, single points of failure or censorship. Decentralisation, however, appears difficult to be formally defined, possibly a continuum property of systems that can be more or less decentralised, or can tend to decentralisation in their lifetime. In this paper we focus on decentralisation in quorum-based approaches to open (permissionless) consensus as illustrated in influential protocols such as the Ripple and Stellar protocols. Drawing from game theory and computational complexity, we establish limiting results concerning the decentralisation vs. safety trade-off in Ripple and Stellar, and we propose a novel methodology to formalise and quantitatively analyse decentralisation in this type of blockchains.

Cite as

Andrea Bracciali, Davide Grossi, and Ronald de Haan. Decentralization in Open Quorum Systems: Limitative Results for Ripple and Stellar. In 2nd International Conference on Blockchain Economics, Security and Protocols (Tokenomics 2020). Open Access Series in Informatics (OASIcs), Volume 82, pp. 5:1-5:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{bracciali_et_al:OASIcs.Tokenomics.2020.5,
  author =	{Bracciali, Andrea and Grossi, Davide and de Haan, Ronald},
  title =	{{Decentralization in Open Quorum Systems: Limitative Results for Ripple and Stellar}},
  booktitle =	{2nd International Conference on Blockchain Economics, Security and Protocols (Tokenomics 2020)},
  pages =	{5:1--5:20},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-157-3},
  ISSN =	{2190-6807},
  year =	{2021},
  volume =	{82},
  editor =	{Anceaume, Emmanuelle and Bisi\`{e}re, Christophe and Bouvard, Matthieu and Bramas, Quentin and Casamatta, Catherine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.Tokenomics.2020.5},
  URN =		{urn:nbn:de:0030-drops-135277},
  doi =		{10.4230/OASIcs.Tokenomics.2020.5},
  annote =	{Keywords: Blockchain, decentralization, game theory, computational complexity}
}
  • Refine by Type
  • 7 Document/PDF
  • 6 Document/HTML

  • Refine by Publication Year
  • 1 2026
  • 5 2025
  • 1 2021

  • Refine by Author
  • 1 Alpos, Orestis
  • 1 Bracciali, Andrea
  • 1 Chapman, James
  • 1 David, Bernardo
  • 1 Grossi, Davide
  • Show More...

  • Refine by Series/Journal
  • 4 LIPIcs
  • 3 OASIcs

  • Refine by Classification
  • 2 Security and privacy → Distributed systems security
  • 1 Applied computing → Economics
  • 1 Applied computing → Electronic commerce
  • 1 Computer systems organization → Dependable and fault-tolerant systems and networks
  • 1 Computer systems organization → Distributed architectures
  • Show More...

  • Refine by Keyword
  • 2 DeFi
  • 1 Agda
  • 1 Atomic Swaps
  • 1 Blockchain
  • 1 Blockchains
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail