University of Tartu - ©2011 Rafik Chaabouni - Last update: 24.10.2012 11:02
Date: 24/10/2012 Location: J. Liivi 2, room 317 (next to the coffee room)
Speaker: Dominique Unruh
Title: Computational Soundness without Protocol Restrictions
Abstract:
The abstraction of cryptographic operations by term algebras, called Dolev-Yao models, is essential in almost all tool-supported methods for verifying security protocols. Recently significant progress was made in establishing computational soundness results: these results prove that Dolev-Yao style models can be sound with respect to actual cryptographic realizations and security definitions. However, these results came at the cost of imposing various constraints on the set of permitted security protocols: e.g., dishonestly generated keys must not be used, key cycles need to be avoided, and many more.
In this talk, we present novel cryptographic security notions for encryption schemes that allow us to get around these limitations: PROG-KDM (programmable key-dependent message security) and MKE (malicious key extractability). Using these notions, we get the first computational soundness result that does not restrict the use of keys.