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

寻找密码验证的意义：后量子密码验证的方法

• 批准号: 2744596
• 金额: --
• 依托单位: Royal Holloway University of London
• 依托单位国家: 英国
• 项目类别: Studentship
• 财政年份: 2019
• 资助国家: 英国
• 起止时间: 2019 至 无数据
• 项目状态: 已结题
• 来源: https://gtr.ukri.org/projects?ref=studentship-2744596
• 关键词: Finding; meaning; cryptographic; verification; Methods

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.

该研究探讨了功能验证复杂加密软件问题的不同方法，以及形式化方法在为新密码学（如后量子公钥密码学）创建强保证案例方面的更广泛作用。我们试图回答的问题是什么方法和途径可能会导致在这种情况下，最有意义和有用的结果，以及如何意义可以从所产生的工件中提取一个严格的方式。大部分工作都基于执行此类验证的技术工作，以及对加密和验证背景下的文献的回顾。重点是Classic McEliece，这是NIST自2016年以来在其正在进行的后量子标准化过程中积极考虑的方案之一。