A SMT-based methodology for monitoring of security-aware workflows

Run-time monitors are crucial to the development of security-aware workflow management systems, which are at the heart of modern e-services and need to mediate access to their resources by imposing authorisation constraints (e.g., separation of duty). In this paper, we propose a new methodology to build run-time monitors capable of ensuring the successful termination of workflows subject to authorisation constraints. The methodology is based on state-of-the-art satisfiability modulo theories techniques.