Tool-supported proofs of security protocols typically rely on abstractions from real cryptography by term algebras, so-called Dolev-Yao models. Although there was traditionally no cryptographic justification, i.e., no theorem that said what a proof with a Dolev-Yao abstraction implied for the real implementation, significant progress has been made during the last years in showing that comprehensive Dolev-Yao models can be securely implemented using actual cryptographic primitives under standard assumptions on the deployed crypto. An important recent result showed that such a link can be achieved even if the considered protocol uses key cycles, e.g., encrypts a key with itself, provided that the encryption scheme satisfies a new security notion called KDM security. However, the adversary there was restricted to passive eavesdropping.

We extend KDM security to active attacks as well as to dynamic revelations of keys, both in unrestricted and polynomial-time versions; we call this (polynomial-time) AKDM and DKDM security. We prove that polynomial-time DKDM security is sufficient to securely realize a Dolev-Yao model of symmetric encryption with real symmetric encryption in the sense of reactive simulatability/UC without excluding key cycles while including joint terms with other operators such as signatures and message authentication codes. We furthermore prove relations among the definitions and present constructions of schemes secure under our new definitions. We also show (answering an open question from the literature) that not only encryption cycles of length 1 can be used to separate KDM security from semantic security but that counterexamples exist for key cycles of any length.