|
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.)
| 
