Logical Foundations of Secure Resource Management in Protocol Implementations

Provided by: Saarixx Labs
Topic: Security
Format: PDF
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, the authors propose the first type system that statically enforces the safety of cryptographic protocol implementations with respect to authorization policies expressed in affine logic.

Find By Topic