On Session Typing, Probabilistic Polynomial Time, and Cryptographic Experiments (Long Version)

TL;DR

This paper introduces a probabilistic session type system derived from Bounded Linear Logic, capable of modeling cryptographic experiments with polynomial time bounds, ensuring properties like subject reduction and progress.

Contribution

It extends session types with probabilistic choices and ground types, providing a novel framework for cryptographic modeling with formal guarantees.

Findings

System satisfies subject reduction and progress

Processes have polynomial time reduction bounds

Suitable for cryptographic experiment modeling

Abstract

A system of session types is introduced as induced by a Curry Howard correspondence applied to Bounded Linear Logic, and then extending the thus obtained type system with probabilistic choices and ground types. The obtained system satisfies the expected properties, like subject reduction and progress, but also unexpected ones, like a polynomial bound on the time needed to reduce processes. This makes the system suitable for modelling experiments and proofs from the so-called computational model of cryptography.