{rfName}
Fo

Indexat a

Llicència i ús

Licencia Icono OpenAccess

Citacions

13

Altmetrics

Anàlisi d'autories institucional

Escobar, SAutor o coautor

Compartir

1 de gener de 2024
Publicacions
>
Article
Sí

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

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

Autors:

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

Afiliacions

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
Veure més

Resum

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.
[+]

Paraules clau

AuthenticationCafeobjEncryptionFormal verificationPost-quantum sshProof scoreProtocolsPublic keyQuantum computingSecuritySecurity analysis

Indicis de qualitat

Impacte bibliomètric. Anàlisi de la contribució i canal de difusió

El treball ha estat publicat a la revista IEEE Access a causa de la seva progressió i el bon impacte que ha aconseguit en els últims anys, segons l'agència Scopus (SJR), s'ha convertit en una referència en el seu camp. A l'any de publicació del treball, 2024 encara no hi ha indicis calculats, però el 2023, es trobava a la posició , aconseguint així situar-se com a revista Q1 (Primer Cuartil), en la categoria Engineering (Miscellaneous).

Independentment de l'impacte esperat determinat pel canal de difusió, és important destacar l'impacte real observat de la pròpia aportació.

Segons les diferents agències d'indexació, el nombre de citacions acumulades per aquesta publicació fins a la data 2026-11-10:

  • Scopus: 4
[+]

Impacte i visibilitat social

Des de la dimensió d'influència o adopció social, i prenent com a base les mètriques associades a les mencions i interaccions proporcionades per agències especialitzades en el càlcul de les denominades "Mètriques Alternatives o Socials", podem destacar a data 2026-11-10:

  • L'ús d'aquesta aportació en marcadors, bifurcacions de codi, afegits a llistes de favorits per a una lectura recurrent, així com visualitzacions generals, indica que algú està fent servir la publicació com a base del seu treball actual. Això pot ser un indicador destacat de futures cites més formals i acadèmiques. Aquesta afirmació està avalada pel resultat de l'indicador "Capture", que aporta un total de: 16 (PlumX).

Amb una intenció més de divulgació i orientada a audiències més generals, podem observar altres puntuacions més globals com:

    És fonamental presentar evidències que recolzin l'alineació plena amb els principis i directrius institucionals sobre Ciència Oberta i la Conservació i Difusió del Patrimoni Intel·lectual. Un clar exemple d'això és:

    • El treball s'ha enviat a una revista la política editorial de la qual permet la publicació en obert Open Access.
    [+]

    Anàlisi del lideratge dels autors institucionals

    Aquest treball s'ha realitzat amb col·laboració internacional, concretament amb investigadors de: Estonia; France; Japan; Turkey.

    [+]

    Reconeixements vinculats a l’ítem

    No Statement Available
    [+]