Explicit Randomness is not Necessary when Modeling Probabilistic Encryption

One of the most popular abstraction used in security analysis uses abstract, symbolic terms to model the bitstrings sent over the network. However, the high level of abstraction blurs the significance of proofs carried out in such models with respect to real executions. In particular, although good encryption functions are randomized, most existing symbolic models for security do not capture explicitly the randomization of ciphertexts. On the other hand, recent results relating symbolic models with cryptographic models require symbolic models where the randomization of ciphertexts is captured explicitly (through the use of labels attached to symbolic ciphertexts). Since little to no tool support exists for the resulting label-based models it may seem necessary to extend the decision procedures and the implementation of existing tools from the simpler models to the models that use labels. In this paper we put forth a more practical alternative. We show that for a large class of security properties (that includes rather standard formulations of secrecy and authenticity), security of protocols with respect to the simpler model implies security in the model that uses labels. Combined with the computational soundness result of~\cite{CortierW-ESOP05}, our theorem enables the translation of security results obtained in symbolic models that do not use labels to standard computational security. Based on these results, we have recently implemented an AVISPA module for verifying security properties in a standard cryptographic model.