Explicit Randomness is not Necessary when Modeling Probabilistic Encryption

Veronique Cortier, Heinrich Hoerdegen, Bogdan Warinschi

Research output: Chapter in Book/Report/Conference proceedingConference Contribution (Conference Proceeding)


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.
Translated title of the contributionExplicit Randomness is not Necessary when Modeling Probabilistic Encryption
Original languageEnglish
Title of host publicationWorkshop on Information and Computer Security -- ICS 2006
Publication statusPublished - 2006

Bibliographical note

Other page information: -
Conference Proceedings/Title of Journal: Workshop on Information and Computer Security -- ICS 2006
Other identifier: 2000657


Dive into the research topics of 'Explicit Randomness is not Necessary when Modeling Probabilistic Encryption'. Together they form a unique fingerprint.

Cite this