A logic of blockchain updates

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 BCL⁠, a dynamic logic to reason about blockchain updates, and show that BCL is sound and complete with respect to a simple blockchain model.