Formalization and analysis of the post-quantum signature scheme FALCON with Maude
[EN] 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 quan...
| Authors: | ; ; |
|---|---|
| Format: | Article |
| Publication date: | 2025 |
| Country: | España |
| Institution: | Universitat Politècnica de València (UPV) |
| Repository: | RiuNet. Repositorio Institucional de la Universitat Politécnica de Valéncia |
| Language: | English |
| OAI Identifier: | oai:riunet.upv.es:10251/220201 |
| Online Access: | https://riunet.upv.es/handle/10251/220201 |
| Access Level: | Open access |
| Keyword: | Formal methods Post-quantum Signature scheme FALCON Maude |
| _version_ | 1878741501854351361 |
|---|---|
| author | García-Valero, Víctor|||0000-0003-0681-1130 |
| author2 | Escobar Román, Santiago|||0000-0002-3550-4781 Ogata, Kazuhiro |
| author2_role | author author |
| author_browse | Escobar Román, Santiago|||0000-0002-3550-4781 García-Valero, Víctor|||0000-0003-0681-1130 Ogata, Kazuhiro |
| author_facet | García-Valero, Víctor|||0000-0003-0681-1130 Escobar Román, Santiago|||0000-0002-3550-4781 Ogata, Kazuhiro |
| author_role | author |
| collection | RiuNet. Repositorio Institucional de la Universitat Politécnica de Valéncia |
| description | [EN] 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. |
| eu_rights_str_mv | openAccess |
| format | article |
| id | ES_e64c0cb467e6583a9b4dfaa4ebe0ca35 |
| institution | Universitat Politècnica de València (UPV) |
| instname_str | Universitat Politècnica de València (UPV) |
| language | eng |
| network_acronym_str | ES |
| network_name_str | España |
| oai_identifier_str | oai:riunet.upv.es:10251/220201 |
| publishDate | 2025 |
| publishDateSort | 2025 |
| publisher | Elsevier |
| publisherStr | Elsevier |
| reponame_str | RiuNet. Repositorio Institucional de la Universitat Politécnica de Valéncia |
| spelling | Formalization and analysis of the post-quantum signature scheme FALCON with Maude García-Valero, Víctor|||0000-0003-0681-1130 Escobar Román, Santiago|||0000-0002-3550-4781 Ogata, Kazuhiro Formal methods Post-quantum Signature scheme FALCON Maude [EN] 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. 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. Elsevier https://riunet.upv.es/handle/10251/220201 |
| spellingShingle | Formalization and analysis of the post-quantum signature scheme FALCON with Maude García-Valero, Víctor|||0000-0003-0681-1130 Formal methods Post-quantum Signature scheme FALCON Maude |
| title | Formalization and analysis of the post-quantum signature scheme FALCON with Maude |
| title_full | Formalization and analysis of the post-quantum signature scheme FALCON with Maude |
| title_fullStr | Formalization and analysis of the post-quantum signature scheme FALCON with Maude |
| title_full_unstemmed | Formalization and analysis of the post-quantum signature scheme FALCON with Maude |
| title_short | Formalization and analysis of the post-quantum signature scheme FALCON with Maude |
| title_sort | Formalization and analysis of the post-quantum signature scheme FALCON with Maude |
| topic | Formal methods Post-quantum Signature scheme FALCON Maude |
| topic_facet | Formal methods Post-quantum Signature scheme FALCON Maude |
| url | https://riunet.upv.es/handle/10251/220201 |