HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation

Explicit Randomness is not Necessary when Modeling Probabilistic Encryption

Véronique Cortier 1 Heinrich Hördegen 1 Bogdan Warinschi 1
1 CASSIS - Combination of approaches to the security of infinite states systems
FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174), Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : Although good encryption functions are probabilistic, most symbolic models do not capture this aspect explicitly. A typical solution, recently used to prove the soundness of such models with respect to computational ones, is to explicitly represent the dependency of ciphertexts on random coins as labels. In order to make these label-based models useful, it seems natural to try to extend the underlying decision procedures and the implementation of existing tools. In this paper we put forth a more practical alternative based on the following soundness theorem. We prove that for a large class of security properties (that includes rather standard formulations for secrecy and authenticity properties), security of protocols in the simpler model implies security in the label-based model. Combined with the soundness result of (\textbf{?}) our theorem enables the translation of security results in unlabeled symbolic models to computational security.
Document type :
Complete list of metadata

Cited literature [2 references]  Display  Hide  Download

Contributor : Rapport de Recherche Inria Connect in order to contact the contributor
Submitted on : Thursday, June 8, 2006 - 3:23:26 PM
Last modification on : Friday, January 21, 2022 - 3:09:04 AM
Long-term archiving on: : Monday, September 20, 2010 - 3:39:31 PM



Véronique Cortier, Heinrich Hördegen, Bogdan Warinschi. Explicit Randomness is not Necessary when Modeling Probabilistic Encryption. [Research Report] RR-5928, INRIA. 2006, pp.12. ⟨inria-00078825v2⟩



Record views


Files downloads