Programming Language Techniques for Cryptographic Proofs

Abstract : Certicrypt is a general framework to certify the security of cryptographic primitives in the Coq proof assistant. Certicrypt adopts the code-based paradigm, in which the statement of security, and the hypotheses under which it is proved, are expressed using probabilistic programs. It provides a set of programming language tools (observational equivalence, relational Hoare logic, semantics-preserving program transformations) to assist in constructing proofs. Earlier publications of Certicrypt provide an overview of its architecture and main components, and describe its application to signature and encryption schemes. This paper describes programming language techniques that arise specifically in cryptographic proofs. The techniques have been developed to complete a formal proof of IND-CCA security of the OAEP padding scheme. In this paper, we illustrate their usefulness for showing the PRP/PRF Switching Lemma, a fundamental cryptographic result that bounds the probability of an adversary to distinguish a family of pseudorandom functions from a family of pseudorandom permutations.
Type de document :
Communication dans un congrès
Matt Kaufmann and Lawrence C. Paulson. ITP'10, 2010, Edinburgh, United Kingdom. Springer, 6172, pp.115-130, 2010, Lecture Notes in Computer Science. 〈10.1007/978-3-642-14052-5_10〉
Liste complète des métadonnées

Littérature citée [11 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00552894
Contributeur : Benjamin Gregoire <>
Soumis le : lundi 10 janvier 2011 - 10:10:40
Dernière modification le : jeudi 11 janvier 2018 - 16:45:01
Document(s) archivé(s) le : lundi 11 avril 2011 - 02:47:50

Fichier

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

Identifiants

Collections

Citation

Gilles Barthe, Benjamin Grégoire, Santiago Zanella-Béguelin. Programming Language Techniques for Cryptographic Proofs. Matt Kaufmann and Lawrence C. Paulson. ITP'10, 2010, Edinburgh, United Kingdom. Springer, 6172, pp.115-130, 2010, Lecture Notes in Computer Science. 〈10.1007/978-3-642-14052-5_10〉. 〈inria-00552894〉

Partager

Métriques

Consultations de la notice

288

Téléchargements de fichiers

134