Limits of the Cryptographic Realization of Dolev-Yao-Style XOR

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 DolevYao models can be sound with respect to actual cryptographic realizations and security definitions. The strongest results show this in the sense of reactive simulatability/UC, a notion that essentially means the preservation of arbitrary security properties under arbitrary active attacks and in arbitrary protocol environments, with only small changes to both Dolev-Yao models and natural implementations. However, these results are so far restricted to cryptographic systems like encryption and signatures which essentially only have constructors and destructors, but no further algebraic properties. Typical modern tools and complexity results around Dolev-Yao models also allow more algebraic operations. The first such operation considered is typically XOR becaus...

• Type: Conference
• Year: 2005
• Where: ESORICS
• Authors: Michael Backes, Birgit Pfitzmann
• Keywords: Cryptographic, Cryptographic Systems, Dolev-yao Model, ESORICS 2005, Security Privacy