Finding meaning in cryptographic verification: Methods in the verification of post-quantum cryptography

点击翻译按钮获取中文摘要

The research explores different approaches to the problem of functionally verifying complex cryptographic software, and the wider role that formal methods has in creating strong assurance cases for novel cryptography such as post-quantum public-key cryptography. We seek to answer the question of what methodology and approach is likely to result in the most meaningful and useful results in this context, and how meaning can be extracted from the resulting artifacts in a rigorous manner. Much of the work has been based on the technical work of performing such verifications, as well as a review of the literatures in both cryptographic and verification contexts. The focus has been on Classic McEliece, one of the schemes under active consideration by NIST since 2016 under its ongoing post-quantum standardization process.