Affine Refinement Types for Authentication and Authorization

Provided by: Saarixx Labs
Topic: Security
Format: PDF
Refinement type systems have proved very effective for security policy verification in distributed authorization systems. In earlier work, the authors have proposed an extension of existing refinement typing techniques to exploit sub-structural logics and affine typing in the analysis of resource aware authorization, with policies predicating over access counts, usage bounds and resource consumption. In this paper, they show that the invariants that they enforced by means of ad-hoc typing mechanisms in their initial proposal can be internalized, and expressed directly as proof obligations for the underlying affine logical system. The new characterization leads to a more general, modular design of the system, and is effective in the analysis of interesting classes of authentication protocols and authorization systems.

Find By Topic