Automated Security Analysis of Cryptographic Systems Under Quantum Attacks
Abstract
The emergence of quantum computing technology has promised unprecedented improvement in our computational ability, which, however, also leads to quantum attacks that would put many security techniques for modern communication in peril in the not-too-distant future. The defence against quantum attacks should ideally be deployed in the near future to protect today’s secret information from future quantum attacks, especially in security-critical domains like hardware signatures or block-chains, both with very long life cycles. Inspired by the success of the development of formal methods in the security analysis for large, real-world cryptographic systems, the PI proposes to develop and apply formal method techniques in quantum cryptography for automated security analysis of cryptographic systems under quantum attacks. Formally generated security analysis will provide not only efficient and high assurance proofs that can replace the tedious and error-prone analysis for experts, but also independently verifiable proofs that can be used by security practitioners without much quantum knowledge. This project will develop theoretical knowledge on the integration of formal methods and quantum cryptography, especially in automated generation of security analysis of cryptographic constructions under quantum attacks, as well as software artifacts as prototypes of such high assurance technology. It also aims to formally verify candidates of cryptographic systems from the NIST quantum-secure cryptography standardization. As a result, it will help protect cryptographic systems from quantum attacks in both theory and practice.
Document Details
- Document Type
- DoD Grant Award
- Publication Date
- Jan 21, 2022
- Source ID
- FA95502110094XX0
Entities
People
- Xiaodi Wu
Organizations
- Air Force Office of Scientific Research
- United States Air Force
- University of Maryland