Paper 2004/059

Symmetric Encryption in a Simulatable Dolev-Yao Style Cryptographic Library

Michael Backes and Birgit Pfitzmann


Recently we solved the long-standing open problem of justifying a Dolev-Yao type model of cryptography as used in virtually all automated protocol provers under active attacks. The justification was done by defining an ideal system handling Dolev-Yao-style terms and a cryptographic realization with the same user interface, and by showing that the realization is as secure as the ideal system in the sense of reactive simulatability. This definition encompasses arbitrary active attacks and enjoys general composition and property-preservation properties. Security holds in the standard model of cryptography and under standard assumptions of adaptively secure primitives. A major primitive missing in that library so far is symmetric encryption. We show why symmetric encryption is harder to idealize in a way that allows general composition than existing primitives in this library. We discuss several approaches to overcome these problems. For our favorite approach we provide a detailed provably secure idealization of symmetric encryption within the given framework for constructing nested terms.

Available format(s)
Publication info
Published elsewhere. Unknown where it was published
cryptographic protocolssecurity analysis of protocolsformal methodsDolev-Yaosymmetric encryptioncryptographically composable operators
Contact author(s)
mbc @ zurich ibm com
2004-02-23: received
Short URL
Creative Commons Attribution


      author = {Michael Backes and Birgit Pfitzmann},
      title = {Symmetric Encryption in a Simulatable Dolev-Yao Style Cryptographic Library},
      howpublished = {Cryptology ePrint Archive, Paper 2004/059},
      year = {2004},
      note = {\url{}},
      url = {}
Note: In order to protect the privacy of readers, does not use cookies or embedded third party content.