Affine Refinement Types for Secure Distributed Programming
| Autor: | Michele Bugliesi, Matteo Maffei, Stefano Calzavara, Fabienne Eigner |
|---|---|
| Rok vydání: | 2015 |
| Předmět: |
Security properties
Analysis of security protocols Theoretical computer science Substructural logics Type systems Settore INF/01 - Informatica Computer science computer.internet_protocol Distributed computing Serialization Cryptographic protocol Leverage (statistics) Affine transformation Kerberos Affine logic Implementation computer Software |
| Zdroj: | ACM Transactions on Programming Languages and Systems. 37:1-66 |
| ISSN: | 1558-4593 0164-0925 |
| DOI: | 10.1145/2743018 |
| 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 article, 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 formulate of an expressive logical encoding of the authentication mechanisms underpinning distributed resource-aware authorization policies. We discuss the effectiveness of our approach on two case studies: the EPMO e-commerce protocol and the Kerberos authentication protocol. We finally devise a sound and complete type-checking algorithm, which is the key to achieving an efficient implementation of our analysis technique. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|