6 Search Results for "Bisière, Christophe"

Volume

OASIcs, Volume 82

2nd International Conference on Blockchain Economics, Security and Protocols (Tokenomics 2020)

Tokenomics 2020, October 26-27, 2020, Toulouse, France

Editors: Emmanuelle Anceaume, Christophe Bisière, Matthieu Bouvard, Quentin Bramas, and Catherine Casamatta

Document
DOI: 10.4230/OASIcs.FMBC.2025.10
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
DOI: 10.4230/LIPIcs.OPODIS.2024.7
Incentive Compatibility of Ethereum’s PoS Consensus Protocol

Authors: Ulysse Pavloff, Yackolley Amoussou-Guenou, and Sara Tucci-Piergiovanni

Published in: LIPIcs, Volume 324, 28th International Conference on Principles of Distributed Systems (OPODIS 2024)

Abstract
This paper investigates whether following the fork-choice rule in the Ethereum PoS consensus protocol constitutes a Nash equilibrium - i.e., whether the protocol that maintains the canonical chain in Ethereum is incentive-compatible. Specifically, we explore whether selfish participants may attempt to manipulate the fork-choice rule by forking out previous blocks and capturing the rewards associated with those blocks. Our analysis considers two strategies for participants: the obedient strategy, which adheres to the prescribed protocol, and the cunning strategy, which attempts to manipulate the fork-choice rule to gain more rewards. We evaluate the conditions under which selfish participants might deviate from the obedient strategy. We found that, in a synchronous system, following the prescribed fork-choice rule is incentive-compatible. However, in an eventually synchronous system, the protocol is eventually incentive-compatible - that is, only a limited number of proposers will find it profitable to fork the chain during the synchronous period. After this sequence of cunning proposers, subsequent proposers will find it more profitable to follow the protocol.
Cite as

Ulysse Pavloff, Yackolley Amoussou-Guenou, and Sara Tucci-Piergiovanni. Incentive Compatibility of Ethereum’s PoS Consensus Protocol. In 28th International Conference on Principles of Distributed Systems (OPODIS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 324, pp. 7:1-7:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{pavloff_et_al:LIPIcs.OPODIS.2024.7,
  author =	{Pavloff, Ulysse and Amoussou-Guenou, Yackolley and Tucci-Piergiovanni, Sara},
  title =	{{Incentive Compatibility of Ethereum’s PoS Consensus Protocol}},
  booktitle =	{28th International Conference on Principles of Distributed Systems (OPODIS 2024)},
  pages =	{7:1--7:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-360-7},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{324},
  editor =	{Bonomi, Silvia and Galletta, Letterio and Rivi\`{e}re, Etienne and Schiavoni, Valerio},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.OPODIS.2024.7},
  URN =		{urn:nbn:de:0030-drops-225431},
  doi =		{10.4230/LIPIcs.OPODIS.2024.7},
  annote =	{Keywords: Ethereum PoS, Game Theory, Block Reward}
}
Document
Complete Volume
DOI: 10.4230/OASIcs.Tokenomics.2020
OASIcs, Volume 82, Tokenomics 2020, Complete Volume

Authors: Emmanuelle Anceaume, Christophe Bisière, Matthieu Bouvard, Quentin Bramas, and Catherine Casamatta

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

Abstract
OASIcs, Volume 82, Tokenomics 2020, Complete Volume
Cite as

2nd International Conference on Blockchain Economics, Security and Protocols (Tokenomics 2020). Open Access Series in Informatics (OASIcs), Volume 82, pp. 1-136, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@Proceedings{anceaume_et_al:OASIcs.Tokenomics.2020,
  title =	{{OASIcs, Volume 82, Tokenomics 2020, Complete Volume}},
  booktitle =	{2nd International Conference on Blockchain Economics, Security and Protocols (Tokenomics 2020)},
  pages =	{1--136},
  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},
  URN =		{urn:nbn:de:0030-drops-135213},
  doi =		{10.4230/OASIcs.Tokenomics.2020},
  annote =	{Keywords: OASIcs, Volume 82, Tokenomics 2020, Complete Volume}
}
Document
Front Matter
DOI: 10.4230/OASIcs.Tokenomics.2020.0
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Emmanuelle Anceaume, Christophe Bisière, Matthieu Bouvard, Quentin Bramas, and Catherine Casamatta

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

Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as

2nd International Conference on Blockchain Economics, Security and Protocols (Tokenomics 2020). Open Access Series in Informatics (OASIcs), Volume 82, pp. 0:i-0:x, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{anceaume_et_al:OASIcs.Tokenomics.2020.0,
  author =	{Anceaume, Emmanuelle and Bisi\`{e}re, Christophe and Bouvard, Matthieu and Bramas, Quentin and Casamatta, Catherine},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{2nd International Conference on Blockchain Economics, Security and Protocols (Tokenomics 2020)},
  pages =	{0:i--0:x},
  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.0},
  URN =		{urn:nbn:de:0030-drops-135220},
  doi =		{10.4230/OASIcs.Tokenomics.2020.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
DOI: 10.4230/OASIcs.Gabbrielli.2
A Formal Analysis of the Bitcoin Protocol

Authors: Cosimo Laneve and Adele Veschetti

Published in: OASIcs, Volume 86, Recent Developments in the Design and Implementation of Programming Languages (2020)

Abstract
We study Nakamoto’s Bitcoin protocol that implements a distributed ledger on peer-to-peer asynchronous networks. In particular, we define a principled formal model of key participants - the miners - as stochastic processes and describe the whole system as a parallel composition of miners. We therefore compute the probability that ledgers turn into a state with more severe inconsistencies, e.g. with longer forks, under the assumptions that messages are not lost and nodes are not hostile. We also study how the presence of hostile nodes mining blocks in wrong positions impacts on the consistency of the ledgers. Our theoretical results agree with the simulations performed on a probabilistic model checker that we extended with dynamic datatypes in order to have a faithful description of miners' behaviour.
Cite as

Cosimo Laneve and Adele Veschetti. A Formal Analysis of the Bitcoin Protocol. In Recent Developments in the Design and Implementation of Programming Languages. Open Access Series in Informatics (OASIcs), Volume 86, pp. 2:1-2:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{laneve_et_al:OASIcs.Gabbrielli.2,
  author =	{Laneve, Cosimo and Veschetti, Adele},
  title =	{{A Formal Analysis of the Bitcoin Protocol}},
  booktitle =	{Recent Developments in the Design and Implementation of Programming Languages},
  pages =	{2:1--2:17},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-171-9},
  ISSN =	{2190-6807},
  year =	{2020},
  volume =	{86},
  editor =	{de Boer, Frank S. and Mauro, Jacopo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.Gabbrielli.2},
  URN =		{urn:nbn:de:0030-drops-132242},
  doi =		{10.4230/OASIcs.Gabbrielli.2},
  annote =	{Keywords: Bitcoin, Distributed consensus, Distributed ledgers, Blockchain, PRISM, forks}
}
  • Refine by Type
  • 5 Document/PDF
  • 2 Document/HTML
  • 1 Volume

  • Refine by Publication Year
  • 2 2025
  • 3 2021
  • 1 2020

  • Refine by Author
  • 2 Anceaume, Emmanuelle
  • 2 Bisière, Christophe
  • 2 Bouvard, Matthieu
  • 2 Bramas, Quentin
  • 2 Casamatta, Catherine
  • Show More...

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

  • Refine by Classification
  • 2 Applied computing → Economics
  • 2 Computing methodologies → Distributed algorithms
  • 2 Security and privacy → Distributed systems security
  • 1 Computer systems organization → Dependable and fault-tolerant systems and networks
  • 1 Theory of computation → Distributed algorithms
  • Show More...

  • Refine by Keyword
  • 1 Agda
  • 1 Bitcoin
  • 1 Block Reward
  • 1 Blockchain
  • 1 Conference Organization
  • 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
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact