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

2022/07/07 by Ugo Dal Lago, Lago, Ugo Dal, Giulia Giusti +1
Computer Science · #Cryptography and Security (cs.CR) #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #cs.CR #cs.LO

paper · pdf · doi:10.48550/arxiv.2207.03360

arxiv created 2022/07/07 · arxiv updated 2022/07/08

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.

Related

• On Computational Indistinguishability and Logical Relations
• Soft Session Types (Long Version)
• On Higher-Order Cryptography (Long Version)
• On Equivalences, Metrics, and Polynomial Time (Long Version)
• An Higher-Order Characterization of Probabilistic Polynomial Time (Long Version)