Resource-Aware Authorization Policies for Statically Typed Cryptographic Protocols

Type systems for authorization are a popular device for the specification and verification of security properties in cryptographic applications. Though promising, existing frameworks exhibit limited expressive power, as the underlying specification languages fail to account for powerful notions of authorization based on access counts, usage bounds, and mechanisms of resource consumption, which instead characterize most of the modern online services and applications. We present a new type system that features a novel combination of affine logic, refinement types, and types for cryptography, to support the verification of resource-aware security policies. The type system allows us to analyze a number of cryptographic protocol patterns and security properties, which are out of reach for existing verification frameworks based on static analysis.