The structure of the protocol is one commonly encountered in practice: first run a key-exchange to establish a shared key (which performs authentication and key confirmation), only then use the channel to exchange application messages. Although common in practice, this structure takes the protocol out of the reach of most standard security models for key-exchange. Unfortunately, the only models that can cope with the above structure suffer from some drawbacks that make them unsuitable for our analysis. Our second contribution is to provide new security models for channel establishment protocols. Our models have a more inclusive syntax, are quite general, deal with a realistic notion of authentication (one-sided authentication as required by EMV), and do not suffer from the drawbacks that we identify in prior models.
Category / Keywords: applications / Date: received 24 Jan 2013, last revised 8 May 2013 Contact author: nigel at cs bris ac uk Available format(s): PDF | BibTeX Citation Version: 20130508:174904 (All versions of this report) Short URL: ia.cr/2013/031 Discussion forum: Show discussion | Start new discussion