Automated analysis of SSH client state machines

State Machine Learning (SML) is a powerful technique to analyze the behavior of network protocol implementations. In this thesis, we apply SML to 12 SSH clients to examine their adherence to the SSH protocol specification. While SML enables automatic inference of protocol state machines, the manual analysis of these models is often time-consuming. Instead, we explore a differential-based analysis approach, where two different state machines are compared to highlight behavioral differences. For this, we apply the LTSDiff algorithm to SSH client state machines and systematically evaluate its effectiveness. We find that plain LTSDiff is insufficient, but that it can be tailored to work with Secure Shell (SSH) and used to identify meaningful differences. These differences reveal minor violations of the SSH transport protocol and hint at a broader issue of under- specification in the SSH standard. Fully automated detection of non-compliance remains challenging, as our differential analysis still requires expert interpretation in the absence of a comprehensive reference model.