Tran, DD.; Ogata, K.; Escobar Román, S.; Akleylek, S.; Otmani, A. (2024). Formal Analysis of Post-Quantum Hybrid Key Exchange SSH Transport Layer Protocol. IEEE Access. 12:1672-1687. https://doi.org/10.1109/ACCESS.2023.3347914
Por favor, use este identificador para citar o enlazar este ítem: http://hdl.handle.net/10251/203853
Título:
|
Formal Analysis of Post-Quantum Hybrid Key Exchange SSH Transport Layer Protocol
|
Autor:
|
Tran, Duong Dinh
Ogata, Kazuhiro
Escobar Román, Santiago
Akleylek, Sedat
Otmani, Ayoub
|
Entidad UPV:
|
Universitat Politècnica de València. Escola Tècnica Superior d'Enginyeria Informàtica
|
Fecha difusión:
|
|
Resumen:
|
[EN] Facing the quantum attack threat, a quantum-resistant version of the SSH Transport Layer protocol has been proposed and been standardized by an IETF working group. This standardization process has been motivated by ...[+]
[EN] Facing the quantum attack threat, a quantum-resistant version of the SSH Transport Layer protocol has been proposed and been standardized by an IETF working group. This standardization process has been motivated by the fact that if practical quantum computers become available, classical key exchange algorithms used today will no longer be safe because their security can be efficiently broken by Shor's algorithm running on a quantum computer. In this paper, we construct a symbolic model of the proposed protocol, specify it in the specification language CafeOBJ, and conduct a formal analysis of the claimed security properties with the employment of a formal method tool called Invariant Proof Score Generator (IPSG). Three security properties are formally verified with respect to an unbounded number of protocol participants and protocol executions by employing IPSG to produce their formal proofs, the so- called proof scores in CafeOBJ. With another property, namely authentication, we find a counterexample against it, and then we propose to slightly revise the protocol. With the improved version, we formally verify that the authentication property is enjoyed, while the three properties remain secure. To model the presence of malicious participants, we extend the Dolev-Yao intruder, which is the standard intruder model used in security protocol analysis/verification, because the availability assumption of large-scale quantum computers gives the attacker some new capabilities. Under our threat model, the intruder is given capabilities of fully controlling the network as the Dolev-Yao intruder, and additionally breaking ECDH's security as well as compromising secrets.
[-]
|
Palabras clave:
|
Protocols
,
Security
,
Quantum computing
,
Public key
,
Formal verification
,
Encryption
,
Authentication
,
Post-quantum SSH
,
CafeOBJ
,
Proof score
,
Security analysis
|
Derechos de uso:
|
Reconocimiento - No comercial - Sin obra derivada (by-nc-nd)
|
Fuente:
|
IEEE Access. (eissn:
2169-3536
)
|
DOI:
|
10.1109/ACCESS.2023.3347914
|
Editorial:
|
Institute of Electrical and Electronics Engineers
|
Versión del editor:
|
https://doi.org/10.1109/ACCESS.2023.3347914
|
Código del Proyecto:
|
info:eu-repo/grantAgreement/AEI/Plan Estatal de Investigación Científica y Técnica y de Innovación 2017-2020/PCI2020-120708-2/ES/FORMAL ANALYSIS AND VERIFICATION OF POST-QUANTUM CRYPTOGRAPHIC PROTOCOLS/
...[+]
info:eu-repo/grantAgreement/AEI/Plan Estatal de Investigación Científica y Técnica y de Innovación 2017-2020/PCI2020-120708-2/ES/FORMAL ANALYSIS AND VERIFICATION OF POST-QUANTUM CRYPTOGRAPHIC PROTOCOLS/
info:eu-repo/grantAgreement/AEI/Plan Estatal de Investigación Científica y Técnica y de Innovación 2021-2023/PID2021-122830OB-C42/ES/METODOS FORMALES ESCALABLES PARA APLICACIONES REALES/
info:eu-repo/grantAgreement/ANR//ANR-22-PETQ-0008 PQ-TLS/
info:eu-repo/grantAgreement/GVA//CIPROM%2F2022%2F6//Tecnologías de Aprendizaje y Razonamiento Rápido y Lento/
info:eu-repo/grantAgreement/TUBITAK//121R006/
info:eu-repo/grantAgreement/JST//JPMJSC20C2/
[-]
|
Agradecimientos:
|
The work of Duong Dinh Tran and Kazuhiro Ogata was supported by the JST SICORP, Japan, under Grant JPMJSC20C2.
The work of Santiago Escobar was supported in part by the MCIN/AEI/10.13039/501100011033 and ERDF A way of ...[+]
The work of Duong Dinh Tran and Kazuhiro Ogata was supported by the JST SICORP, Japan, under Grant JPMJSC20C2.
The work of Santiago Escobar was supported in part by the MCIN/AEI/10.13039/501100011033 and ERDF A way of making
Europe under Grant PID2021-122830OB-C42, in part by the Generalitat Valenciana under Grant CIPROM/2022/6, in part by the
MICIN/AEI/10.13039/501100011033 under Grant PCI2020-120708-2, and in part by the European Union NextGenerationEU/PRTR.
The work of Sedat Akleylek was supported in part by TUBITAK under Grant 121R006. The work of Ayoub Otmani was supported
in part by the FAVPQC Project funded by CNRS, and in part by the Agence Nationale de la Recherche (ANR) within France 2030
Program under Grant ANR-22-PETQ-0008 PQ-TLS.
[-]
|
Tipo:
|
Artículo
|