Rigorous specifications of the SSH Transport Layer
Erik Poll, Aleksy Schubert · 2011
Abstract. This document presents (semi-)formal specifications of the security protocol SSH, more specifically the transport layer protocol, and describe a source code review of OpenSSH, the leading implementation of SSH, using these specifications. Our specifications, in the form of finite state machines, are at a different level of abstraction that the typical formal descriptions used to study security protocols. Our motivation is to understand actual implementations of SSH, so we try to capture some of the details from the official (informal) specification that are irrelevant to the security of the abstract protocol, but which do complicate the implementation. Our specifications should be useful to anyone trying to understand or implement SSH. First versions of our specifications were developed for the formal verification of a Java implementation of SSH [17]. 1