Modelling and verification of post-quantum key encapsulation mechanisms using Maude.

Area of Science:

• Computer Science
• Cryptography
• Information Security

Background:

• Current communication systems rely on classical cryptography, vulnerable to quantum computing.
• The National Institute of Standards and Technologies' Post-Quantum Cryptography project aims to develop quantum-resistant solutions.
• Formal verification is crucial for assessing the security of cryptographic protocols.

Purpose of the Study:

• To develop a formal framework in Maude for analyzing post-quantum key encapsulation mechanisms.
• To assess the security of these mechanisms under the Dolev-Yao model.
• To identify vulnerabilities and propose solutions for post-quantum cryptography.

Main Methods:

• Constructed a symbolic model of participant behavior in a network using Maude.
• Performed reachability analysis to detect security flaws.
• Utilized Maude Linear Temporal Logic model checker for security, liveness, and fairness analysis.

Main Results:

• Identified a man-in-the-middle attack affecting all analyzed post-quantum key encapsulation mechanisms.
• Discovered a design vulnerability in the Bit Flipping Key Encapsulation protocol.
• Confirmed that security properties are compromised, while liveness and fairness properties hold.

Conclusions:

• The developed Maude framework effectively identifies security vulnerabilities in post-quantum cryptography.
• The man-in-the-middle attack and Bit Flipping Key Encapsulation vulnerability necessitate further research for robust solutions.
• Formal methods are essential for ensuring the security of future quantum-resistant cryptographic systems.