In this paper we propose a new security definition for key exchange protocols that offers two important benefits. Our notion is weaker than the more established ones and thus allows the analysis of a larger class of protocols. Furthermore, security in the sense that we define enjoys rather general composability properties. In addition our composability properties are derived within game based formalisms, and do not appeal to any simulation based paradigm.
Specifically, for protocols whose security relies exclusively on some underlying symmetric primitive we show that they can be securely composed with key exchange protocols provided that two main requirements hold: 1) no adversary can break the underlying {\em primitive}, even when the primitive uses keys obtained from executions of the key exchange protocol in the presence of the adversary (this is essentially the security requirement that we introduce and formalize in this paper), and 2) the security of the protocol can be reduced to that of the primitive, no matter how the keys for the primitive are distributed. 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. We exemplify our results in the case of a profile of the TLS protocol. Our definition and results are set entirely within the framework of cryptographic games (and thus avoid the use of simulation).
Category / Keywords: cryptographic protocols / Date: received 30 Apr 2012, last revised 21 Jan 2013 Contact author: nigel at cs bris ac uk,brzuska@cased de,marc fischlin@gmail com,bogdan@cs bris ac uk Available formats: PDF | BibTeX Citation Version: 20130121:135721 (All versions of this report) Discussion forum: Show discussion | Start new discussion