International Association
for Cryptologic Research

The abstraction of cryptographic operations by term algebras, called

Dolev-Yao models, is essential in almost all tool-supported methods

for verifying security protocols. Recently significant progress was

made in establishing computational soundness results: these results

prove that Dolev-Yao style models can be sound with respect to actual

cryptographic realizations and security definitions. However, these

results came at the cost of imposing various constraints on the set of

permitted security protocols: e.g., dishonestly generated keys must

not be used, key cycles need to be avoided, and many more. In a

nutshell, the cryptographic security definitions did not adequately

capture these cases, but were considered carved in stone; in contrast,

the symbolic abstractions were bent to reflect cryptographic features

and idiosyncrasies, thereby requiring adaptations of existing

verification tools.

In this paper, we pursue the opposite direction: we consider a

symbolic abstraction for public-key encryption and identify two

cryptographic definitions called PROG-KDM (programmable key-dependent

message) security and MKE (malicious-key extractable) security that we

jointly prove to be sufficient for obtaining computational soundness

without imposing assumptions on the protocols using this

abstraction. In particular, dishonestly generated keys obtained from

the adversary can be sent, received, and used. The definitions can be

met by existing cryptographic schemes in the random oracle model. This

yields the first computational soundness result for trace-properties

that holds for arbitrary protocols using this abstraction (in

particular permitting to send and receive dishonestly generated keys),

and that is accessible to all existing tools for reasoning about

Dolev-Yao models without further adaptations.