Kyber, Saber, and SK-MLWR Lattice-Based Key Encapsulation Mechanisms Model Checking with Maude
Facing the potential threat raised by quantum computing, a great deal of research from many groups and industrial giants has gone into building public-key post-quantum cryptographic primitives that are resistant to the quantum attackers. Among them, there is a large number of post-quantum key encaps...
| Main Authors: | , , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Hindawi-IET
2023-01-01
|
| Series: | IET Information Security |
| Online Access: | http://dx.doi.org/10.1049/2023/9399887 |
| _version_ | 1797419433857122304 |
|---|---|
| author | Duong Dinh Tran Kazuhiro Ogata Santiago Escobar Sedat Akleylek Ayoub Otmani |
| author_facet | Duong Dinh Tran Kazuhiro Ogata Santiago Escobar Sedat Akleylek Ayoub Otmani |
| author_sort | Duong Dinh Tran |
| collection | DOAJ |
| description | Facing the potential threat raised by quantum computing, a great deal of research from many groups and industrial giants has gone into building public-key post-quantum cryptographic primitives that are resistant to the quantum attackers. Among them, there is a large number of post-quantum key encapsulation mechanisms (KEMs), whose purpose is to provide a secure key exchange, which is a very crucial component in public-key cryptography. This paper presents a formal security analysis of three lattice-based KEMs including Kyber, Saber, and SK-MLWR. We use Maude, a specification language supporting equational and rewriting logic and a high-performance tool equipped with many advanced features, such as a reachability analyzer that can be used as a model checker for invariant properties, to model the three KEMs as state machines. Because they all belong to the class of lattice-based KEMs, they share many common parts in their designs, such as polynomials, vectors, and message exchange patterns. We first model these common parts and combine them into a specification, called base specification. After that, for each of the three KEMs, by extending the base specification, we just need to model some additional parts and the mechanism execution. Once completing the three specifications, we conduct invariant model checkings with the Maude search command, pointing out a similar man-in-the-middle attack. The occurrence of this attack is due to the fact that authentication is not part of the KEMs, and therefore an active attacker can modify all communication between two honest parties. |
| first_indexed | 2024-03-09T06:48:15Z |
| format | Article |
| id | doaj.art-685916557c7944d49870ab80d9d8abdd |
| institution | Directory Open Access Journal |
| issn | 1751-8717 |
| language | English |
| last_indexed | 2024-03-09T06:48:15Z |
| publishDate | 2023-01-01 |
| publisher | Hindawi-IET |
| record_format | Article |
| series | IET Information Security |
| spelling | doaj.art-685916557c7944d49870ab80d9d8abdd2023-12-03T10:33:06ZengHindawi-IETIET Information Security1751-87172023-01-01202310.1049/2023/9399887Kyber, Saber, and SK-MLWR Lattice-Based Key Encapsulation Mechanisms Model Checking with MaudeDuong Dinh Tran0Kazuhiro Ogata1Santiago Escobar2Sedat Akleylek3Ayoub Otmani4Japan Advanced Institute of Science and TechnologyJapan Advanced Institute of Science and TechnologyVRAINOndokuz Mayis UniversityUniversity of Rouen NormandieFacing the potential threat raised by quantum computing, a great deal of research from many groups and industrial giants has gone into building public-key post-quantum cryptographic primitives that are resistant to the quantum attackers. Among them, there is a large number of post-quantum key encapsulation mechanisms (KEMs), whose purpose is to provide a secure key exchange, which is a very crucial component in public-key cryptography. This paper presents a formal security analysis of three lattice-based KEMs including Kyber, Saber, and SK-MLWR. We use Maude, a specification language supporting equational and rewriting logic and a high-performance tool equipped with many advanced features, such as a reachability analyzer that can be used as a model checker for invariant properties, to model the three KEMs as state machines. Because they all belong to the class of lattice-based KEMs, they share many common parts in their designs, such as polynomials, vectors, and message exchange patterns. We first model these common parts and combine them into a specification, called base specification. After that, for each of the three KEMs, by extending the base specification, we just need to model some additional parts and the mechanism execution. Once completing the three specifications, we conduct invariant model checkings with the Maude search command, pointing out a similar man-in-the-middle attack. The occurrence of this attack is due to the fact that authentication is not part of the KEMs, and therefore an active attacker can modify all communication between two honest parties.http://dx.doi.org/10.1049/2023/9399887 |
| spellingShingle | Duong Dinh Tran Kazuhiro Ogata Santiago Escobar Sedat Akleylek Ayoub Otmani Kyber, Saber, and SK-MLWR Lattice-Based Key Encapsulation Mechanisms Model Checking with Maude IET Information Security |
| title | Kyber, Saber, and SK-MLWR Lattice-Based Key Encapsulation Mechanisms Model Checking with Maude |
| title_full | Kyber, Saber, and SK-MLWR Lattice-Based Key Encapsulation Mechanisms Model Checking with Maude |
| title_fullStr | Kyber, Saber, and SK-MLWR Lattice-Based Key Encapsulation Mechanisms Model Checking with Maude |
| title_full_unstemmed | Kyber, Saber, and SK-MLWR Lattice-Based Key Encapsulation Mechanisms Model Checking with Maude |
| title_short | Kyber, Saber, and SK-MLWR Lattice-Based Key Encapsulation Mechanisms Model Checking with Maude |
| title_sort | kyber saber and sk mlwr lattice based key encapsulation mechanisms model checking with maude |
| url | http://dx.doi.org/10.1049/2023/9399887 |
| work_keys_str_mv | AT duongdinhtran kybersaberandskmlwrlatticebasedkeyencapsulationmechanismsmodelcheckingwithmaude AT kazuhiroogata kybersaberandskmlwrlatticebasedkeyencapsulationmechanismsmodelcheckingwithmaude AT santiagoescobar kybersaberandskmlwrlatticebasedkeyencapsulationmechanismsmodelcheckingwithmaude AT sedatakleylek kybersaberandskmlwrlatticebasedkeyencapsulationmechanismsmodelcheckingwithmaude AT ayoubotmani kybersaberandskmlwrlatticebasedkeyencapsulationmechanismsmodelcheckingwithmaude |