Indexado en

Licencia y uso

Citaciones

Cited 1 times in

Altmetrics

Grant support

star Santiago Escobar and Victor Garcia have been partially supported by the grant PID2021-122830OB-C42 funded by MCIN/AEI/10.13039/501100011033 and ERDF A way of making Europe, by the grant CIPROM/2022/6 funded by Generalitat Valenciana, by INCIBE's Chair funded by the EU-NextGenerationEU through the Spanish government's Plan de Recuperacion, Transformacion y Resiliencia, and by the grant PCI2020-120708-2 funded by MICIN/AEI/10.13039/501100011033 and by the European Union NextGenerationEU/PRTR. Kazuhiro Ogata has been partially supported by JSPS KAKENHI Grant Number 24KK0185.

Análisis de autorías institucional

Compartir

Formalization and analysis of the post-quantum signature scheme FALCON with Maude

Publicado en:Journal Of Logical And Algebraic Methods In Programming. 143 101034- - 2025-02-01 143(), DOI: 10.1016/j.jlamp.2024.101034

Autores: Garcia, Victor; Escobar, Santiago; Ogata, Kazuhiro

Afiliaciones

Resumen

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.

Palabras clave