On Equivalences, Metrics, and Computational Indistinguishability

The continuous technological progress and the constant growing of information flow we observe every day, brought us an urgent need to find a way to defend our data from malicious intruders; cryptography is the field of computer science that deals with security and studies techniques to protect communications from third parties, but in the recent years there has been a crisis in proving the security of cryptographic protocols, due to the exponential increase in the complexity of modeling proofs. In this scenario we study interactions in a typed lambda-calculus properly defined to fit well into the key aspects of a cryptographic proof: interaction, complexity and probability. This calculus, RSLR, is an extension of Hofmann's SLR for probabilistic polynomial time computations and it is perfect to model cryptographic primitives and adversaries. In particular, we characterize notions of context equivalence and context metrics, when defined on linear contexts, by way of traces, making proofs easier. Furthermore we show how to use this techniqe to obtain a proof methodology for computational indistinguishability, a key notion in modern cryptography; finally we give some motivating examples of concrete cryptographic schemes.