{rfName}
Fo

Indexed in

License and Use

Licencia Icono OpenAccess

Citations

13

Altmetrics

Analysis of institutional authors

Escobar, SAuthor

Share

January 1, 2024
Publications
>
Article
Sí

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

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

Authors:

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

Affiliations

Japan Adv Inst Sci & Technol, Nomi - Author
Univ Politecn Valencia, VRAIN - Author
Univ Rouen Normandie - Author
Univ Tartu - Author
See more

Abstract

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

Keywords

AuthenticationCafeobjEncryptionFormal verificationPost-quantum sshProof scoreProtocolsPublic keyQuantum computingSecuritySecurity analysis

Quality index

Bibliometric impact. Analysis of the contribution and dissemination channel

The work has been published in the journal IEEE Access due to its progression and the good impact it has achieved in recent years, according to the agency Scopus (SJR), it has become a reference in its field. In the year of publication of the work, 2024 there are still no calculated indicators, but in 2023, it was in position , thus managing to position itself as a Q1 (Primer Cuartil), in the category 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
[+]

Impact and social visibility

From the perspective of influence or social adoption, and based on metrics associated with mentions and interactions provided by agencies specializing in calculating the so-called "Alternative or Social Metrics," we can highlight as of 2026-11-10:

  • The use of this contribution in bookmarks, code forks, additions to favorite lists for recurrent reading, as well as general views, indicates that someone is using the publication as a basis for their current work. This may be a notable indicator of future more formal and academic citations. This claim is supported by the result of the "Capture" indicator, which yields a total of: 16 (PlumX).

With a more dissemination-oriented intent and targeting more general audiences, we can observe other more global scores such as:

    It is essential to present evidence supporting full alignment with institutional principles and guidelines on Open Science and the Conservation and Dissemination of Intellectual Heritage. A clear example of this is:

    • The work has been submitted to a journal whose editorial policy allows open Open Access publication.
    [+]

    Leadership analysis of institutional authors

    This work has been carried out with international collaboration, specifically with researchers from: Estonia; France; Japan; Turkey.

    [+]

    Awards linked to the item

    No Statement Available
    [+]