Formal verification of Hybrid Post-Quantum TLS protocol

Abstract

[EN] With the arrival of quantum computing, ensuring the security of communications protocol has become even more crucial. This study explores the formal verification of a Transport Layer Security protocol designed to withstand quantum menaces. While traditional cryptographic methods are effective against classical computing adversaries, they are susceptible to attacks empowered by quantum computation. Hence, there is a real need to transition to Post-Quantum cryptography, which offers resilience against future threats. This research focuses on formally veryfiying the Hybrid Post-Quantum TLS protocol to provide mathematical assurance of its security properties. Formal verification offers a rigorous method for analyzing the correctness and robustness of cryptographic protocols, reducing the risk of undetected vulnerabilities. By employing formal methods, we scrutinize the protocol s design, implementation, and cryptographic primitives to identify a potential weaknesses and ensure compliance with security standards. The formal verification of the Hybrid Post-Quantum TLS protocol not only enhances our understanding of its security assurances but also underscores the significance of rigorous validation in cryptographic design.

[ES] Con la llegada de la computación cuántica, asegurar la seguridad del protocolo de comunicaciones se ha vuelto aún más crucial. Este estudio explora la verificación formal de un protocolo de Seguridad en la Capa de Transporte diseñado para resistir las amenazas cuánticas. Mientras que los métodos criptográficos tradicionales son efectivos contra adversarios de computación clásica, son susceptibles a ataques potenciados por la computación cuántica. Por lo tanto, hay una necesidad real de hacer la transición a la criptografía post-cuántica, que ofrece resistencia contra amenazas futuras. Esta investigación se centra en verificar formalmente el protocolo Hybrid Post-Quantum TLS para proporcionar aseguramiento matemático de sus propiedades de seguridad. La verificación formal ofrece un método riguroso para analizar la corrección y la robustez de los protocolos criptográficos, reduciendo el riesgo de vulnerabilidades no detectadas. Al emplear métodos formales, examinamos el diseño del protocolo, la implementación y las primitivas criptográficas para identificar posibles debilidades y garantizar el cumplimiento de los estándares de seguridad. La verificación formal del protocolo Hybrid Post-Quantum TLS no solo mejora nuestra comprensión de sus garantías de seguridad, sinó que también subraya la importancia de una validación rigurosa en el diseño criptográfico.

[CA] Amb l’arribada de la computació quàntica, garantir la seguretat dels protocols de comunicació s’ha tornat encara més crucial. Aquest estudi explora la verificació formal d’un protocol de Seguretat de la Capa de Transport dissenyat per a resistir les amenaces quàntiques. Mentre que els mètodes criptogràfics tradicionals són efectius contra adversaris de la computació clàssica, són susceptibles a atacs potenciats per la computació quàntica. Per tant, hi ha una necessitat real de transicionar a la criptografia post-quàntica, que ofereix resistència contra amenaces futures. Aquesta investigació es centra en verificar formalment un protocol TLS post-quàntic per a proporcionar una garantia matemàtica de les seues propietats de seguretat. La verificació formal ofereix un mètode rigorós per analitzar la correcció i robustesa dels protocols criptogràfics, reduint el risc de vulnerabilitats no detectades. En emprar mètodes formals, examinem el disseny del protocol, la seua implementació i primitives criptogràfiques per a identificar possibles debilitats. La verificació formal del protocol TLS post-quàntic no només millora la nostra comprensió de les seues garanties de seguretat, sinó que també subratlla la importància d’una validació rigorosa en el disseny criptogràfic.