A Logic of Blockchain Updates

Abstract

Abstract Blockchains are distributed data structures that are used to achieve consensus in systems for cryptocurrencies (like Bitcoin) or smart contracts (like Ethereum). Although blockchains gained a lot of popularity recently, there are only few logic-based models for blockchains available. We introduce $\mathsf{BCL}$, a dynamic logic to reason about blockchain updates, and show that $\mathsf{BCL}$ is sound and complete with respect to a simple blockchain model.