Verification of Quantum Cryptography
Abstract
The security of cryptographic systems is normally ensured by mathematical proofs. Due to human error, these proofs may often contain errors, limiting the usefulness of said proofs.In recent years, methods for verifying cryptographic security proofs using computers havebeen developed (e.g., the EasyCrypt tool). However, there is an increasing demand for postquantum secure protocols (protocols that stay secure if the attacker has a quantum computer); existing proof tools cannot handle post-quantum security. In this project, we will design theoretical foundations and tools (software) for developing and verifying security proofs on the computer, supporting post-quantum security and also allowing us to analyze protocols that use quantum communication. Our main approach is the design of a logic (quantum relational Hoare logic, qRHL) for reasoning about the relationship between pairs of quantum programs, together with a set of reasoning rules. This logic then allows us to formalize game-based proofs (game-based proofs are an established method for formulating cryptography proofs). The anticipated outcome is a tool that allows us to write and verify proofs written using qRHL, as well as proofs for selected protocols. The impact of this research is to improve the security of protocols in a quantum age, by removing one possible source of human error. In addition, it will impact the research community, by providing new foundations in program verification, and by providing cryptographers with new tools for the verification of their protocols.
Document Details
- Document Type
- DoD Grant Award
- Publication Date
- May 02, 2017
- Source ID
- FA23861714022
Entities
People
- Dominique Unruh
Organizations
- Air Force Office of Scientific Research
- United States Air Force
- University of Tartu