{rfName}
Fo

Indexado en

Licencia y uso

Licencia Icono OpenAccess

Citaciones

13

Altmetrics

Investigadores/as Institucionales

Escobar, SAutor o Coautor

Compartir

1 de enero de 2024
Publicaciones
>
Artículo
Sí

Formal Analysis of Post-Quantum Hybrid Key Exchange SSH Transport Layer Protocol

Publicado en: IEEE Access. 12 1672-1687 - 2024-01-01, DOI: 10.1109/ACCESS.2023.3347914

Autores:

Tran, Duong Dinh; Ogata, Kazuhiro; Escobar Román, Santiago; Akleylek, Sedat; Otmani, Ayoub
[+]

Afiliaciones

Japan Adv Inst Sci & Technol, Nomi - Autor o Coautor
Univ Politecn Valencia, VRAIN - Autor o Coautor
Univ Rouen Normandie - Autor o Coautor
Univ Tartu - Autor o Coautor
Ver más

Resumen

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

AuthenticationCafeobjEncryptionFormal verificationPost-quantum sshProof scoreProtocolsPublic keyQuantum computingSecuritySecurity analysis

Indicios de calidad

Impacto bibliométrico. Análisis de la aportación y canal de difusión

El trabajo ha sido publicado en la revista IEEE Access debido a la progresión y el buen impacto que ha alcanzado en los últimos años, según la agencia Scopus (SJR), se ha convertido en una referencia en su campo. En el año de publicación del trabajo, 2024 aún no existen indicios calculados, pero en 2023, se encontraba en la posición , consiguiendo con ello situarse como revista Q1 (Primer Cuartil), en la categoría Engineering (Miscellaneous).

Independientemente del impacto esperado determinado por el canal de difusión, es importante destacar el impacto real observado de la propia aportación.

Según las diferentes agencias de indexación, el número de citas acumuladas por esta publicación hasta la fecha 2026-11-10:

  • Scopus: 4
[+]

Impacto y visibilidad social

Desde la dimensión de Influencia o adopción social, y tomando como base las métricas asociadas a las menciones e interacciones proporcionadas por agencias especializadas en el cálculo de las denominadas “Métricas Alternativas o Sociales”, podemos destacar a fecha 2026-11-10:

  • La utilización de esta aportación en marcadores, bifurcaciones de código, añadidos a listas de favoritos para una lectura recurrente, así como visualizaciones generales, indica que alguien está usando la publicación como base de su trabajo actual. Esto puede ser un indicador destacado de futuras citas más formales y académicas. Tal afirmación es avalada por el resultado del indicador “Capture” que arroja un total de: 16 (PlumX).

Con una intencionalidad más de divulgación y orientada a audiencias más generales podemos observar otras puntuaciones más globales como:

    Es fundamental presentar evidencias que respalden la plena alineación con los principios y directrices institucionales en torno a la Ciencia Abierta y la Conservación y Difusión del Patrimonio Intelectual. Un claro ejemplo de ello es:

    • El trabajo se ha enviado a una revista cuya política editorial permite la publicación en abierto Open Access.
    [+]

    Análisis de liderazgo de los autores institucionales

    Este trabajo se ha realizado con colaboración internacional, concretamente con investigadores de: Estonia; France; Japan; Turkey.

    [+]

    Reconocimientos ligados al ítem

    No Statement Available
    [+]