We consider security against adversaries that control all network traffic, can register arbitrary public keys, and can retrieve session keys. We do not attempt to mitigate damage from hardware failures, such as session-state compromise, as we aim to improve our understanding of this simpler setting. We give two natural but substantially different game based definitions of security and prove that they are equivalent. Such proofs are rare for SKA. The bulk of this proof consists of showing that, for secure protocols, only compatible processes can be made to share a key. This property is very natural but surprisingly subtle. For comparison, we give a version of our definition in which processes output session IDs and we give strong theorems relating these two types of definitions.
Category / Keywords: foundations / Key Exchange, Definitions, Public Key Infrastructure Date: received 7 Mar 2013 Contact author: wgeorge at cs toronto edu Available formats: PDF | BibTeX Citation Note: A very similar version of this paper was submitted to and rejected from TCC 2011 and TCC 2012. We had hoped to quickly create a revised version, but since we didn’t, we present this version as is.Version: 20130312:212356 (All versions of this report) Discussion forum: Show discussion | Start new discussion