Formal Verification of Quantum Cryptography by Dominique Unruh

Explore the significance of formal verification in quantum cryptography as discussed by Dominique Unruh from the University of Tartu. Understand the challenges, motivations, and current work in verifying quantum crypto protocols, and the potential impact of quantum computers on common encryption methods. Delve into post-quantum cryptography and the necessity for research and proactive measures in the face of evolving threats.

• Quantum Cryptography
• Formal Verification
• Quantum Computers
• Post-quantum Cryptography
• Cryptographic Protocols

aslan Follow

Uploaded on Jul 15, 2024 | 0 Views

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. Download presentation by click this link. If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.

Presentation Transcript

1. Formal Verification of Quantum Cryptography Dominique Unruh University of Tartu

2. Outline Quantum crypto: What and why? Challenges. Verification of quantum crypto Motivation and challenges Current work Dominique Unruh Verification of Quantum Crypto 2

3. What is quantum cryptography? Cryptography involving quantum mechanics Using quantum mechanics in crypto protocols Security against quantum computers Dominique Unruh Verification of Quantum Crypto 3

4. Quantum computers Computer is in many states: Quantum parallelism Can be exploited Under very specific conditions! We can: Compute discrete logarithms (breaks ElGamal etc.) Factor large integers (breaks RSA etc.) Reduce the time for brute force attacks to the square root Dominique Unruh Verification of Quantum Crypto 6

5. If quantum computers were here ElGamal, RSA, elliptic curve crypto All commonly used public key crypto: BROKEN If quantum computers were available today Candidates for replacements: Exist, but not as well-studied we would be screwed. Lattice-based crypto, McEliece etc. Symmetric crypto: Double the key length! Common symmetric crypto (AES etc.) Dominique Unruh Verification of Quantum Crypto 7

6. The threat today Quantum computers do not exist Unclear when Post-quantum cryptography If we don t start research now, major disaster when they come (classical crypto, quantum-secure) Research & awareness: now! Dominique Unruh Verification of Quantum Crypto 8

7. Quantum Protocols Use quantum communication to make impossible tasks feasible Best known example: Unconditionally secure key distribution Possible today! (No quantum computer needed.) (Not the main focus of this talk.) Dominique Unruh Verification of Quantum Crypto 9

8. 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 10

9. 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 11

10. 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 12

11. 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 13

12. 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 14

13. 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 15

14. 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 16

15. 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} (Ignores: entanglement) Dominique Unruh Verification of Quantum Crypto 17

16. QuEasyCrypt (work in progress) 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 18

17. Quantum Hoare Logic Semantics of programs: ? ? ? ? a program on classical and quantum variables density operator (a probabilistic quantum state ) the quantum state after execution Assertions: Sets of density operators (preferable closed vector spaces) Hoare triples: ? ?{?} means ? ?. ? ? ? Dominique Unruh Verification of Quantum Crypto 19

18. Classical Relational Hoare Logic Assertions: Relations on states (e.g., ?1= ?2+ ?2) RHL judgements: ? ?1~?2{?} means: if initial states in ?, then final states in ? E.g.: ?1= ?2 skip ~ ?2 ?2+ ?2 {?1= ?2+ ?2} Dominique Unruh Verification of Quantum Crypto 20

19. Classical Relational Hoare Logic RHL judgements: ? ?1~?2{?} means: if initial states in ?, then final states in ? For any ?1,?2 ?: Exists distribution ?on pairs s.t.: Pr ?1,?2 ??= 0 and Formally: ?1 = ?1(?1) ? ?2 = ?2(?2) Dominique Unruh Verification of Quantum Crypto 21

20. Quantum Relational Hoare Logic? If analogous to classical, loose frame rule: ? s variables distinct from ?,?,? ? ? ?{? ?} ? ? ? Without frame rule: No compositional analysis useless Dominique Unruh Verification of Quantum Crypto 22

21. Quantum Relational Hoare Logic? Assertions: Sets of quantum states of systems with two states ? ?1~?2{?} means: Exists quantum process ?: For all ? ?: qRHL: ?1 ?1 ?1 ? ? ? ? ?2 ?2 ?2 ? ? Dominique Unruh Verification of Quantum Crypto 23

22. 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 24

23. 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 25

24. Q? uestions? (Or catch me for offline discussion ) Dominique Unruh Verification of Quantum Crypto 26

25. I thank for your attention This research was supported by European Social Fund s Doctoral Studies and Internationalisation Programme DoRa Logo soup