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

该研究探索了解决功能验证复杂加密软件问题的不同方法，以及形式化方法在为新型加密（如后量子公钥加密）创建强保证案例方面的更广泛作用。我们试图回答这样的问题：在这种情况下，什么样的方法论和方法可能产生最有意义和最有用的结果，以及如何以严格的方式从产生的工件中提取意义。大部分工作都是基于执行此类验证的技术工作，以及对密码学和验证上下文的文献的回顾。经典McEliece是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.