In this paper, we pursue the opposite direction: we consider a symbolic abstraction for public-key encryption and identify two cryptographic definitions called PROG-KDM (programmable key-dependent message) security and MKE (malicious-key extractable) security that we jointly prove to be sufficient for obtaining computational soundness without imposing assumptions on the protocols using this abstraction. In particular, dishonestly generated keys obtained from the adversary can be sent, received, and used. The definitions can be met by existing cryptographic schemes in the random oracle model. This yields the first computational soundness result for trace-properties that holds for arbitrary protocols using this abstraction (in particular permitting to send and receive dishonestly generated keys), and that is accessible to all existing tools for reasoning about Dolev-Yao models without further adaptations.
Category / Keywords: foundations / protocol verification, computational soundness Publication Info: A short version appears at ACM CCS 2012 Date: received 22 Aug 2012 Contact author: unruh at ut ee Available format(s): PDF | BibTeX Citation Version: 20120822:232836 (All versions of this report) Short URL: ia.cr/2012/486