Skip to Main content Skip to Navigation
Conference papers

Formal Indistinguishability Extended to the Random Oracle Model

Cristian Ene 1 Yassine Lakhnech 1 van Chan Ngo 2 
2 ESPRESSO - Synchronous programming for the trusted component-based engineering of embedded systems and mission-critical systems
IRISA - Institut de Recherche en Informatique et Systèmes Aléatoires, Inria Rennes – Bretagne Atlantique
Abstract : There are two main frameworks for analyzing cryptographic systems; the symbolic frame-work, originating from the work of Dolev and Yao, and the computational approach, growing out of the work of Goldwasser and Micali. A significant amount of effort has been made in order to link both approaches and profit from the advantages of each of them. Indeed, while the symbolic approach is more amenable to automated proof methods, the computation approach can be more realistic. Abadi and Rogaway were the first to prove a formal link between these two models. More precisely, they introduced an equivalence relation on terms and prove that equivalent terms correspond to indistinguishable distributions ensembles, when interpreted in the computational model. The work of Abadi and Rogaway has been extended to active adversaries and various cryptographic primitives. Related works. A recently emerging branch of relating symbolic and computational mod-els for passive adversaries is based on static equivalence from π-calculus, induced by an equa-tional theory. Equational theories provide a framework to specify algebraic properties of the underlying signature, and hence, symbolic computations in a similar way as for abstract data types. That is, for a fixed equational theory, a term describes a computation in the symbolic model. Thus, an adversary can distinguish two frames (which roughly speaking are tuples of terms), if he is able to come up with two computations that yield the same result when applied to one frame, but different results when applied to the other frame. Such a pair of terms is called a test. Thus, a static equivalence relation is fully determined by the underlying equational theory, as two frames are statically equivalent, if there is no test that separates them. Baudet, Cortier and Kremer studied soundness and faithfulness of static equivalence for general equa-tional theories and used their framework to prove soundness of exclusive or as well as certain symmetric encryptions.
Document type :
Conference papers
Complete list of metadata
Contributor : Van Chan Ngo Connect in order to contact the contributor
Submitted on : Tuesday, November 25, 2014 - 10:18:45 AM
Last modification on : Friday, February 4, 2022 - 3:32:55 AM
Long-term archiving on: : Thursday, February 26, 2015 - 10:56:54 AM


Files produced by the author(s)



Cristian Ene, Yassine Lakhnech, van Chan Ngo. Formal Indistinguishability Extended to the Random Oracle Model. Workshop on Formal and Computational Cryptography FCC 2009, Jul 2009, New York, United States. pp.7 - 8, ⟨10.1007/978-3-642-04444-1_34⟩. ⟨hal-01086869⟩



Record views


Files downloads