Universität Bremen  
  FB 3  
  Group BKB > Publications > Search > Deutsch

Publications Search - Details

Publication type: Article in Proceedings
Author: M. Drouineaud, M. Bortin, P. Torrini, K. Sohr
Editor: H.-D. Ehrich, K.-D. Schewe
Title: A First Step towards Formal Verification of Security Policy Properties of RBAC
Book / Collection title: Procceedings of the Fourth International Conference on Quality Software
Series: IEEE
Year published: 2004
Abstract: Considering the current expansion of IT-infrastructure the security of the data inside this infrastructure becomes increasingly important. Therefore assuring certain security properties of IT-systems by formal methods is desirable. So far in security formal methods have mostly been used to prove properties of security protocols. However, access control is an indispensable part of security inside a given IT-system, which has not yet been sufficiently examined using formal methods. The paper presents an example of a RBAC security policy having the dual control property. This is proved in a first-order linear temporal logic (LTL) that has been embedded in the theorem prover Isabelle/HOL by the authors. Thus the correctness of the proof is assured by Isabelle/HOL. The authors consider first-order LTL a good formalism for expressing RBAC authorisation constraints and deriving properties from given RBAC security policies. Furthermore it might also be applied to safety-related issues in a similar manner.
PostScript Version: http://www.informatik.uni-bremen.de/~sohr/45_sohr_k.ps
Status: Reviewed
Last updated: 19. 10. 2004

 Back to result list
Author: Automatically generated page
  Group BKB 
Last updated: February 23, 2006   impressum