CerQuS · Certified Quantum Security

Digital communication permeates all areas of today's daily life. Cryptographic protocols are used to secure thatcommunication. Quantum communication and the advent of quantum computers both threaten existing cryptographicsolutions, and create new opportunities for secure protocols. The security of cryptographic systems is normally ensured bymathematical proofs. Due to human error, however, these proofs often contain errors, limiting the usefulness of said proofs.This is especially true in the case of quantum protocols since human intuition is well-adapted to the classical world, but notto quantum mechanics. To resolve this problem, methods for verifying cryptographic security proofs using computers (i.e.,for ""certifying"" the security) have been developed. Yet, all existing verification approaches handle classical cryptographyonly - for quantum protocols, no approaches exist.This project will lay the foundations for the verification of quantum cryptography. We will design logics and software toolsfor developing and verifying security proofs on the computer, both for classical protocols secure against quantum computer(post-quantum security) and for protocols that use quantum communication.Our main approach is the design of a logic (quantum relational Hoare logic, qRHL) for reasoning about the relationshipbetween pairs of quantum programs, together with an ecosystem of manual and automated reasoning tools, culminating infully certified security proofs for real-world quantum protocols.As a final result, the project will improve the security of protocols in the quantum age, by removing one possible source ofhuman error. In addition, the project directly impacts the research community, by providing new foundations in programverification, and by providing cryptographers with new tools for the verification of their protocols.""