MORES2

MORES2 aims at the development of appropriate refinement techniques for workflow specifications. In particular, the notion of refinement to be developed has to support the refinement of the various aspects (e.g. activities, data, users) of workflows and also has to be able to translate the security properties to corresponding properties in other refinement levels. Translated security guarantees of higher abstraction levels will serve as initial building blocks for the verification of security properties on lower levels. However, we cannot expect that the notion of refinement will preserve the security guarantees in general because otherwise the arising restrictions would render such a refinement impracticable. Additionally, changing the abstraction level may also result in a refinement of the abilities of an attacker observing the workflow, which causes a change of how the required security guarantees are formulated. In MORES2 we will develop techniques to make use of security guarantees of higher abstraction levels in verifying the corresponding security properties on lower abstraction levels. We will provide a corresponding verification tool support based on existing interactive proof systems.