Room 206 (2nd floor, badged access)
2 juillet 2026 - 14h00
Towards intuitive and formal security proofs using quantum-inspired diagrammatic reasoning
par Léo Colisson Palais de UGA (LJK - CASC)
Abstract: Given the high risks of many cryptographic applications, it is fundamental to have security proofs to assert their security, ideally automatically verified by a computer. But security proofs (not even mentioning formal proofs!) present many challenges, making them really tedious to write and check… and things get even worse when considering protocols secure against quantum adversaries, quantum protocols, or formal security proofs. This is slowly leading to a trust crisis in cryptography as it is basically impossible to verify new results, and generative AI make this question even more relevant. While formal tools exist to check security proofs, they all have many important limitations, notably they are often not made to take into account the specificities of quantum adversaries, and instead of helping us to reason, they actually add an extra (huge) layer of complexity.
In this presentation, I will explore a new approach that we developed to write diagrammatic security proofs, inspired by the ZX-calculus, a tool used to efficiently describe quantum processes. Not only our approach greatly simplify the generation and verification of security proofs. Moreover, as a side result, we can also easily generate a proof that can formally be checked by a computer, and I will give a demonstration of our software in development. Yet, many challenges remain, for instance to study and increase the expressiveness of our framework, and to compile these proofs into other formal proof systems… and that's where you may enter into the picture ?
