Hybrid post-quantum Transport Layer Security formal analysis in Maude-NPA and its parallel version
This article presents a security formal analysis of the hybrid post-quantum Transport Layer Security (TLS) protocol, a quantum-resistant version of the TLS protocol proposed by Amazon Web Services as a precaution in dealing with future attacks from quantum computers. In addition to a classical key e...
| Main Authors: | , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
PeerJ Inc.
2023-09-01
|
| Series: | PeerJ Computer Science |
| Subjects: | |
| Online Access: | https://peerj.com/articles/cs-1556.pdf |
| _version_ | 1827808158340349952 |
|---|---|
| author | Duong Dinh Tran Canh Minh Do Santiago Escobar Kazuhiro Ogata |
| author_facet | Duong Dinh Tran Canh Minh Do Santiago Escobar Kazuhiro Ogata |
| author_sort | Duong Dinh Tran |
| collection | DOAJ |
| description | This article presents a security formal analysis of the hybrid post-quantum Transport Layer Security (TLS) protocol, a quantum-resistant version of the TLS protocol proposed by Amazon Web Services as a precaution in dealing with future attacks from quantum computers. In addition to a classical key exchange algorithm, the proposed protocol uses a post-quantum key encapsulation mechanism, which is believed invulnerable under quantum computers, so the protocol’s key negotiation is called the hybrid key exchange scheme. One of our assumptions about the intruder’s capabilities is that the intruder is able to break the security of the classical key exchange algorithm by utilizing the power of large quantum computers. For the formal analysis, we use Maude-NPA and a parallel version of Maude-NPA (called Par-Maude-NPA) to conduct experiments. The security properties under analysis are (1) the secrecy property of the shared secret key established between two honest principals with the classical key exchange algorithm, (2) a similar secrecy property but with the post-quantum key encapsulation mechanism, and (3) the authentication property. Given the time limit T = 1,722 h (72 days), Par-Maude-NPA found a counterexample of (1) at depth 12 in T, while Maude-NPA did not find it in T. At the same time T, Par-Maude-NPA did not find any counterexamples of (2) and (3) up to depths 12 and 18, respectively, and neither did Maude-NPA. Therefore, the protocol does not enjoy (1), while it enjoys (2) and (3) up to depths 12 and 18, respectively. Subsequently, the secrecy property of the master secret holds for the protocol up to depth 12. |
| first_indexed | 2024-03-11T22:08:18Z |
| format | Article |
| id | doaj.art-cf6379819ec84ebd988a94b441821f45 |
| institution | Directory Open Access Journal |
| issn | 2376-5992 |
| language | English |
| last_indexed | 2024-03-11T22:08:18Z |
| publishDate | 2023-09-01 |
| publisher | PeerJ Inc. |
| record_format | Article |
| series | PeerJ Computer Science |
| spelling | doaj.art-cf6379819ec84ebd988a94b441821f452023-09-24T15:05:11ZengPeerJ Inc.PeerJ Computer Science2376-59922023-09-019e155610.7717/peerj-cs.1556Hybrid post-quantum Transport Layer Security formal analysis in Maude-NPA and its parallel versionDuong Dinh Tran0Canh Minh Do1Santiago Escobar2Kazuhiro Ogata3Japan Advanced Institute of Science and Technology, Nomi, JapanJapan Advanced Institute of Science and Technology, Nomi, JapanUniversidad Politécnica de Valencia, Valencia, SpainJapan Advanced Institute of Science and Technology, Nomi, JapanThis article presents a security formal analysis of the hybrid post-quantum Transport Layer Security (TLS) protocol, a quantum-resistant version of the TLS protocol proposed by Amazon Web Services as a precaution in dealing with future attacks from quantum computers. In addition to a classical key exchange algorithm, the proposed protocol uses a post-quantum key encapsulation mechanism, which is believed invulnerable under quantum computers, so the protocol’s key negotiation is called the hybrid key exchange scheme. One of our assumptions about the intruder’s capabilities is that the intruder is able to break the security of the classical key exchange algorithm by utilizing the power of large quantum computers. For the formal analysis, we use Maude-NPA and a parallel version of Maude-NPA (called Par-Maude-NPA) to conduct experiments. The security properties under analysis are (1) the secrecy property of the shared secret key established between two honest principals with the classical key exchange algorithm, (2) a similar secrecy property but with the post-quantum key encapsulation mechanism, and (3) the authentication property. Given the time limit T = 1,722 h (72 days), Par-Maude-NPA found a counterexample of (1) at depth 12 in T, while Maude-NPA did not find it in T. At the same time T, Par-Maude-NPA did not find any counterexamples of (2) and (3) up to depths 12 and 18, respectively, and neither did Maude-NPA. Therefore, the protocol does not enjoy (1), while it enjoys (2) and (3) up to depths 12 and 18, respectively. Subsequently, the secrecy property of the master secret holds for the protocol up to depth 12.https://peerj.com/articles/cs-1556.pdfPost-quantumTLSCryptographic protocolMaude-NPAParallel Maude-NPASecurity analysis |
| spellingShingle | Duong Dinh Tran Canh Minh Do Santiago Escobar Kazuhiro Ogata Hybrid post-quantum Transport Layer Security formal analysis in Maude-NPA and its parallel version PeerJ Computer Science Post-quantum TLS Cryptographic protocol Maude-NPA Parallel Maude-NPA Security analysis |
| title | Hybrid post-quantum Transport Layer Security formal analysis in Maude-NPA and its parallel version |
| title_full | Hybrid post-quantum Transport Layer Security formal analysis in Maude-NPA and its parallel version |
| title_fullStr | Hybrid post-quantum Transport Layer Security formal analysis in Maude-NPA and its parallel version |
| title_full_unstemmed | Hybrid post-quantum Transport Layer Security formal analysis in Maude-NPA and its parallel version |
| title_short | Hybrid post-quantum Transport Layer Security formal analysis in Maude-NPA and its parallel version |
| title_sort | hybrid post quantum transport layer security formal analysis in maude npa and its parallel version |
| topic | Post-quantum TLS Cryptographic protocol Maude-NPA Parallel Maude-NPA Security analysis |
| url | https://peerj.com/articles/cs-1556.pdf |
| work_keys_str_mv | AT duongdinhtran hybridpostquantumtransportlayersecurityformalanalysisinmaudenpaanditsparallelversion AT canhminhdo hybridpostquantumtransportlayersecurityformalanalysisinmaudenpaanditsparallelversion AT santiagoescobar hybridpostquantumtransportlayersecurityformalanalysisinmaudenpaanditsparallelversion AT kazuhiroogata hybridpostquantumtransportlayersecurityformalanalysisinmaudenpaanditsparallelversion |