A structural change is required in how we reason about and evaluate novel cryptography. There is increasing interest in the usage of formal proof in the cryptographic domain, and a growing cornucopia of tools and frameworks to allow for the formal verification of cryptographic software and designs. What is required, however, is a structured approach to reasoning about the results such tools produce.

The value to a "formal proof" is an interpretation of its content into meaning; yet that meaning is not given through formal means, but through socio-technical context. There are good solutions in other problem domains to the question of how to build an assurance case effectively, and the lessons they provide can be transposed to this context. The use of a "Claims, Argument, Evidence" (CAE) assurance methodology creates a clearer space for interpreting the meaning of formal analysis and verification: if a formal proof is to be regarded as a form of evidence for the security of an implementation or design, that evidence has meaning only alongside the claims it justifies and the argument which links them to a web of justified belief.

To explain the context in a little more depth: the problem domain under consideration is "novel cryptography", by which is meant cryptographic designs and their implementations which are in some sense new, but which address well-defined needs. The most recent archetypal example of this is the so-called NIST post-quantum standardization process, which has occurred over the last half-decade. This process was designed to select quantum-computing-secure key encapsulation mechanisms and digital signature scheme to be standardized.

Despite optimism from the developers and researchers of formal verification technology, by and large these tools and methods have not played an explicit role in the evaluation and winnowing of the schemes considered by NIST, despite a clear need to improve the quality of offered implementations. That is to say: the tools are available, in principle they could prove evidence in support of the schemes under consideration, but in practice this has not been presented or required.

The issue is not the technology itself, nor indeed the community of practice of those who actively develop and research them: rather, the issue is that there is a disconnection between the way that the "cryptographer on the street" sees these tools and the way they are understood by tooling experts. It is often unclear what the evidence they produce should actually be interpreted to mean, and without this interpretation, it is difficult for them to have a clear role.

Hence, the aim in this talk will be to sketch a vision for the use of CAE assurance methodologies in this problem domain, which has the goal of providing a skeleton framework to be used in future development of novel cryptography.

Download Slides