Quantum Cryptography and Its Challenges
Explore the formal verification of quantum cryptography by Dominique Unruh from the University of Tartu. Delve into the trouble with security proofs, post-quantum cryptography, quantum protocols, and more. Understand the post-quantum fallacy and why typical cryptographic proofs may not suffice in the quantum realm. Discover the importance of finding quantum-hard assumptions and the challenges faced by cryptographers in verifying their schemes.
Download Presentation
Please find below an Image/Link to download the presentation.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author. If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
You are allowed to download the files provided on this website for personal or commercial use, subject to the condition that they are used lawfully. All files are the property of their respective owners.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.
E N D
Presentation Transcript
Formal Verification of Quantum Cryptography Dominique Unruh University of Tartu
The trouble with security proofs In theory: Once a protocol is proven secure, it is secure In practice: Implementation is broken Proof is wrong Computer Computer- -aided verification verification to the rescue! to the rescue! aided Dominique Unruh Verification of Quantum Crypto 2
What is quantum cryptography? Cryptography involving quantum mechanics Post-quantum crypto Quantum protocols Dominique Unruh Verification of Quantum Crypto 3
Quantum Protocols Use quantum communication to make impossible tasks feasible Best known example: Unconditionally secure key distribution Dominique Unruh Verification of Quantum Crypto 4
Post-quantum cryptography What must be done? 1. Identify assumptions that are not quantum- broken (e.g., lattice-based crypto, not RSA) 2. Build cryptosystems based on those Possible without quantum literacy ? 3. Prove security Dominique Unruh Verification of Quantum Crypto 5
The post-quantum fallacy If protocol ? is proven secure, and based on assumption ?, and ? is quantum-secure, then ? is quantum-secure. Not true! Consequence: cryptographers focus on finding protocols based on lattices and call it post- quantum crypto. Dominique Unruh Verification of Quantum Crypto 6
Why is the fallacy wrong? Typical crypto proof: If adversary ? breaks protocol ?, then we construct from ? an adversary ? that breaks assumption ?. If ? is quantum, the construction may not work Protocol might be secure, but has no proof! Quantum proofs can be much harder! Dominique Unruh Verification of Quantum Crypto 7
Summary (so far) Post-quantum crypto: Security of classical protocols against quantum attacks Finding quantum hard assumptions: Not enough Need quantum proof techniques Normal cryptographers cannot verify their own schemes! Dominique Unruh Verification of Quantum Crypto 8
Quantum Crypto & Verification Nothing to do (?) For classical protocols ??? Symbolic models Formal methods For quantum protocols & security Existing tools? Post-quantum crypto Classical proofs Computational crypto Quantum protocols Quantum proofs New languages and logics Dominique Unruh Verification of Quantum Crypto 9
Post-quantum crypto verification (computational / classical proto / quantum adv) Tools exist for computational verification CertiCrypt (relational Hoare) EasyCrypt (relational Hoare, higher level) CryptoVerif (rewriting, automated) Could those be quantum-sound? Dominique Unruh Verification of Quantum Crypto 10
Quantum soundness of EasyCrypt CHSH game: ? 0,1 Adv wins if: ? ? = ? ? No communication (after start) ? 0,1 ???? ???? ? ? EasyCrypt proof: Quantum strategy: Pr ??? 0.85 Pr ??? 0.75 Dominique Unruh Verification of Quantum Crypto 11
How EC works: Relational Hoare Logic Assertions: Relations on variable assignments (e.g., ?1= ?2+ ?2) Enables: step Enables: step- -by games are equivalent games are equivalent by- -step proof that two step proof that two A A.k.a. game .k.a. game- -based proofs based proofs RHL judgements: ? ?1~?2{?} means: if initial mem satisfy ?, then final mem satisfy ? E.g.: ?1= ?2 ?1 0 ~ ( ?2 ?2+ ?2) {?1= ?2+ ?2} Dominique Unruh Verification of Quantum Crypto 12
Why EasyCrypt fails Case distinction (e.g., on adv s state ?) ?. ? = ? ?{?} true ?{?} (Related to: coin fixing, rewinding) Composition of equality ? ?1~?2 {?1= ?2 ?1= ?2} ? ?1~?2 { ?1,?1 = ?2,?2} (What does this even mean???) Dominique Unruh Verification of Quantum Crypto 13
QuEasyCrypt (ongong work) Quantum language for crypto games Follows EasyCrypt, no surprises Quantum Hoare Logic Quantum Relational Hoare Logic Same intuition as probabilistic RHL But semantics are quantum rules must be refined Dominique Unruh Verification of Quantum Crypto 14
Challenges If defining quantum RHL analogous to classical: No frame rule judgements are not preserved when adding environment No sensible notion of equality of variables More info offline if interested Dominique Unruh Verification of Quantum Crypto 15
QuEasyCrypt the future If you can use EasyCrypt, you can use QuEasyCrypt Get post-quantum verification for free (when classical proof is quantum-sound) Verification of quantum protocols: Should be possible Time will show Dominique Unruh Verification of Quantum Crypto 16
Summary Nothing to do (?) For classical protocols ??? Symbolic models Formal methods For quantum protocols & security Existing tools? Post-quantum crypto Classical proofs Computational crypto Quantum protocols Quantum proofs New languages and logics Dominique Unruh Verification of Quantum Crypto 17
I thank for your attention This research was supported by European Social Fund s Doctoral Studies and Internationalisation Programme DoRa Logo soup
