Titre :

Formal security proofs with minimal fuss: Implicit computational complexity at work

Auteur(s) :

Nowak, David [Auteur]
Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 [CRIStAL]
Extra Small Extra Safe [2XS]
Zhang, Yu [Auteur]
State Key Laboratory of Computer Science [Beijing] [LCS]

Titre de la revue :

Information and Computation

Pagination :

96-113

Éditeur :

Elsevier

Date de publication :

2015-04

ISSN :

0890-5401

Mot(s)-clé(s) en anglais :

lambda-calculus
safe recursion
probabilistic computation
cryptography

Discipline(s) HAL :

Informatique [cs]/Logique en informatique [cs.LO]
Informatique [cs]/Complexité [cs.CC]
Informatique [cs]/Cryptographie et sécurité [cs.CR]
Informatique [cs]/Langage de programmation [cs.PL]

Résumé en anglais : [en]

We show how implicit computational complexity can be used in order to increase confidence in game-based security proofs in cryptography. For this purpose we extend CSLR, a probabilistic lambda-calculus with a type system ...
Lire la suite >We show how implicit computational complexity can be used in order to increase confidence in game-based security proofs in cryptography. For this purpose we extend CSLR, a probabilistic lambda-calculus with a type system that guarantees the existence of a probabilistic polynomial-time bound on computations. This allows us to define cryptographic constructions, feasible adversaries, security notions, computational assumptions, game transformations, and game-based security proofs in a unified framework. We also show that the standard practice of cryptographers, ignoring that polynomial-time Turing machines cannot generate all uniform distributions, is actually sound. We illustrate our calculus on cryptographic constructions for public-key encryption and pseudorandom bit generation.Lire moins >

Langue :

Anglais

Vulgarisation :

Non

Collections :

• Centre de Recherche en Informatique, Signal et Automatique de Lille (CRIStAL) - UMR 9189

Source :

Harvested from HAL