Skip to main page content
U.S. flag

An official website of the United States government

Dot gov

The .gov means it’s official.
Federal government websites often end in .gov or .mil. Before sharing sensitive information, make sure you’re on a federal government site.

Https

The site is secure.
The https:// ensures that you are connecting to the official website and that any information you provide is encrypted and transmitted securely.

Access keys NCBI Homepage MyNCBI Homepage Main Content Main Navigation
. 2023 Sep 19:9:e1547.
doi: 10.7717/peerj-cs.1547. eCollection 2023.

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

Víctor García  1 , Santiago Escobar  1 , Kazuhiro Ogata  2 , Sedat Akleylek  3   4 , Ayoub Otmani  5
Affiliations

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

Víctor García et al. PeerJ Comput Sci. .

Abstract

Communication and information technologies shape the world's systems of today, and those systems shape our society. The security of those systems relies on mathematical problems that are hard to solve for classical computers, that is, the available current computers. Recent advances in quantum computing threaten the security of our systems and the communications we use. In order to face this threat, multiple solutions and protocols have been proposed in the Post-Quantum Cryptography project carried on by the National Institute of Standards and Technologies. The presented work focuses on defining a formal framework in Maude for the security analysis of different post-quantum key encapsulation mechanisms under assumptions given under the Dolev-Yao model. Through the use of our framework, we construct a symbolic model to represent the behaviour of each of the participants of the protocol in a network. We then conduct reachability analysis and find a man-in-the-middle attack in each of them and a design vulnerability in Bit Flipping Key Encapsulation. For both cases, we provide some insights on possible solutions. Then, we use the Maude Linear Temporal Logic model checker to extend the analysis of the symbolic system regarding security, liveness and fairness properties. Liveness and fairness properties hold while the security property does not due to the man-in-the-middle attack and the design vulnerability in Bit Flipping Key Encapsulation.

Keywords: Formal verification; Key encapsulation mechanisms; Maude; Post-quantum protocols; Rewriting logic.

PubMed Disclaimer

Conflict of interest statement

Sedat Akleylek is an Academic Editor for PeerJ.

Figures

Figure 1
Figure 1. Network diagram of a simplified Needham–Schroeder protocol version.
Figure 2
Figure 2. Subtype relation between defined Key, PubKey and SecKey types.
Figure 3
Figure 3. Definition of operators for participants and messages in our model of the simplified NSPK.
Figure 4
Figure 4. Definition in Maude of a set operator for participants with associative and commutative properties and empty as the identity element.
Figure 5
Figure 5. Definition of the system state for the NSPK protocol.
Figure 6
Figure 6. Rules regarding the capabilities of the honest participants as defined by the simplified version of the NSPK protocol.
Figure 7
Figure 7. Rules regarding the capabilities of the intruder as defined by the simplified version of the NSPK protocol.
Figure 8
Figure 8. Output of a search command to examine the execution paths for states where two participants have applied the NSPK protocol, and thus share their respective secret values.
Figure 9
Figure 9. Output of a search command to examine the execution paths for a MITM attack in the NSPK protocol symbolic specification.
Figure 10
Figure 10. Code of a functional module that implements the factorial in Maude.
Figure 11
Figure 11. Execution of two factorial expressions with the reduce command.
Figure 12
Figure 12. High-level view of the behaviour of a key exchange of a KEM between two honest participants, i.e., Alice and Bob.
Figure 13
Figure 13. Algorithms of Kyber Key Encapsulation Mechanism adapted from Avanzi et al. (2019).
Figure 14
Figure 14. Internal algorithms of the Kyber Key Encapsulation Mechanism adapted from Avanzi et al. (2019).
Figure 15
Figure 15. Algorithms implementing the three main steps of the KEM BIKE, adapted from Aragon et al. (2017).
Figure 16
Figure 16. Algorithms of McEliece adapted from Chou et al. (2022).
Figure 17
Figure 17. Structure of our framework in modules with relations of inclusion between them.
Figure 18
Figure 18. Definition of a participant at the network in MODEL-CONFIGURATION.
Figure 19
Figure 19. Definition of components to link three notions of keys with a participant.
Figure 20
Figure 20. Definition of the message operator for our symbolic model.
Figure 21
Figure 21. Definition of the syntax to represent the global state of our system.
Figure 22
Figure 22. Example of initial state definition for KYBER.
Figure 23
Figure 23. General definition of conditional rule KeyGen in our framework.
Figure 24
Figure 24. Definition of rules SendPK and ReceivePK to send and receive a public key in our framework.
Figure 25
Figure 25. Definition of conditional rule Enc in our framwork.
Figure 26
Figure 26. Definition of rules SendCiph and ReceiveCiph to send and receive a ciphertext in our framework.
Figure 27
Figure 27. Definition of conditional rule Dec in our system module KYBER.
Figure 28
Figure 28. Definition of conditional rule Intercept1 in our system module KYBER.
Figure 29
Figure 29. Definition of conditional rule Intercept2 in our system module KYBER.
Figure 30
Figure 30. Conditions of rule KeyGen in the symbolic model of Kyber.
Figure 31
Figure 31. Conditions of rule Enc in the symbolic model of Kyber.
Figure 32
Figure 32. Conditions of rule Dec in the symbolic model of Kyber.
Figure 33
Figure 33. Conditions of rule KeyGen in the symbolic model of BIKE.
Figure 34
Figure 34. Conditions of Enc in the symbolic model of BIKE.
Figure 35
Figure 35. Conditions of rule Dec in the symbolic model of BIKE.
Figure 36
Figure 36. Conditions of rule KeyGen in the symbolic model of Classic McEliece.
Figure 37
Figure 37. Conditions of rule Enc in the symbolic model of Classic McEliece.
Figure 38
Figure 38. Conditions of rule Dec in the symbolic model of Classic McEliece.
Figure 39
Figure 39. New capabilities an intruder might use to learn certain values in BIKE without following the scheme.
Figure 40
Figure 40. Definition template of an initial state for any of our system modules representing a KEM.
Figure 41
Figure 41. Command template for a key agreement session of any KEMs of our framework in Maude.
Figure 42
Figure 42. Command template to search for a man-in-the-middle attack of any KEMs of our framework in Maude.
Figure 43
Figure 43. Diagram depicting a possible step trace that led to the MITM attack of a KEM regarding our symbolic model.
Figure 44
Figure 44. Diagram depicting a step trace in the BIKE symbolic model leading to the leakage of critical information.
Figure 45
Figure 45. wantsToShareKey predicate definition in module KEM-PREDS.
Figure 46
Figure 46. sharedAKeyWith predicate definition in module KEM-PREDS.
Figure 47
Figure 47. stolenSharedKey predicate definition in module KEM-PREDS.
See this image and copyright information in PMC

References

    1. Abadi M, Rogaway P. Reconciling two views of cryptography (the computational soundness of formal encryption) Journal of Cryptology. 2002;15(2):103–127. doi: 10.1007/s00145-001-0014-7. - DOI
    1. Aragon N, Barreto PS, Bettaieb S, Bidoux L, Blazy O, Deneuville J-C, Gaborit P, Ghosh S, Gueron S, Güneysu T, Melchor CA, Misoczki R, Persichetti E, Richter-Brockmann J, Sendrier N, Tillich J-P, Vasseur V, Zémor G. Hyper Articles en Ligne (HAL); Lyon, France: 2017. Bike: bit flipping key encapsulation.
    1. Avanzi R, Bos J, Ducas L, Kiltz E, Lepoint T, Lyubashevsky V, Schanck JM, Schwabe P, Seiler G, Stehlé D. Crystals-kyber algorithm specifications and supporting documentation. NIST PQC Round 2(4).2019.
    1. Bae K, Meseguer J, Ölveczky PC. Formal patterns for multirate distributed real-time systems. Science of Computer Programming. 2014;91:3–44. doi: 10.1016/j.scico.2013.09.010. - DOI
    1. Barbosa M, Barthe G, Bhargavan K, Blanchet B, Cremers C, Liao K, Parno B. Sok: Computer-aided cryptography. 42nd IEEE Symposium on Security and Privacy, SP 2021, San Francisco, CA, USA, 24–27 May 2021; Piscataway. 2021. pp. 777–795.

LinkOut - more resources