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.
Originalsprog | Engelsk |
---|---|
Titel | Proceedings - 2021 IEEE 34th Computer Security Foundations Symposium, CSF 2021 |
Antal sider | 15 |
Forlag | IEEE |
Publikationsdato | 2021 |
ISBN (Elektronisk) | 978-1-7281-7607-9 |
DOI | |
Status | Udgivet - 2021 |
Begivenhed | 34th IEEE Computer Security Foundations Symposium - Virtual, Online, USA Varighed: 21 jun. 2021 → 25 jun. 2021 Konferencens nummer: 34 https://www.ieee-security.org/TC/CSF2021/ |
Konference
Konference | 34th IEEE Computer Security Foundations Symposium |
---|---|
Nummer | 34 |
Lokation | Virtual |
Land/Område | USA |
By | Online |
Periode | 21/06/2021 → 25/06/2021 |
Internetadresse |