On the security of key exchange protocols

• Main Author: Williams, Stephen C.
• Published: University of Bristol 2011
• Subjects: 004.6
• Online Access: http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.556744

This thesis is primarily concerned with the security of key exchange protocols. Specifically, we consider composability properties for such protocols within the tradi- tional game-based framework. Our composition results are distinguished from virtually all existing work as we do not rely, neither directly nor indirectly, on the simulation paradigm. In addition we provide a formal analysis of the widely deployed SSH pro- tocol's key exchange mechanism. As a first step, we show composability properties for key exchange protocols secure in the prevalent model of Bellare and Rogaway. Roughly speaking, we show these may be composed with arbitrary two-party protocols that require symmetrically distributed keys. Here, we use session identifiers derived by the protocol to define notions of partner sessions. This leads to an interesting technical requirement, namely, it should be possible to determine which sessions are partnered given only the publicly available information. Next, we propose a new security definition for key exchange protocols. The defini- tion offers two important benefits. It is weaker than the more established ones and thus allows for the analysis of a larger class of protocols. Furthermore, security in the sense that we define enjoys rather general composability properties. In essence, we show that a key exchange can be securely composed with some other protocol, provided two main requirements hold. First, the security of the protocol can be reduced to that of some primitive, no matter how the keys for the primitive are distributed. Secondly, no adversary can break the primitive when keys for the primitive are obtained from execu- tions of the key exchange protocol. Proving that the two conditions are satisfied, and then applying our generic theorem, should be simpler than performing a monolithic analysis of the composed protocol. Finally, we provide a security analysis of the key exchange stage of the SSH protocol. Our proof is modular, and exploits the design of SSH. 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. We define models, following well- established paradigms, that clarify the security provided by each type of key. We show that although the shared secret key exchanged by SSH is not indistinguishable, the transformation then applied yields indistinguishable application keys.