R. Janvier, Y. Lakhnech et L. Mazare
Completing the Picture: Soundness of Formal Encryption in the Presence of Active Adversaries (2004)
Completing the Picture: Soundness of Formal Encryption in the Presence of Active Adversaries (2004)
TR-2004-19.pdf
TR-2004-19.ps
Keywords: Security, cryptographic protocols, formal model, Dolev-Yao, Computational model, IND-CCA
Abstract: Starting from the work of Abadi and Rogaway, there has been a growing interest in joining the two yet separated approaches of cryptographic properties: the formal and the computational views. As these two domains seem quite mature now, the gap between them is believed to be smaller than expected. Abadi and Rogaway studied in their seminal work the distinguishability of messages in the formal and computational models. They only considered passive intruders. Later Micciancio and Warinschi considered an active intruder and developed sufficient conditions to guarantee that the formal model is a safe abstraction of the computational, that is, positive verification results obtained in the formal model hold for the computational as well. Although, Micciancio and Warinschi's work is important from a conceptual point of vue, the conditions that are imposed are too severe and exclude almost all practical cryptographic protocols (except maybe the Needham-Schroeder protocol). In this paper, we present practical conditions that guarantee safety of the formal model. Indeed, almost all cryptographic protocol from the Clarke and Jacob collection satisfy our conditions. To obtain this result, we introduce a precise definition for security criteria which leads to a nice reduction theorem. The reduction theorem is of interest on its own as it seems to be a powerful tool for proving equivalences between security criteria. Also, the proof of this theorem uses original ideas that seem to be applicable in other situations.
