Such mathematical specifications are important, as cryptography is a very slippery business where the tiniest mistake can lead to loss of all security.  It is therefore crucial that cryptographic protocols are proven secure. There are different levels of what it means to be proven secure. In cryptography, one often uses an informal mathematical argument. These informal arguments occasionally miss corner cases in the proof. So, a detailed tedious mathematical proof is needed. Tedious tasks are often better done with the help of computers. At Aarhus University, we have been working on the use of computer proof assistants to facilitate this tedious task to reduce informal proofs to the logical axioms. In this way we obtain the highest standard of rigour. Such a proof does not only help to show the absence of accidental errors, it also allows one to accept a protocol from a possibly malicious party, as the proofs can be automatically checked.

Importantly, cryptographers often only give proofs of security of abstract protocols, but in the end, what matters is the running code. Computer proof assistants allow one to refine the protocol into a prototype implementation/executable specification, and even into efficient running code. There has been a lot of progress in the academic community, developing proof assistants. This is now slowly being taken up by the industry for cases where security is crucial, such as the design of hardware, or in critical infrastructure. Blockchain is such an example, where security is crucial and the stakes are high. We are doing basic research in developing these tools for the blockchain space. This includes modeling cryptographic frameworks for modularly composable protocols. The security proof of a blockchain will be built up from composable building blocks, such as the P2P-layer, the consensus protocol, the transactor layer, etc. These mathematical models are both being built in the crypto community and in the programming language community. We do research on bringing them together.