[Resource Topic] 2004/059: Symmetric Encryption in a Simulatable Dolev-Yao Style Cryptographic Library

Welcome to the resource topic for 2004/059

Title:
Symmetric Encryption in a Simulatable Dolev-Yao Style Cryptographic Library

Authors: Michael Backes, Birgit Pfitzmann

Abstract:

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.

ePrint: https://eprint.iacr.org/2004/059

See all topics related to this paper.

Feel free to post resources that are related to this paper below.

Example resources include: implementations, explanation materials, talks, slides, links to previous discussions on other websites.

For more information, see the rules for Resource Topics .