Formalizing Nakamoto-Style Proof of Stake

Søren Eller Thomsen, Bas Spitters

Publikation: Bidrag til bog/antologi/rapport/proceedingKonferencebidrag i proceedingsForskningpeer review

15 Citationer (Scopus)

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

OriginalsprogEngelsk
TitelProceedings - 2021 IEEE 34th Computer Security Foundations Symposium, CSF 2021
Antal sider15
ForlagIEEE
Publikationsdato2021
ISBN (Elektronisk)978-1-7281-7607-9
DOI
StatusUdgivet - 2021
Begivenhed34th IEEE Computer Security Foundations Symposium - Virtual, Online, USA
Varighed: 21 jun. 202125 jun. 2021
Konferencens nummer: 34
https://www.ieee-security.org/TC/CSF2021/

Konference

Konference34th IEEE Computer Security Foundations Symposium
Nummer34
LokationVirtual
Land/OmrådeUSA
ByOnline
Periode21/06/202125/06/2021
Internetadresse

Fingeraftryk

Dyk ned i forskningsemnerne om 'Formalizing Nakamoto-Style Proof of Stake'. Sammen danner de et unikt fingeraftryk.

Citationsformater