Explicit Randomness is not Necessary when Modeling Probabilistic Encryption

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 [Cortier and Warinschi, 2005], is to explicitly represent the dependency of ciphertexts on randomness 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 [Cortier and Warinschi, 2005], our theorem enables the translation of security results in unlabeled symbolic models to computational security...

• Type: Journal
• Year: 2006
• Where: CORR
• Authors: Véronique Cortier, Heinrich Hördegen, Bogdan Warinschi
• Keywords: CORR 2006, Education, Label-based Model, Security, Symbolic Models