CWI Cryptology Group

Abstract: Computational soundness is a research direction that aims to bridge the gap between the computational (or complexity-based) and the symbolic (or formal methods-based) approaches to cryptography. In this talk I will describe the origins of the problem, the benefits of solving it, some of the inherent difficulties, as well as some of the existing results. As basis of discussion I will use an extension of the celebrated result of Abadi and Rogaway.

Abstract: The abstraction of cryptographic operations by term algebras, called Dolev-Yao models, is essential in almost all tool-supported methods for proving security protocols. Recently significant progress was made in proving that Dolev-Yao models offering the core cryptographic operations such as encryption and digital signatures can be sound with respect to actual cryptographic realizations and security definitions (computational soundness).
Recent work, however, has started to extend Dolev-Yao models to more sophisticated operations with unique security features. Zero-knowledge proofs arguably constitute the most amazing such extension. In this talk, we show how zero-knowledge proofs can be modelled in a Dolev-Yao model and analyse the cryptographic properties a zero-knowledge proof needs to fulfil to allow for computational soundness results.
Joint work with Michael Backes and Matteo Maffei.

Abstract: Standard security notions for encryption do not guarantee any security if the encrypted messages depend on the secret key. Yet it is exactly this stronger notion in the presence of key-dependent messages (KDM security) that is required in a number of applications: most prominently, KDM security plays an important role in analyzing multi-party protocols in a formal calculus. We give an overview over existing approaches to derive KDM secure schemes as well as over impossibility results concerning KDM security.