Hybrid post-quantum Transport Layer Security formal analysis in Maude-NPA and its parallel version.

Area of Science:

• Cybersecurity
• Cryptography
• Quantum Computing

Background:

• The increasing threat of quantum computers necessitates quantum-resistant cryptographic protocols.
• Transport Layer Security (TLS) is crucial for secure internet communication.
• Amazon Web Services proposed a hybrid post-quantum TLS protocol combining classical and quantum-resistant methods.

Purpose of the Study:

• To perform a formal security analysis of the hybrid post-quantum TLS protocol.
• To evaluate the protocol's resilience against quantum computer attacks.
• To verify key exchange secrecy and authentication properties.

Main Methods:

• Formal security analysis using Maude-NPA and Par-Maude-NPA.
• Experimental evaluation of security properties under a time limit.
• Analysis of classical key exchange secrecy, post-quantum key encapsulation secrecy, and authentication.

Main Results:

• A counterexample for the classical key exchange secrecy property was found by Par-Maude-NPA.
• No counterexamples were found for the post-quantum key encapsulation secrecy (up to depth 12).
• No counterexamples were found for the authentication property (up to depth 18).

Conclusions:

• The hybrid post-quantum TLS protocol's classical component is vulnerable to quantum attacks.
• The post-quantum component and authentication properties demonstrate resilience against quantum threats.
• The protocol's master secret secrecy is maintained up to depth 12.