On Computational Indistinguishability and Logical Relations

TL;DR

This paper introduces a probabilistic lambda-calculus capable of modeling cryptographic protocols and adversaries, establishing a logical framework for reasoning about computational indistinguishability and providing a novel proof technique for cryptographic security.

Contribution

It presents a new lambda-calculus with polynomial-time evaluation, defines observational equivalence for cryptographic indistinguishability, and develops approximate logical relations as a sound proof method.

Findings

Logical relations effectively characterize computational indistinguishability.

The framework supports formal security proofs for cryptographic schemes.

An example proof demonstrates security of a pseudorandom function-based encryption scheme.

Abstract

A $\lambda$-calculus is introduced in which all programs can be evaluated in probabilistic polynomial time and in which there is sufficient structure to represent sequential cryptographic constructions and adversaries for them, even when the latter are oracle-based. A notion of observational equivalence capturing computational indistinguishability and a class of approximate logical relations are then presented, showing that the latter represent a sound proof technique for the former. The work concludes with the presentation of an example of a security proof in which the encryption scheme induced by a pseudorandom function is proven secure against active adversaries in a purely equational style.