| 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 |
