Paper 2020/917

Formalizing Nakamoto-Style Proof of Stake

Søren Eller Thomsen and Bas Spitters

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.

Metadata
Available format(s)
PDF
Publication info
Preprint. MINOR revision.
Keywords
blockchainformal methods
Contact author(s)
sethomsen @ cs au dk
spitters @ cs au dk
History
2021-06-11: revised
2020-07-26: received
See all versions
Short URL
https://ia.cr/2020/917
License
Creative Commons Attribution
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},
      note = {\url{https://eprint.iacr.org/2020/917}},
      url = {https://eprint.iacr.org/2020/917}
}
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.