Towards secure and trustful cryptographic currencies and consensus ledgers

The project addresses the problems of an emerging (and highly problematic) field of cryptographic currencies and consensus ledgers, commonly referred to as blockchains. Following the original on-line publication of the Bitcoin paper, this field grows fast but often bypasses the peer-reviewing of scientic publishing. On the one side, the on-line innovations produced a lot of exciting prototypes and a world-wide recognition of cryptocurrency. On the other side, this has led to deficits in systematization and poses security and safety problems already being exploited by criminals.This project aims to significantly narrow this gap with a well-structured approach for modeling and validation of cryptocurrencies and blockchains. In particular, we propose a generalised formal modeling approach which on the one hand would provide a platform for systematic design of blockchain aspects and on the other hand which would enable mathematical proving of the behavior of cryptographic puzzles, as well as their interaction with peer-to-peer communication protocols - the main safety and security critical components of blockchains.The project will be a collaborative effort between members of the Centre for Cryptocurrency Research and Engineering (CCRE) at Imperial College, London, UK and the experts in formal modeling and program analysis from USI.