Verified Indifferentiable Hashing into Elliptic Curves

Abstract : Many cryptographic systems based on elliptic curves are proven secure in the Random Oracle Model, assuming there exist probabilistic functions that map elements in some domain (e.g. bitstrings) onto uniformly and independently distributed points in a curve. When implementing such systems, and in order for the proof to carry over to the implementation, those mappings must be instantiated with concrete constructions whose behavior does not deviate significantly from random oracles. In contrast to other approaches to public-key cryptography, where candidates to instantiate random oracles have been known for some time, the first generic construction for hashing into ordinary elliptic curves indifferentiable from a random oracle was put forward only recently by Brier et al. We present a machine-checked proof of this construction. The proof is based on an extension of the CertiCrypt framework with logics and mechanized tools for reasoning about approximate forms of observational equivalence, and integrates mathematical libraries of group theory and elliptic curves.
Type de document :
Communication dans un congrès
Pierpaolo Degano and Joshua D. Guttman. Principles of Security and Trust - First International Conference, POST 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Mar 2012, Tallinn, Estonia. Springer, 7215, pp.209-228, 2012, Lecture Notes in Computer Science. 〈10.1007/978-3-642-28641-4_12〉
Liste complète des métadonnées

https://hal.inria.fr/hal-00765874
Contributeur : Benjamin Gregoire <>
Soumis le : lundi 17 décembre 2012 - 10:03:21
Dernière modification le : jeudi 11 janvier 2018 - 16:21:50
Document(s) archivé(s) le : dimanche 18 décembre 2016 - 03:00:05

Fichier

main.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, Federico Olmedo, Santiago Zanella-Béguelin. Verified Indifferentiable Hashing into Elliptic Curves. Pierpaolo Degano and Joshua D. Guttman. Principles of Security and Trust - First International Conference, POST 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Mar 2012, Tallinn, Estonia. Springer, 7215, pp.209-228, 2012, Lecture Notes in Computer Science. 〈10.1007/978-3-642-28641-4_12〉. 〈hal-00765874〉

Partager

Métriques

Consultations de la notice

268

Téléchargements de fichiers

109