A Multimodal view on Access Control and Trust Management: Fibred Security Language (bibtex)
by Guido Boella, Valerio Genovese, Dov Gabbay, 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. Finally we propose a model- driven study of the says axiomatization by constraining the Kripke models in order to respect desirable security properties.
Reference:
A Multimodal view on Access Control and Trust Management: Fibred Security Language (Guido Boella, Valerio Genovese, Dov Gabbay, Leendert van der Torre), In Proceedings of STM09, 2009.
Bibtex Entry:
@InProceedings{Boella2009m,
  Title                    = {A Multimodal view on Access Control and Trust Management: Fibred Security Language},
  Author                   = {Guido Boella and Valerio Genovese and Dov Gabbay and Leendert van der Torre},
  Booktitle                = {Proceedings of STM09},
  Year                     = {2009},

  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. Finally we propose a model- driven study of the says axiomatization by constraining the Kripke models in order to respect desirable security properties.},
  Affiliation              = {icr,SnT},
  Bdsk-url-1               = {http://icr.uni.lu/leonvandertorre/papers/FSL-STM.pdf},
  Timestamp                = {2013.07.26},
  Url                      = {http://icr.uni.lu/leonvandertorre/papers/FSL-STM.pdf}
}
Powered by bibtexbrowser