Logical Foundations of Secure Resource Management in Protocol Implementations
| Autor: | Fabienne Eigner, Matteo Maffei, Stefano Calzavara, Michele Bugliesi |
|---|---|
| Rok vydání: | 2013 |
| Předmět: |
Authentication
Theoretical computer science Settore INF/01 - Informatica Computer science Programming language Serialization Authorization Cryptographic protocol computer.software_genre Linear logic Automated theorem proving Leverage (statistics) Affine transformation Affine logic Replay attack computer |
| Zdroj: | Lecture Notes in Computer Science ISBN: 9783642368295 POST |
| DOI: | 10.1007/978-3-642-36830-1_6 |
| Popis: | Recent research has shown that it is possible to leverage general-purpose theorem proving techniques to develop powerful type systems for the verification of a wide range of security properties on application code. Although successful in many respects, these type systems fall short of capturing resource-conscious properties that are crucial in large classes of modern distributed applications. In this paper, we propose the first type system that statically enforces the safety of cryptographic protocol implementations with respect to authorization policies expressed in affine logic. Our type system draws on a novel notion of "exponential serialization" of affine formulas, a general technique to protect affine formulas from the effect of duplication. This technique allows to formulate an expressive logical encoding of the authentication mechanisms underpinning distributed resource-aware authorization policies. We further devise a sound and complete type checking algorithm. We discuss the effectiveness of our approach on a case study from the world of e-commerce protocols. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|