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.
| Identifer | oai:union.ndltd.org:unibo.it/oai:amsdottorato.cib.unibo.it:7389 |
| Date | 12 May 2016 |
| Creators | Cappai, Alberto <1988> |
| Contributors | Dal Lago, Ugo |
| Publisher | Alma Mater Studiorum - Università di Bologna |
| Source Sets | Università di Bologna |
| Language | English |
| Detected Language | English |
| Type | Doctoral Thesis, PeerReviewed |
| Format | application/pdf |
| Rights | info:eu-repo/semantics/openAccess |
Page generated in 0.0025 seconds