Pith. sign in

REVIEW 1 major objections 5 minor 64 references

Finding SSH Strict Key Exchange Violations by State Learning

T0 review · 1 major / 5 minor · reviewed 2026-08-04 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read The paper shows that seven of ten SSH server implementations violate the strict key exchange specification, and that two of those violations are exploitable: a rogue session attack against Tectia SSH and unauthenticated remote code executio

desk verdict A solid empirical paper with two independently confirmed critical vulnerabilities in SSH strict KEX; the main claims hold up despite some convergence caveats. read the letter →

arxiv 2509.10895 v1 pith:PBZV56U2 submitted 2025-09-13 cs.CR

Fabian Bäumer , Marcel Maehren , Marcus Brinkmann , Jörg Schwenk This is my paper · ORCID
classification cs.CR
keywords SSHstrictkeyexchangestatemachinelearningprotocolfuzzingTerrapinattackmessageinjectionroguesessionremotecodeexecution
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

This paper sets out to determine whether real SSH servers correctly implement strict key exchange, the main deployed countermeasure to the Terrapin prefix-truncation attack. Using black-box state learning over a 94-symbol message alphabet, the authors infer handshake state machines for ten SSH server implementations across up to five key-exchange flow types. They find that seven of the ten tolerate optional or invalid messages during the handshake even though strict KEX requires immediate termination. Two such tolerances are shown to be practically exploitable: a man-in-the-middle can log a Tectia SSH client into the attacker's account, and an unauthenticated remote attacker can execute arbitrary code on Erlang SSH servers. The result matters because strict KEX is currently the main defense against Terrapin, and the paper shows that non-cryptographic handshake hardening is easy to get wrong and hard to notice.

What carries the argument

The method is black-box state learning of the SSH handshake phase: a TTT-style learner builds an input/output state machine from queries, a custom mapper translates abstract symbols into dynamically generated valid SSH messages (including messages normally sent by the server and undefined message IDs), and a purpose-built 'happy flow mutation' equivalence oracle inserts up to two arbitrary alphabet symbols at every position of the normal key-exchange flow, generating roughly 133,000 to 186,000 test sequences per flow. That combination lets the learner expose self-loops or unexpected transitions where a strict-KEX server should have closed the connection. The four violation categories (C1–C4)

What would settle it

Re-running the happy-flow mutation oracle (up to two arbitrary alphabet symbols inserted at every position of the ECDH, DH, DHGEX, RSA, and PQ-hybrid happy flows, with strict KEX active) against all ten servers and finding that fewer than seven implementations accept a misplaced message and still reach user-authentication service would refute the paper's central count.

Watch

Extended reading notes

Core claim

The central claim is that strict KEX, as implemented, does not produce the clean linear handshake it was meant to produce: seven of ten surveyed server implementations accept at least one message that the specification says must terminate the connection. The violations fall into four recurring categories—injection before KEXINIT, injection that depends on the negotiated key-exchange algorithm, blocklists that miss some message types, and restrictions lifted after the server sends NEWKEYS instead of after it receives the client's NEWKEYS. For Tectia SSH, the paper constructs a rogue session attack: a man-in-the-middle injects a USERAUTH_REQUEST with attacker credentials before the handshake c

Load-bearing premise

The load-bearing assumption is that every tested server correctly implements the sequence-number-reset half of strict KEX, so only message-acceptance behavior needs to be audited; if any server mishandles the reset in a way that still allows a session, the learned state machines and the Tectia attack analysis could misattribute the behavior.

Editorial extensions

If this is right

  • Every violating server gives a network attacker a message-injection primitive during the handshake; the paper demonstrates practical exploitation for two of them.
  • Taint-based strict KEX, as used by Bitvise SSH and libssh, can be security-equivalent to strict compliance only if the taint flag is set for every forbidden message and checked before the secure channel opens.
  • The Dropbear and TinySSH C4 violations allow injection between the server's NEWKEYS and the client's NEWKEYS, which can desynchronize sequence numbers across the encryption boundary, directly breaching strict KEX's separation goal.
  • A full transcript verification mechanism, analogous to TLS 1.3's verify_data, would make handshake tampering cryptographically detectable, but the paper notes it would not have prevented the Erlang RCE because the attacker controls the entire transcript.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • Inference: The four violation categories likely generalize beyond the ten tested servers; any implementation using a blocklist rather than an allowlist of exact KEX messages is at risk for C3-style misses, and any server that lifts restrictions after sending NEWKEYS is at risk for C4.
  • Inference: Tectia's repeated USERAUTH_SUCCESS suggests other connection-layer processing may be similarly permissive during the handshake, so client-side state machines deserve the same state-learning treatment; the paper itself lists client analysis as future work.
  • Inference: Because the mapper assumes every NEWKEYS resets sequence numbers and installs cipher state, the learned models could misrepresent implementations that delay cipher activation; re-running with per-implementation mapper assumptions derived from source inspection would be a natural testable extension.
  • Inference: The paper's observation about AES-GCM invocation-counter injection may apply even to strict-KEX-compliant implementations using AES-GCM, since strict KEX does not address the counter's initialization; checking whether any of the ten servers accept an injected packet under AES-GCM would be a concrete follow-up test.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

1 major / 5 minor

Summary. The paper analyzes SSH implementations that support the strict key exchange (strict KEX) countermeasure to the Terrapin attack. The authors learn state machines of ten SSH servers across up to five key-exchange flow types using a novel mapper with a 94-symbol alphabet and a targeted 'happy flow mutation' equivalence oracle. They report that seven of the ten implementations violate the strict KEX specification, and that two of the violations are exploitable: a rogue session attack against Tectia SSH (CVE-2025-32942) and pre-authentication remote code execution in Erlang SSH (CVE-2025-32433). Each reported violation is confirmed by a manually crafted protocol flow executed outside the learner, and the artifacts include PoCs and learned state machines.

Significance. If the findings hold, this is a significant contribution: it is the first systematic study of strict KEX implementations, shows that a security countermeasure designed to prevent a critical attack is widely misimplemented, and demonstrates two critical vulnerabilities in real-world SSH servers. The methodological work—particularly the dynamic mapper and the equivalence oracle designed for state learning of the SSH handshake—is also valuable beyond this specific setting. The paper is strengthened by vendor confirmations, assigned CVEs, and a public artifact package with reproducible PoCs. The two vulnerability results are independently verified and therefore robust even if the learning methodology has limitations.

major comments (1)
  1. [Section 4, Table 2; Abstract] The paper's central claim that 'seven implementations violate the strict KEX specification' depends on an operational definition that is not stated until §3.7/§4.2: a violation is counted only if the server can still complete the transport layer and accept a service request despite the forbidden message. Under this definition, taint-based implementations (Bitvise, libssh) are excluded even though §4.2 admits they are 'not strictly compliant with the specification.' Additionally, three of the counted implementations (Tectia, LANCOM, and libssh-DHGEX) come from learning runs that were manually terminated after one hour and analyzed from the last hypothesis. The abstract and introduction should state the operational definition of 'violation' explicitly, and Table 2 should mark entries derived from non-converged runs, so readers can correctly interpret the headline count.
minor comments (5)
  1. [References] The reference list contains duplicates: [60] and [61] are the same paper. In addition, the related-work text attributes the work in [45] to 'Dong et al.' but the reference is by Rashid et al.; the attribution should be corrected.
  2. [Section 4.3] The Tectia rogue session attack was confirmed with OpenSSH and PuTTY clients only. This client-dependence should be stated in §6.4 as a limitation of the exploit analysis.
  3. [Section 3.4] The formula for the number of generated sequences uses |F| without defining it in the surrounding text. Define |F| as the length of the happy flow symbol sequence at the point where the counting formula appears.
  4. [Section 6.4] The sentence 'the number of cache conflicts renders our approach infeasible' is too strong; the paper did complete learning for most systems. Use 'can render' or qualify the statement to acknowledge the successful runs.
  5. [Figure 2] Figure 2 is very dense and hard to read because it combines the happy-flow message sequence with a large partial state machine. Consider splitting it into two figures or simplifying the state machine for readability.

Circularity Check

0 steps flagged · score 1.0 of 10

No significant circularity: all central claims are empirically verified and do not reduce to fitted inputs or self-citations.

full rationale

The paper is an empirical state-learning study, not a derivation from first principles. Its central claims are that seven of ten SSH servers violate strict KEX and that two of those violations are exploitable. Each reported violation is independently confirmed outside the learning loop: Section 3.7 states that for any deviation, the authors 'manually implement a dedicated test flow using our SSH implementation to confirm and further investigate the impact of the identified issues,' and that a violation is only considered confirmed if 'the server responds to this request by accepting the service despite the strict KEX violation present.' The two vulnerabilities are additionally supported by proof-of-concept exploits, vendor acknowledgments, and CVEs (CVE-2025-32433, CVE-2025-32942), which are external validations. The happy-flow mutation oracle is deliberately aimed at finding strict KEX violations, but this is a search strategy, not a way of baking in the answer: the oracle enumerates message insertions, and the observed behavior comes from the server under test. The paper's assumption that sequence-number reset is correct (Section 2.1, Section 3.5) is a stated limitation, not a circular step, because the mapper is a standard-compliant SSH stack; if a server mishandled the reset, MAC verification on the first encrypted message would fail and the session could not reach the authentication stage used to confirm violations. Self-citations to the Terrapin paper [6] appear in the background and in the comparison of the rogue-session attack, but they are not load-bearing: the Tectia rogue-session attack relies on strict KEX's sequence-number reset and Tectia's specific handling of authentication requests, behaviors that are observed and replayed in this work, not assumed from prior work. No fitted parameter is renamed as a prediction, and no uniqueness theorem is imported from the authors' prior work. The paper is self-contained against external benchmarks (independent PoCs and CVEs), so the appropriate finding is no significant circularity, with only a minor self-citation in the background that does not affect the validity of the results.

Assumptions & free parameters 5 free parameters · 5 assumptions · 0 invented entities

No new physical or protocol entities are introduced; the 'tainted' state is an abstraction of existing implementation behavior. The free parameters are methodological thresholds that bound the search space. The axioms are the load-bearing modeling assumptions: determinism, SQN reset correctness, NEWKEYS state behavior, KEXINIT parameter independence, and the taint-acceptability interpretation.

free parameters (5)
  • happy flow mutation: max insertions n = 2
    Section 3.4: the equivalence oracle exhaustively tries all combinations of up to n inserted symbols. n=2 with 94-symbol alphabet yields 133,011 (or 186,121 for DHGEX) sequences; higher n would improve coverage but increase runtime.
  • random words oracle run count and length = 10,000 sequences, length 5 to 15 symbols
    Section 3.4: the random words supplement to the equivalence oracle. These values bound the search for counterexamples outside the happy flow; changing them would change post-handshake state discovery.
  • learning timeout for non-converging systems = 1 hour
    Section 4: Tectia SSH, LANCOM LCOS, and libssh-DHGEX did not converge and were manually terminated after one hour; the last hypothesis was used for analysis. This threshold affects completeness of the violation set.
  • majority voting population for cache conflicts = 13
    Sections 3.1 and 6.4: when replayed prefixes conflict with the cache, the disputed output is resolved by 13-query majority voting. The choice affects how non-determinism is filtered.
  • static client banner string = SSH-2.0-OpenSSH_9.0
    Section 3.6: the client banner is fixed to this value because some servers use banners to activate compatibility modes. A different banner could alter the learned state machines.
assumptions (5)
  • domain assumption The SUL (server under learning) is deterministic and cache/majority voting can resolve non-determinism.
    Active automata learning assumes a deterministic system; Section 3.1 and 6.4 describe cache conflicts and a 13-query majority vote to handle timing and cryptographic randomness. If non-determinism is not fully resolved, learned states can be artifacts.
  • domain assumption The strict KEX sequence number reset is correctly implemented in all tested servers.
    Section 2.1: 'As any violation of the sequence number reset would prevent a peer from using the secure channel, we assume it is correctly implemented.' The paper only audits message acceptance, so combined SQN reset and message-handling bugs would be missed.
  • domain assumption Every NEWKEYS message switches the peer to the pending cipher state and resets sequence numbers, as assumed by the mapper.
    Section 3.5 and 6.4: if the peer does not actually change cipher state or reset SQN when the mapper does, the session state misaligns and the learned machine can contain artificial states. This is an acknowledged modeling assumption.
  • domain assumption Choices of encryption, MAC, and compression algorithms in KEXINIT do not affect the handshake state machine.
    Section 3.3 states this explicitly and leaves a study of such side effects out of scope. If false for a tested server, the learned per-KEX-flow machines may not cover the server's real behavior.
  • domain assumption A taint-based implementation that delays connection termination until the end of key exchange can be considered acceptable if it sets a taint flag on all forbidden messages.
    Section 4.2 defines this interpretation: Bitvise/libssh taint approach is 'not strictly compliant' but not counted as an inherent violation unless other violations exist. This interpretive choice shapes the seven-violation count.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Finding SSH Strict Key Exchange Violations by State Learning." pith.science (2026). https://pith.science/paper/PBZV56U2

@misc{pith2026250910895,
  author       = {Pith},
  title        = {Pith review of: Finding SSH Strict Key Exchange Violations by State Learning},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/PBZV56U2}},
  note         = {Machine review of arXiv:2509.10895}
}
read the original abstract

SSH is an important protocol for secure remote shell access to servers on the Internet. At USENIX 2024, B\"aumer et al. presented the Terrapin attack on SSH, which relies on the attacker injecting optional messages during the key exchange. To mitigate this attack, SSH vendors adopted an extension developed by OpenSSH called strict key exchange ("strict KEX"). With strict KEX, optional messages are forbidden during the handshake, preventing the attack. In practice, this should simplify the state machine of an SSH handshake to a linear message flow similar to that of TLS. In this work, we analyze the design, implementation, and security of strict KEX in popular SSH servers, using black-box state learning, which can uncover the hidden state machine of an implementation. In practice, it is limited by the number of learned messages and the complexity of the state machine. Thus, learning the complete state machine of SSH is infeasible. Previous research on SSH, therefore, excluded optional messages, learning only a partial state machine. However, these messages are a critical part of the Terrapin attack. We propose to instead learn the complete state machine of the handshake phase of an SSH server, but with strict KEX enabled. We investigate the security of ten SSH implementations supporting strict KEX for up to five key exchange algorithms. In total, we learn 33 state machines, revealing significant differences in the implementations. We show that seven implementations violate the strict KEX specification and find two critical security vulnerabilities. One results in a rogue session attack in the proprietary Tectia SSH implementation. Another affects the official SSH implementation of the Erlang Open Telecom Platform, and enables unauthenticated remote code execution in the security context of the SSH server.

Figures

Figures reproduced from arXiv: 2509.10895 by the authors.

Figure 1
Figure 1. A simplified state machine of a strict KEX [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. First, an ASCII banner is exchanged, followed by a [PITH_FULL_IMAGE:figures/full_fig_p004_2.png] view at source ↗
Figure 3
Figure 3. Illustration of the components of our state learner. [PITH_FULL_IMAGE:figures/full_fig_p005_3.png] view at source ↗
Figures from the paper (3 more)
Figure 4
Figure 4. Figure 4: Idealized state machines illustrating different strict KEX violation categories which were observed during the [PITH_FULL_IMAGE:figures/full_fig_p009_4.png]
Figure 5
Figure 5. Figure 5: Taint-based implementation of strict KEX used by [PITH_FULL_IMAGE:figures/full_fig_p010_5.png]
Figure 7
Figure 7. Figure 7: Remote code execution in Erlang SSH. A malicious [PITH_FULL_IMAGE:figures/full_fig_p011_7.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

64 extracted references · 15 canonical work pages

  1. [1]

    Albrecht, Kenneth G

    Martin R. Albrecht, Kenneth G. Paterson, and Gaven J. Watson. 2009. Plaintext Recovery Attacks against SSH. In 2009 IEEE Symposium on Security and Privacy . IEEE Computer Society Press, Oakland, CA, USA, 16–26. https://doi.org/10.1109/ SP.2009.5

    2009

  2. [2]

    An Automated Blackbox Noncompliance Checker for QUIC Server Implementations

    Kian Kai Ang, Guy Farrelly, Cheryl Pope, and Damith C. Ranasinghe. 2025. An Automated Blackbox Noncompliance Checker for QUIC Server Implementa- tions. CoRR abs/2505.12690 (2025). https://doi.org/10.48550/ARXIV.2505.12690 arXiv:2505.12690

    work page Pith review arXiv doi:10.48550/arxiv.2505.12690 2025

  3. [3]

    Dana Angluin. 1987. Learning regular sets from queries and counterexamples. Information and computation 75, 2 (1987), 87–106

    1987

  4. [4]

    Keromytis, and Aggelos Kiayias

    George Argyros, Ioannis Stais, Suman Jana, Angelos D. Keromytis, and Aggelos Kiayias. 2016. SFADiff: Automated Evasion Attacks and Fingerprinting Using Black-box Differential Automata Learning. In ACM CCS 2016, Edgar R. Weippl, Stefan Katzenbeisser, Christopher Kruegel, Andrew C. Myers, and Shai Halevi (Eds.). ACM Press, Vienna, Austria, 1690–1701. https:...

    doi:10.1145/2976749 2016

  5. [5]

    Fabian Bäumer, Marcus Brinkmann, Nurullah Erinola, Sven Hebrok, Nico Heit- mann, Felix Lange, Marcel Maehren, Robert Merget, Niklas Niere, Maximilian Radoy, Conrad Schmidt, Jörg Schwenk, and Juraj Somorovsky. 2024. TLS-Attacker: A Dynamic Framework for Analyzing TLS Implementations. InProceedings of Cy- bersecurity Artifacts Competition and Impact A ward ...

    2024

  6. [6]

    Fabian Bäumer, Marcus Brinkmann, and Jörg Schwenk. 2024. Terrapin Attack: Breaking SSH Channel Integrity By Sequence Number Manipulation. In USENIX Security 2024, Davide Balzarotti and Wenyuan Xu (Eds.). USENIX Association, Philadelphia, PA, USA. https://www.usenix.org/conference/usenixsecurity24/ presentation/b%C3%A4umer

    2024

  7. [7]

    Mihir Bellare, Tadayoshi Kohno, and Chanathip Namprempre. 2002. Authenti- cated Encryption in SSH: Provably Fixing The SSH Binary Packet Protocol. In ACM CCS 2002, Vijayalakshmi Atluri (Ed.). ACM Press, Washington, DC, USA, 1–11. https://doi.org/10.1145/586110.586112

    arXiv 2002

  8. [8]

    Florian Bergsma, Benjamin Dowling, Florian Kohlar, Jörg Schwenk, and Douglas Stebila. 2014. Multi-Ciphersuite Security of the Secure Shell (SSH) Protocol. In ACM CCS 2014, Gail-Joon Ahn, Moti Yung, and Ninghui Li (Eds.). ACM Press, Scottsdale, AZ, USA, 369–381. https://doi.org/10.1145/2660267.2660286

    arXiv 2014

Show all 64 references
  1. [9]

    Karthikeyan Bhargavan and Gaëtan Leurent. 2016. Transcript Collision Attacks: Breaking Authentication in TLS, IKE and SSH. InNDSS 2016. The Internet Society, San Diego, CA, USA. https://doi.org/10.14722/ndss.2016.23418

    2016

  2. [10]

    Denis Bider. 2018. Extension Negotiation in the Secure Shell (SSH) Protocol. RFC

    2018

  3. [11]

    Merlin Chlosta, David Rupprecht, and Thorsten Holz. 2021. On the challenges of automata reconstruction in LTE networks. In Proceedings of the 14th ACM Conference on Security and Privacy in Wireless and Mobile Networks (Abu Dhabi, United Arab Emirates) (WiSec ’21). Association ...

    2021

  4. [12]

    Lesly-Ann Daniel, Erik Poll, and Joeri de Ruiter. 2018. Inferring OpenVPN State Machines Using Protocol State Fuzzing. In 2018 IEEE European Symposium on Security and Privacy Workshops (EuroS&PW) . 11–19. https://doi.org/10.1109/ EuroSPW.2018.00009

    2018

  5. [13]

    Joeri de Ruiter. 2016. A Tale of the OpenSSL State Machine: A Large-Scale Black- Box Analysis. In Secure IT Systems , Billy Bob Brumley and Juha Röning (Eds.). Springer International Publishing, Cham, 169–184

    2016

  6. [14]

    Joeri de Ruiter and Erik Poll. 2015. Protocol State Fuzzing of TLS Implementations. In USENIX Security 2015, Jaeyeon Jung and Thorsten Holz (Eds.). USENIX Asso- ciation, Washington, DC, USA, 193–206. https://www.usenix.org/conference/ usenixsecurity15/technical-sessions/presen...

    2015

  7. [15]

    Yilu Dong, Tianchang Yang, Abdullah Al Ishtiaq, Syed Md Mukit Rashid, Ali Ranjbar, Kai Tu, Tianwei Wu, Md Sultan Mahmud, and Syed Rafiul Hussain. 2025. CoreCrisis: Threat-Guided and Context-Aware Iterative Learning and Fuzzing of 5G Core Networks. In 34th USENIX Security Sympo...

    2025

  8. [16]

    Tiago Ferreira, Harrison Brewton, Loris D’Antoni, and Alexandra Silva. 2021. Prognosis: closed-box analysis of network protocol implementations. In Pro- ceedings of the 2021 ACM SIGCOMM 2021 Conference (Virtual Event, USA) (SIG- COMM ’21). Association for Computing Machinery, ...

    2021

  9. [17]

    Paul Fiterau-Brostean, Bengt Jonsson, Robert Merget, Joeri de Ruiter, Kon- stantinos Sagonas, and Juraj Somorovsky. 2020. Analysis of DTLS Implemen- tations Using Protocol State Fuzzing. In USENIX Security 2020 , Srdjan Cap- kun and Franziska Roesner (Eds.). USENIX Association...

    2020

  10. [18]

    Paul Fiterau-Brostean, Bengt Jonsson, Konstantinos Sagonas, and Fredrik Tåquist

  11. [19]

    Paul Fiterău-Broştean, Toon Lenaerts, Erik Poll, Joeri de Ruiter, Frits Vaan- drager, and Patrick Verleg. 2017. Model learning and model checking of SSH implementations. In Proceedings of the 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software (Santa Ba...

    2017

  12. [20]

    Martin Forssen and Frank Cusack. 2006. Generic Message Exchange Authenti- cation for the Secure Shell Protocol (SSH). RFC 4256. https://doi.org/10.17487/ RFC4256

    2006

  13. [21]

    Markus Friedl, Niels Provos, and William A. Simpson. 2006. Diffie-Hellman Group Exchange for the Secure Shell (SSH) Transport Layer Protocol. RFC 4419. https://doi.org/10.17487/RFC4419 Finding SSH Strict Key Exchange Violations by State Learning CCS ’25, October 13–17, 2025, T...

    2006 doi

  14. [22]

    Garbelini, Chundong Wang, Sudipta Chattopadhyay, Sun Sumei, and Ernest Kurniawan

    Matheus E. Garbelini, Chundong Wang, Sudipta Chattopadhyay, Sun Sumei, and Ernest Kurniawan. 2020. SweynTooth: Unleashing Mayhem over Bluetooth Low Energy. In 2020 USENIX Annual Technical Conference (USENIX ATC 20) . USENIX Association, 911–925. https://www.usenix.org/conferen...

    2020

  15. [23]

    Jiaxing Guo, Chunxiang Gu, Xi Chen, and Fushan Wei. 2019. Model Learning and Model Checking of IPSec Implementations for Internet of Things. IEEE Access 7 (2019), 171322–171332. https://doi.org/10.1109/ACCESS.2019.2956062

    2019

  16. [24]

    Torben Brandt Hansen. 2020. Cryptographic Security of SSH Encryption Schemes . PhD thesis. University of London

    2020

  17. [25]

    Ben Harris. 2006. RSA Key Exchange for the Secure Shell (SSH) Transport Layer Protocol. RFC 4432. https://doi.org/10.17487/RFC4432

    2006 doi

  18. [26]

    Alex Halderman

    Nadia Heninger, Zakir Durumeric, Eric Wustrow, and J. Alex Halderman. 2012. Mining Your Ps and Qs: Detection of Widespread Weak Keys in Network Devices. In USENIX Security 2012 , Tadayoshi Kohno (Ed.). USENIX Association, Belle- vue, WA, USA, 205–220. https://www.usenix.org/co...

    2012

  19. [27]

    Syed Rafiul Hussain, Imtiaz Karim, Abdullah Al Ishtiaq, Omar Chowdhury, and Elisa Bertino. 2021. Noncompliance as Deviant Behavior: An Automated Black- box Noncompliance Checker for 4G LTE Cellular Devices. In ACM CCS 2021 , Giovanni Vigna and Elaine Shi (Eds.). ACM Press, Vir...

    2021

  20. [28]

    Kevin Igoe and Jerome Solinas. 2009. AES Galois Counter Mode for the Secure Shell Transport Layer Protocol. RFC 5647. https://doi.org/10.17487/RFC5647

    2009 doi

  21. [29]

    Malte Isberner, Falk Howar, and Bernhard Steffen. 2014. The TTT Algorithm: A Redundancy-Free Approach to Active Automata Learning. In Runtime Verifica- tion, Borzoo Bonakdarpour and Scott A. Smolka (Eds.). Springer International Publishing, Cham, 307–322

    2014

  22. [30]

    Malte Isberner, Falk Howar, and Bernhard Steffen. 2015. The Open-Source Learn- Lib. In Computer Aided Verification, Daniel Kroening and Corina S. Păsăreanu (Eds.). Springer International Publishing, Cham, 487–495

    2015

  23. [31]

    Imtiaz Karim, Abdullah Al Ishtiaq, Syed Rafiul Hussain, and Elisa Bertino. 2023. BLEDiff: Scalable and Property-Agnostic Noncompliance Checking for BLE Im- plementations. In 2023 IEEE Symposium on Security and Privacy . IEEE Computer Society Press, San Francisco, CA, USA, 3209...

    2023

  24. [32]

    Lee and M

    D. Lee and M. Yannakakis. 1996. Principles and methods of testing finite state machines-a survey. Proc. IEEE 84, 8 (1996), 1090–1123. https://doi.org/10.1109/5. 533956

    1996 doi

  25. [33]

    Lonvick and Sami Lehtinen

    Chris M. Lonvick and Sami Lehtinen. 2006. The Secure Shell (SSH) Protocol Assigned Numbers. RFC 4250. https://doi.org/10.17487/RFC4250

    2006 doi

  26. [34]

    Lonvick and Tatu Ylonen

    Chris M. Lonvick and Tatu Ylonen. 2006. The Secure Shell (SSH) Authentication Protocol. RFC 4252. https://doi.org/10.17487/RFC4252

    2006 doi

  27. [35]

    Lonvick and Tatu Ylonen

    Chris M. Lonvick and Tatu Ylonen. 2006. The Secure Shell (SSH) Connection Protocol. RFC 4254. https://doi.org/10.17487/RFC4254

    2006 doi

  28. [36]

    Lonvick and Tatu Ylonen

    Chris M. Lonvick and Tatu Ylonen. 2006. The Secure Shell (SSH) Protocol Archi- tecture. RFC 4251. https://doi.org/10.17487/RFC4251

    2006 doi

  29. [37]

    Lonvick and Tatu Ylonen

    Chris M. Lonvick and Tatu Ylonen. 2006. The Secure Shell (SSH) Transport Layer Protocol. RFC 4253. https://doi.org/10.17487/RFC4253

    2006 doi

  30. [38]

    Marcel Maehren, Nurullah Erinola, Robert Merget, Jörg Schwenk, and Juraj Somorovsky. 2025. Towards Internet-Based State Learning of TLS State Machines. In 34th USENIX Security Symposium (USENIX Security 25) . 7097–7116

    2025

  31. [39]

    Damien Miller. 2025. SSH Strict KEX extension . Internet-Draft draft-ietf-sshm- strict-kex-00. Internet Engineering Task Force. https://datatracker.ietf.org/doc/ draft-ietf-sshm-strict-kex/00/ Work in Progress

    2025

  32. [40]

    Miller, and Darren Tucker

    Damien Miller, Markus Friedl, Mike Frysinger, Todd C. Miller, and Darren Tucker

  33. [41]

    Soo-Jin Moon, Jeffrey Helt, Yifei Yuan, Yves Bieri, Sujata Banerjee, Vyas Sekar, Wenfei Wu, Mihalis Yannakakis, and Ying Zhang. 2019. Alembic: Automated Model Inference for Stateful Network Functions. In 16th USENIX Symposium on Networked Systems Design and Implementation (NSD...

    2019

  34. [42]

    Paterson and Gaven J

    Kenneth G. Paterson and Gaven J. Watson. 2010. Plaintext-Dependent Decryption: A Formal Security Treatment of SSH-CTR. In EUROCRYPT 2010 (LNCS, Vol. 6110), Henri Gilbert (Ed.). Springer Berlin Heidelberg, Germany, French Riviera, 345–

    2010

  35. [43]

    Aichernig

    Andrea Pferscher and Bernhard K. Aichernig. 2021. Fingerprinting Bluetooth Low Energy Devices via Active Automata Learning. In Formal Methods, Marieke Huisman, Corina Păsăreanu, and Naijun Zhan (Eds.). Springer International Publishing, Cham, 524–542

    2021

  36. [44]

    Aichernig

    Andrea Pferscher and Bernhard K. Aichernig. 2022. Stateful Black-Box Fuzzing of Bluetooth Devices Using Automata Learning. In NASA Formal Methods, Jyotir- moy V. Deshmukh, Klaus Havelund, and Ivan Perez (Eds.). Springer International Publishing, Cham, 373–392

    2022

  37. [45]

    Mukit Rashid, Tianwei Wu, Kai Tu, Abdullah Al Ishtiaq, Ridwanul Hasan Tanvir, Yilu Dong, Omar Chowdhury, and Syed Rafiul Hussain

    Syed Md. Mukit Rashid, Tianwei Wu, Kai Tu, Abdullah Al Ishtiaq, Ridwanul Hasan Tanvir, Yilu Dong, Omar Chowdhury, and Syed Rafiul Hussain. 2024. State Ma- chine Mutation-based Testing Framework for Wireless Communication Pro- tocols. In ACM CCS 2024 , Bo Luo, Xiaojing Liao, Ju...

    2024

  38. [46]

    Aina Toky Rasoamanana, Olivier Levillain, and Hervé Debar. 2022. Towards a Systematic and Automatic Use of State Machine Inference to Uncover Security Flaws and Fingerprint TLS Stacks. In ESORICS 2022, Part III (LNCS, Vol. 13556) , Vijayalakshmi Atluri, Roberto Di Pietro, Chri...

    2022 doi

  39. [47]

    Abdullah Rasool, Greg Alpár, and Joeri de Ruiter. 2019. State machine inference of QUIC. CoRR abs/1903.04384 (2019). arXiv:1903.04384 http://arxiv.org/abs/ 1903.04384

    2019 arXiv

  40. [48]

    Phillip Remaker and Joseph Galbraith. 2006. The Secure Shell (SSH) Session Channel Break Extension. RFC 4335. https://doi.org/10.17487/RFC4335

    2006 doi

  41. [49]

    Eric Rescorla. 2018. The Transport Layer Security (TLS) Protocol Version 1.3. RFC 8446. https://doi.org/10.17487/RFC8446

    2018 doi

  42. [50]

    Keromytis, and Suman Jana

    Suphannee Sivakorn, George Argyros, Kexin Pei, Angelos D. Keromytis, and Suman Jana. 2017. HVLearn: Automated Black-Box Analysis of Hostname Verification in SSL/TLS Implementations. In 2017 IEEE Symposium on Secu- rity and Privacy . IEEE Computer Society Press, San Jose, CA, U...

    2017 doi

  43. [51]

    Wouter Smeenk, Joshua Moerman, Frits Vaandrager, and David N. Jansen. 2015. Applying Automata Learning to Embedded Control Software. In Formal Methods and Software Engineering , Michael Butler, Sylvain Conchon, and Fatiha Zaïdi (Eds.). Springer International Publishing, Cham, 67–83

    2015

  44. [52]

    Juraj Somorovsky. 2016. Systematic Fuzzing and Testing of TLS Libraries. In ACM CCS 2016 , Edgar R. Weippl, Stefan Katzenbeisser, Christopher Kruegel, Andrew C. Myers, and Shai Halevi (Eds.). ACM Press, Vienna, Austria, 1492–1504. https://doi.org/10.1145/2976749.2978411

    2016

  45. [53]

    Wagner, and Xuqing Tian

    Dawn Xiaodong Song, David A. Wagner, and Xuqing Tian. 2001. Timing Analysis of Keystrokes and Timing Attacks on SSH. In USENIX Security 2001 , Dan S. Wallach (Ed.). USENIX Association, Washington, DC, USA. http://www.usenix. org/publications/library/proceedings/sec01/song.html

    2001

  46. [54]

    Douglas Stebila and Jonathan Green. 2009. Elliptic Curve Algorithm Integration in the Secure Shell Transport Layer. RFC 5656. https://doi.org/10.17487/RFC5656

    2009 doi

  47. [55]

    Chris McMahon Stone, Tom Chothia, and Joeri de Ruiter. 2018. Extending Automated Protocol State Learning for the 802.11 4-Way Handshake. In ES- ORICS 2018, Part I (LNCS, Vol. 11098) , Javier López, Jianying Zhou, and Miguel Soriano (Eds.). Springer, Cham, Switzerland, Barcelon...

    2018 doi

  48. [56]

    Thomas, Mathy Vanhoef, James Henderson, Nico- las Bailluet, and Tom Chothia

    Chris McMahon Stone, Sam L. Thomas, Mathy Vanhoef, James Henderson, Nico- las Bailluet, and Tom Chothia. 2022. The Closer You Look, The More You Learn: A Grey-box Approach to Protocol State Machine Learning. In ACM CCS 2022, Heng Yin, Angelos Stavrou, Cas Cremers, and Elaine S...

    2022

  49. [57]

    Max Tijssen. 2014. Automatic modeling of SSH implementations with state machine learning algorithms. Bachelor’s thesis, Radboud University Nijmegen. Supervised by Erik Poll and Joeri de Ruiter

    2014

  50. [58]

    Mukit Rashid, Yilu Dong, Weixuan Wang, Tianwei Wu, and Syed Rafiul Hussain

    Kai Tu, Abdullah Al Ishtiaq, Syed Md. Mukit Rashid, Yilu Dong, Weixuan Wang, Tianwei Wu, and Syed Rafiul Hussain. 2024. Logic Gone Astray: A Security Analysis Framework for the Control Plane Protocols of 5G Basebands. InUSENIX Security 2024, Davide Balzarotti and Wenyuan Xu (E...

    2024

  51. [59]

    Williams

    Stephen C. Williams. 2011. Analysis of the SSH Key Exchange Protocol. In 13th IMA International Conference on Cryptography and Coding (LNCS, Vol. 7089) , Liqun Chen (Ed.). Springer Berlin Heidelberg, Germany, Oxford, UK, 356–374. https://doi.org/10.1007/978-3-642-25516-8_22

    2011 doi

  52. [61]

    Tarun Yadav and Koustav Sadhukhan. 2019. Identification of Bugs and Vulnerabil- ities in TLS Implementation for Windows Operating System Using State Machine Learning. In Security in Computing and Communications , Sabu M. Thampi, San- jay Madria, Guojun Wang, Danda B. Rawat, an...

    2019

  53. [361]

    https://doi.org/10.1007/978-3-642-13190-5_18

    doi

  54. [2023]

    In NDSS 2023

    Automata-Based Automated Detection of State Machine Bugs in Protocol Implementations. In NDSS 2023. The Internet Society, San Diego, CA, USA

    2023

  55. [2024]

    https://cvsweb.openbsd.org/cgi-bin/cvsweb/src/usr.bin/ssh/ PROTOCOL?rev=1.55 Accessed: 2025-04-14

    This documents OpenSSH’s deviations and extensions to the published SSH protocol. https://cvsweb.openbsd.org/cgi-bin/cvsweb/src/usr.bin/ssh/ PROTOCOL?rev=1.55 Accessed: 2025-04-14

    2025

  56. [8308]

    https://doi.org/10.17487/RFC8308

    doi

Pith tools

Reviewed August 4, 2026 · model on record in the stance chip above.