DROPS

Document

DOI: 10.4230/OASIcs.FMBC.2020.9

On the Formal Verification of the Stellar Consensus Protocol

Authors: Giuliano Losa and Mike Dodds

Published in: OASIcs, Volume 84, 2nd Workshop on Formal Methods for Blockchains (FMBC 2020)

Abstract

The Stellar Consensus Protocol (SCP) is a quorum-based BFT consensus protocol. However, instead of using threshold-based quorums, SCP is permissionless and its quorum system emerges from participants’ self-declared trust relationships. In this paper, we describe the methodology we deploy to formally verify the safety and liveness of SCP for arbitrary but fixed configurations. The proof uses a combination of Ivy and Isabelle/HOL. In Ivy, we model SCP in first-order logic, and we verify safety and liveness under eventual synchrony. In Isabelle/HOL, we prove the validity of our first-order encoding with respect to a more direct higher-order model. SCP is currently deployed in the Stellar Network, and we believe this is the first mechanized proof of both safety and liveness, specified in LTL, for a deployed BFT protocol.

Cite as

Giuliano Losa and Mike Dodds. On the Formal Verification of the Stellar Consensus Protocol. In 2nd Workshop on Formal Methods for Blockchains (FMBC 2020). Open Access Series in Informatics (OASIcs), Volume 84, pp. 9:1-9:9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{losa_et_al:OASIcs.FMBC.2020.9,
  author =	{Losa, Giuliano and Dodds, Mike},
  title =	{{On the Formal Verification of the Stellar Consensus Protocol}},
  booktitle =	{2nd Workshop on Formal Methods for Blockchains (FMBC 2020)},
  pages =	{9:1--9:9},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-169-6},
  ISSN =	{2190-6807},
  year =	{2020},
  volume =	{84},
  editor =	{Bernardo, Bruno and Marmsoler, Diego},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2020.9},
  URN =		{urn:nbn:de:0030-drops-134226},
  doi =		{10.4230/OASIcs.FMBC.2020.9},
  annote =	{Keywords: Consensus, Blockchains, First-Order Logic, Stellar, Ivy Prover, Decidability}
}

Search Results

Documents authored by Dodds, Mike

On the Formal Verification of the Stellar Consensus Protocol

Abstract

Cite as

Thanks for your feedback!

Could not send message