Explicit Randomness is not Necessary when Modeling Probabilistic Encryption 1

One of the most popular abstraction used in security analysis uses abstract, symbolic terms to model the bit strings 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 [Cortier, V. and Warinschi, B. (2005). Computationally Sound, Automated Proofs for Security Protocols. In Proc. 14th European Symposium on Programming (ESOP'05), volume 3444 of Lecture Notes in Computer Science, pages 157–171. Springer], 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.