Refinement type systems have proved very effective for security policy verification in distributed authorization systems. In earlier work [12], we have proposed an extension of existing refinement typing techniques to exploit sub-structural logics and affine typing in the analy- sis of resource aware authorization, with policies predicating over access counts, usage bounds and resource consumption. In the present paper, we show that the invariants that we enforced by means of ad-hoc typing mechanisms in our initial proposal can be internalized, and expressed directly as proof obligations for the underlying ane 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.

Affine Refinement Types for Authentication and Authorization

BUGLIESI, Michele;CALZAVARA, STEFANO;
2013

Abstract

Refinement type systems have proved very effective for security policy verification in distributed authorization systems. In earlier work [12], we have proposed an extension of existing refinement typing techniques to exploit sub-structural logics and affine typing in the analy- sis of resource aware authorization, with policies predicating over access counts, usage bounds and resource consumption. In the present paper, we show that the invariants that we enforced by means of ad-hoc typing mechanisms in our initial proposal can be internalized, and expressed directly as proof obligations for the underlying ane 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.
7th International Symposium on Trustworthy Global Computing
File in questo prodotto:
File Dimensione Formato  
chp:10.1007/978-3-642-41157-1_2.pdf

non disponibili

Tipologia: Versione dell'editore
Licenza: Accesso chiuso-personale
Dimensione 268.84 kB
Formato Adobe PDF
268.84 kB Adobe PDF   Visualizza/Apri

I documenti in ARCA sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/10278/37560
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 1
  • ???jsp.display-item.citation.isi??? 0
social impact