The National Institute of Standards and Technologies launched the Post-Quantum Cryptography project to standardise new algorithms and protocols that are secure against quantum attackers. In the Formal Analysis and Verification of Post-Quantum Cryptographic Protocols (FAVPQC) project funded by The European Interest Group (EIG) CONCERT-Japan with Japan, France, and Turkey, we have modelled and analysed several post-quantum protocols using different approaches, formal specification in Maude and CafeOBJ, theorem proving using Proof Scores, and model checking using the Maude-NPA protocol analyser.
In this talk, I will overview the problematic of post-quantum protocols, discuss the final decision of the NIST, explain the underlying notions of these post-quantum protocols, and show the different results that we have obtained.
Join at: imt.lu/sagrestia