Aarhus University Seal

Formalizing Nakamoto-Style Proof of Stake

Research output: Contribution to book/anthology/report/proceedingArticle in proceedingsResearchpeer-review

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 imply both safety and liveness.

Original languageEnglish
Title of host publicationProceedings - 2021 IEEE 34th Computer Security Foundations Symposium, CSF 2021
Number of pages15
Publication year2021
ISBN (Electronic)978-1-7281-7607-9
Publication statusPublished - 2021
Event34th IEEE Computer Security Foundations Symposium - Virtual, Online, United States
Duration: 21 Jun 202125 Jun 2021
Conference number: 34


Conference34th IEEE Computer Security Foundations Symposium
LandUnited States

See relations at Aarhus University Citationformats

ID: 227594886