Formal methods for quantum security

Huijuan Liu, Xiangjun Xin, Yuzhuo Han +2 more

Ellie D’Hondt

Adrián Sánchez-Marco

[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.

Yi Liu, Xingtong Liu, Jian Wang +2 more

Electronic payment protocols play a vital role in electronic commerce to ensure the security of transaction process. Current electronic payment protocols based on complex mathematical problems will be vulnerable facing a quantum computer. In order to enhance the security against quantum computers, quantum cryptography is introduced into electronic payment protocols. Although the quantum cryptography is claimed to be unconditionally secure, Logical defects are still likely to cause serious problems. We introduced formal analysis to verify the security of electronic payment protocols based on quantum cryptography. Formal analysis methods can discover the vulnerabilities of protocols and help to improve the security of protocols. In this paper, we analyze an electronic payment protocol based on quantum cryptography and the result shows that the protocol is not secure even adopting unconditionally secure quantum cryptography. We found that both the accountability and fairness of the original protocol are not satisfied. Then we proposed an improved protocol to meet the requirement of accountability and fairness and verified it through formal analysis method.

Carmelo R. Cartiere

Jincheng Zhang

Quantum Information Cryptography (QIC) aims to secure information through cryptographic algorithms that are resistant to computational attacks. Traditional cryptographic approaches frequently rely on mathematical hardness assumptions, while geometric cryptography leverages the properties of geometric spaces to create secure systems. This paper explores a novel approach to QIC: the geometric formalization of key decryption. We propose a method that transforms the core decryption problem into a geometric problem, employing a novel optimization algorithm to refine cryptographic parameters and enhance security. The core claim is that this geometric formalization significantly improves the security of key decryption compared to traditional methods, leveraging the power of geometric topology. This work introduces a new framework for analyzing and optimizing cryptographic systems, potentially offering a more robust approach to secure communication.