Formal security proofs with minimal fuss: Implicit computational complexity at work.
Information and Computation(2015)
摘要
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.
更多查看译文
关键词
Lambda-calculus,Safe recursion,Probabilistic computation,Cryptography
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络