Date Added: May 2011
The authors provide an analysis of the widely deployed SSH protocol's key exchange mechanism. They exploit the design of the SSH key exchange to perform the analysis in a modular manner. First, a shared secret key is obtained via a Diffie-Hellman key exchange. Next, a transform is applied to obtain the application keys used by later stages of SSH. They define models, following well-established paradigms that clarify the security provided by each type of key. Previously, there has been no formal analysis of the SSH key exchange protocol. They provide a modular proof of security for the SSH shared secret and application keys.