Formally verifying the security properties of a proof-of-stake blockchain protocol

In 2009, Bitcoin was brought into existence, as the first real-world application of blockchain protocols, by its pseudonymous and mysterious creator, Satoshi Nakamoto. It was presented as a form of cryptocurrency, has become widely known and been recognised as the first successful E-cash since the introduction of the E-cash idea in 1983. Many more crytocurrencies including Ethereum and Tether have emerged following the success of Bitcoin. Bitcoin is secure, meaning that it satisfies persistence and liveness. Without the need of a trusted third party, it appears to prevent double-spending attacks. Bitcoin's security is obtained by the use of cryptographically secure chains of blocks for time-stamping (hence the name 'blockchain') and a technique, often called Nakamoto consensus, combined from the longest-chain rule and Proof-of-Work (PoW). Briefly, it allows and encourages all parties to participate in picking the longest chain in the system and solving a cryptographically difficult puzzle to declare the next block of transactions for that chain. PoW is sometimes referred to as a lottery system. PoW requires a majority of the computational power to be honest and it consumes a gigantic amount of energy, so it is not scalable. In the light of this problem, Proof-of-Stake (PoS) was suggested to replace PoW. PoS-based blockchain protocols, instead of using computational power, use in-system currency to agree on a new block to be added, but keep mostly everything else the same. Kiayias et al. was the first to propose a provably secure PoS-based blockchain protocol: Ouroboros. Ouroboros' security guarantees, persistence and liveness, can be verified through proving that Ouroboros satisfies three elementary properties for blockchains as proposed by Gary et al.: Common Prefix, Chain Growth, and Chain Quality. In this project, we attempt to formalise, in Isabelle/HOL, the combinatorial analysis used to prove that Ouroboros satisfies common prefix with near certainty. We cover the case of a static stake protocol under a few assumptions: the network is synchronous, the majority of the stake is honest, and the stake transfer between executions does not effect the lottery system.

Name dc:type.qualificationname

Doctor of Philosophy (PhD)

Level dc:type.qualificationlevel

Doctoral

Grantor dc:publisher.institution

University of Cambridge

Year dc:date.issued

2021

Author dc:creator

• Worrasangasilpa, Kawin

Advisor dc:contributor.advisor

• Paulson, Lawrence

• blockchain
• cryptocurrencies
• formal verification
• proof-of-stake
• theorem proving

Licence

• https://www.repository.cam.ac.uk/bitstreams/111373aa-2667-4a7e-83f6-7844b8b32dec/download
• https://www.rioxx.net/licenses/all-rights-reserved/

Language dc:language

eng

DOI dc:identifier.doi

https://doi.org/10.17863/CAM.107393

OAI identifier oai:identifier

oai:www.repository.cam.ac.uk:1810/366500