Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

On Computational Indistinguishability and Logical Relations

Ugo Dal Lago, Zeinab Galal, Giulia Giusti

Abstract

A $λ$-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.

On Computational Indistinguishability and Logical Relations

Abstract

A -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.
Paper Structure (21 sections, 8 theorems, 38 equations, 5 figures)

This paper contains 21 sections, 8 theorems, 38 equations, 5 figures.

Table of Contents

  1. ${\lambda}\mathbf{BLL}$: a Calculus Capturing PPT
  2. Types
  3. Terms
  4. Typing Rules
  5. Probability Distributions
  6. Combining Probability with References
  7. Operational Semantics
  8. Soundness and Completeness for Polynomial Time
  9. Soundness for PPT
  10. Completeness for PPT
  11. Computational Indistinguishability
  12. Term Relations
  13. Contextual Indistinguishability
  14. Weighted Relations
  15. Pseudo-metric Spaces
  16. ...and 6 more sections

Key Result

lemma thmcounterlemma

For a fixed reference context $\Theta$, type $A$ and security parameter $n$, the following are equivalent: for any term $M \in \Lambda_n^\Theta(A)$, store $e \in \mathrm{St}_{\Theta n}$ and distribution $\mathscr{D} \in\mathbf{D} (\mathcal{V}_n(A) \times \mathrm{St}_{\Theta n})$:

Figures (5)

  • Figure 1: Syntax of ${\lambda}\mathbf{BLL}$
  • Figure 2: ${\lambda}\mathbf{BLL}$ typing rules
  • Figure 3: Small step semantics of ${\lambda}\mathbf{BLL}$
  • Figure 4: Types for Terms in the CPA-security Proof
  • Figure 5: Outline Proof of Security

Theorems & Definitions (18)

  • lemma thmcounterlemma
  • theorem thmcountertheorem: Polytime Soundness
  • lemma thmcounterlemma
  • definition thmcounterdefinition
  • definition thmcounterdefinition
  • definition thmcounterdefinition
  • definition thmcounterdefinition
  • lemma thmcounterlemma
  • definition thmcounterdefinition
  • definition thmcounterdefinition
  • ...and 8 more