Formalization and analysis of the post-quantum signature scheme FALCON with Maude
Víctor García, Santiago Escobar, Kazuhiro Ogata · Journal of Logical and Algebraic Methods in Programming · 2024
Digital signatures ensure the authenticity and integrity of digital assets , vital properties for any secure communication. 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. The post-quantum signature scheme FALCON was one of the finalists. We present a continuation of the first steps towards the formal specification and analysis, in the high-performance language Maude, of signature schemes. We have adapted and improved a previous framework, originally aimed to formally specify and analyse post-quantum key encapsulation mechanisms. As a use case of the new framework, we specify an executable symbolic model of FALCON. On the symbolic model, we verify termination and fairness using LTL formulas with Maude's model checker . Furthermore, authentication , integrity and non-repudiation are analysed through invariant analysis. Integrity and non-repudiation hold, meanwhile, authentication does not hold in our symbolic model.