Cargando…

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...

Descripción completa

Detalles Bibliográficos
Autores principales: Tran, Duong Dinh, Do, Canh Minh, Escobar, Santiago, Ogata, Kazuhiro
Formato: Online Artículo Texto
Lenguaje:English
Publicado: PeerJ Inc. 2023
Materias:
Acceso en línea:https://www.ncbi.nlm.nih.gov/pmc/articles/PMC10557497/
https://www.ncbi.nlm.nih.gov/pubmed/37810331
http://dx.doi.org/10.7717/peerj-cs.1556
_version_ 1785117102395359232
author Tran, Duong Dinh
Do, Canh Minh
Escobar, Santiago
Ogata, Kazuhiro
author_facet Tran, Duong Dinh
Do, Canh Minh
Escobar, Santiago
Ogata, Kazuhiro
author_sort Tran, Duong Dinh
collection PubMed
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.
format Online
Article
Text
id pubmed-10557497
institution National Center for Biotechnology Information
language English
publishDate 2023
publisher PeerJ Inc.
record_format MEDLINE/PubMed
spelling pubmed-105574972023-10-07 Hybrid post-quantum Transport Layer Security formal analysis in Maude-NPA and its parallel version Tran, Duong Dinh Do, Canh Minh Escobar, Santiago Ogata, Kazuhiro PeerJ Comput Sci Cryptography 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. PeerJ Inc. 2023-09-22 /pmc/articles/PMC10557497/ /pubmed/37810331 http://dx.doi.org/10.7717/peerj-cs.1556 Text en ©2023 Tran et al. https://creativecommons.org/licenses/by/4.0/This is an open access article distributed under the terms of the Creative Commons Attribution License (https://creativecommons.org/licenses/by/4.0/) , which permits unrestricted use, distribution, reproduction and adaptation in any medium and for any purpose provided that it is properly attributed. For attribution, the original author(s), title, publication source (PeerJ Computer Science) and either DOI or URL of the article must be cited.
spellingShingle Cryptography
Tran, Duong Dinh
Do, Canh Minh
Escobar, Santiago
Ogata, Kazuhiro
Hybrid post-quantum Transport Layer Security formal analysis in Maude-NPA and its parallel version
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 Cryptography
url https://www.ncbi.nlm.nih.gov/pmc/articles/PMC10557497/
https://www.ncbi.nlm.nih.gov/pubmed/37810331
http://dx.doi.org/10.7717/peerj-cs.1556
work_keys_str_mv AT tranduongdinh hybridpostquantumtransportlayersecurityformalanalysisinmaudenpaanditsparallelversion
AT docanhminh hybridpostquantumtransportlayersecurityformalanalysisinmaudenpaanditsparallelversion
AT escobarsantiago hybridpostquantumtransportlayersecurityformalanalysisinmaudenpaanditsparallelversion
AT ogatakazuhiro hybridpostquantumtransportlayersecurityformalanalysisinmaudenpaanditsparallelversion