FB3

ForRBAC

Due to the fact that more and more data are stored on IT-systems and security-critical business processes such as banking workflows are mapped to their digital pendants, a systematic method for role-based authorisation is required. Specifically, in organisations such as hospitals, financial institutes, or government agencies role-based security policies must be established. Owing to the fact that the security policies can be quite complex in large organisations inconsistencies and unallowed access might be the consequence.

For this reason, in ForRBAC a role-based control system shall be developed which allows a security officer to

formally specify role-based security policies,
carry out a formal policy analysis, and
provide mechanisms to enforce those policies.

In the first phase of the ForRBAC project, the aforementioned control system will be developed on the basis of a temporal logic in order to deal with dynamic security policies. Dynamic security policies often occur in the context of workflows (e.g., dynamic and history-based separation of duty). The temporal logic will be embedded into the theorem prover Isabelle. This way, proofs on the security policies can be carried out automatically. However, in order to have a practical use, a security policy specification language tailored towards the needs of a security officer will be developed. This language will then be translated into the temporal calculus.

In the second phase, an authorisation engine which can enforce the aforementioned dynamic security policies shall be specified with the help of the Java Modeling Language (JML) and afterwards be implemented in Java. At least parts of this engine will be formally verified.

Period: 01/06/2006 -31/05/2008
Funding Body: DFG

Author: Dr. Karsten Sohr

Last updated: June 13, 2006