On Equivalences, Metrics, and Polynomial Time (Long Version)

TL;DR

This paper explores how to adapt notions of equivalence and metrics from cryptography to a probabilistic lambda calculus, providing a new proof methodology for computational indistinguishability.

Contribution

It introduces a characterization of context equivalence and metrics via traces in linear contexts within a probabilistic lambda calculus, linking it to cryptographic indistinguishability.

Findings

Context equivalence and metrics can be characterized by traces in linear contexts.

This characterization provides a new proof methodology for cryptographic indistinguishability.

The approach suggests potential extensions with more general context notions.

Abstract

Interactive behaviors are ubiquitous in modern cryptography, but are also present in $\lambda$-calculi, in the form of higher-order constructions. Traditionally, however, typed $\lambda$-calculi simply do not fit well into cryptography, being both deterministic and too powerful as for the complexity of functions they can express. We study interaction in a $\lambda$-calculus for probabilistic polynomial time computable functions. In particular, we show how notions of context equivalence and context metric can both be characterized by way of traces when defined on linear contexts. We then give evidence on how this can be turned into a proof methodology for computational indistinguishability, a key notion in modern cryptography. We also hint at what happens if a more general notion of a context is used.