Formalizing Nakamoto-Style Proof of Stake

Søren Eller Thomsen; Bas Spitters

Paper 2020/917

Formalizing Nakamoto-Style Proof of Stake

Søren Eller Thomsen

, Aarhus University

Bas Spitters

, Aarhus University

Abstract

Fault-tolerant distributed systems move the trust in a single party to a majority of parties participating in the protocol. This makes blockchain based crypto-currencies possible: they allow parties to agree on a total order of transactions without a trusted third party. To trust a distributed system, the security of the protocol and the correctness of the implementation must be indisputable. We present the first machine checked proof that guarantees both safety and liveness for a consensus algorithm. We verify a Proof of Stake (PoS) Nakamoto-style blockchain (NSB) protocol, using the foundational proof assistant Coq. In particular, we consider a PoS NSB in a synchronous network with a static set of corrupted parties. We define execution semantics for this setting and prove chain growth, chain quality, and common prefix which together implies both safety and liveness.

Note: Publication information

Metadata

Available format(s): PDF
Publication info: Published elsewhere. 2021 IEEE 34th Computer Security Foundations Symposium (CSF)
DOI: 10.1109/CSF51468.2021.00042
Keywords: blockchain formal methods
Contact author(s): sethomsen @ cs au dk
spitters @ cs au dk
History: 2023-11-29: last of 2 revisions; 2020-07-26: received; See all versions
Short URL: https://ia.cr/2020/917
License: CC BY

BibTeX

@misc{cryptoeprint:2020/917,
      author = {Søren Eller Thomsen and Bas Spitters},
      title = {Formalizing Nakamoto-Style Proof of Stake},
      howpublished = {Cryptology {ePrint} Archive, Paper 2020/917},
      year = {2020},
      doi = {10.1109/CSF51468.2021.00042},
      url = {https://eprint.iacr.org/2020/917}
}