Fibred Security Language (bibtex)
by Guido Boella, Dov Gabbay, Valerio Genovese, Leendert van der Torre
Abstract:
We study access control policies based on the says operator by introducing a logical framework called Fibred Security Language (FSL) which is able to deal with features like joint responsibility between sets of principals and to identify them by means of first-order formulas. FSL is based on a multimodal logic methodology. We first discuss the main contributions from the expressiveness point of view, we give semantics for the language both for classical and intuitionistic fragment), we then prove that in order to express well-known properties like `speaks-for or `hand-off', defined in terms of says, we do not need second-order logic (unlike previous approaches) but a decidable fragment of first-order logic suffices. We propose a model-driven study of the says axiomatization by constraining the Kripke models in order to respect desirable security properties, we study how existing access control logics can be translated into FSL and we give completeness for the logic.
Reference:
Fibred Security Language (Guido Boella, Dov Gabbay, Valerio Genovese, Leendert van der Torre), In Studia Logica, volume 92, 2009.
Bibtex Entry:
@Article{Boella2009o,
  Title                    = {Fibred Security Language},
  Author                   = {Guido Boella and Dov Gabbay and Valerio Genovese and Leendert van der Torre},
  Journal                  = {Studia Logica},
  Year                     = {2009},
  Number                   = {3},
  Pages                    = {395-436},
  Volume                   = {92},

  Abstract                 = {We study access control policies based on the says operator by introducing a logical framework called Fibred Security Language (FSL) which is able to deal with features like joint responsibility between sets of principals and to identify them by means of first-order formulas. FSL is based on a multimodal logic methodology. We first discuss the main contributions from the expressiveness point of view, we give semantics for the language both for classical and intuitionistic fragment), we then prove that in order to express well-known properties like `speaks-for or `hand-off', defined in terms of says, we do not need second-order logic (unlike previous approaches) but a decidable fragment of first-order logic suffices. We propose a model-driven study of the says axiomatization by constraining the Kripke models in order to respect desirable security properties, we study how existing access control logics can be translated into FSL and we give completeness for the logic.},
  Affiliation              = {icr,SnT},
  Bdsk-url-1               = {http://www.springerlink.com/openurl.asp?genre=article&id=doi:10.1007/s11225-009-9201-6},
  Timestamp                = {2013.07.26},
  Url                      = {http://www.springerlink.com/openurl.asp?genre=article&id=doi:10.1007/s11225-009-9201-6}
}
Powered by bibtexbrowser