Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Parametric Iteration in Resource Theories

Alessandro Di Giorgio, Pawel Sobocinski, Niels Voorneveld

TL;DR

This work develops a parametric-iteration framework for resource theories, enabling completely parametric cryptographic reasoning within a diagrammatic, compositional setting. It defines free and parametric iteration constructions, proves that the parametric construction forms a symmetric monoidal category with a stable endofunctor, and introduces asymptotic equivalence to model negligibility. By instantiating the framework in the Markov category of Boolean stochastic maps and equipping it with a metric (total variation), the authors establish a sound and complete quantitative reasoning system and demonstrate key results such as the negligibility of guessing a random key and the feasibility of iterated von Neumann tricks. The approach offers a structured, parameter-aware path to cryptographic proofs that scale with security parameters and supports future extensions to broader primitives and notions of equivalence.

Abstract

Many algorithms are specified with respect to a fixed but unspecified parameter. Examples of this are especially common in cryptography, where protocols often feature a security parameter such as the bit length of a secret key. Our aim is to capture this phenomenon in a more abstract setting. We focus on resource theories -- general calculi of processes with a string diagrammatic syntax -- introducing a general parametric iteration construction. By instantiating this construction within the Markov category of probabilistic Boolean circuits and equipping it with a suitable metric, we are able to capture the notion of negligibility via asymptotic equivalence, in a compositional way. This allows us to use diagrammatic reasoning to prove simple cryptographic theorems -- for instance, proving that guessing a randomly generated key has negligible success.

Parametric Iteration in Resource Theories

TL;DR

This work develops a parametric-iteration framework for resource theories, enabling completely parametric cryptographic reasoning within a diagrammatic, compositional setting. It defines free and parametric iteration constructions, proves that the parametric construction forms a symmetric monoidal category with a stable endofunctor, and introduces asymptotic equivalence to model negligibility. By instantiating the framework in the Markov category of Boolean stochastic maps and equipping it with a metric (total variation), the authors establish a sound and complete quantitative reasoning system and demonstrate key results such as the negligibility of guessing a random key and the feasibility of iterated von Neumann tricks. The approach offers a structured, parameter-aware path to cryptographic proofs that scale with security parameters and supports future extensions to broader primitives and notions of equivalence.

Abstract

Many algorithms are specified with respect to a fixed but unspecified parameter. Examples of this are especially common in cryptography, where protocols often feature a security parameter such as the bit length of a secret key. Our aim is to capture this phenomenon in a more abstract setting. We focus on resource theories -- general calculi of processes with a string diagrammatic syntax -- introducing a general parametric iteration construction. By instantiating this construction within the Markov category of probabilistic Boolean circuits and equipping it with a suitable metric, we are able to capture the notion of negligibility via asymptotic equivalence, in a compositional way. This allows us to use diagrammatic reasoning to prove simple cryptographic theorems -- for instance, proving that guessing a randomly generated key has negligible success.

Paper Structure

This paper contains 16 sections, 17 theorems, 25 equations, 4 figures.

Table of Contents

  1. Introduction
  2. Symmetric Monoidal Categories as Resource Theories
  3. Parametric Iteration
  4. Reasoning with Probabilities and Distances
  5. Quantitative Reasoning
  6. Asymptotic Equivalence
  7. Examples
  8. Conclusions and Future Work
  9. Additional Material
  10. Symmetric Monoidal Categories
  11. String Diagrams for Symmetric Monoidal Categories
  12. Appendix to Section \ref{['sec:iteration']}
  13. Appendix to Section \ref{['sec:preliminaries']}
  14. A Complete Equational Theory of Boolean Stochastic Maps
  15. Other results
  16. ...and 1 more sections

Key Result

Lemma 3

There is a functor $M : \textsf{PI}(\textsf{PI}(\mathcal{C})) \to \textsf{PI}(\mathcal{C})$ satisfying the properties above.

Figures (4)

  • Figure 1: Axioms for Markov categories (top) and probabilistic choice (bottom). Here $f \colon A \to B$, $q = 1-p$, $c = \frac{(1-a)b}{1 - ab}$ and $d = ab$.
  • Figure 2: Derived laws for Markov categories with probabilistic choice.
  • Figure 3: Axioms in term-based syntax.
  • Figure 4:

Theorems & Definitions (29)

  • Example 1
  • Definition 2
  • Definition 2
  • Lemma 3
  • Lemma 4
  • Corollary 5
  • Lemma 6: Newton's cradle
  • Example 7
  • Example 8
  • Definition 9
  • ...and 19 more