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

这项研究探索了从功能上验证复杂密码软件问题的不同方法，以及形式方法在为后量子公钥密码学等新型密码学创建强有力的保证案例方面具有的更广泛的作用。我们试图回答这样一个问题，即在这种情况下，什么方法和方法可能会产生最有意义和最有用的结果，以及如何以严格的方式从产生的构件中提取意义。大部分工作的基础是进行这种核查的技术工作，以及对密码学和核查方面的文献的审查。重点一直放在Classic McEliess上，这是NIST自2016年以来在其正在进行的后量子标准化进程中积极考虑的计划之一。

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.