Xiangpeng Zhao, Antonio Cerone and Paddy Krishnan

Verifying BPEL Workflows under Authorisation Constraints

Keywords:

workflow, BPEL, RBAC, model-checking

Abstract:

Business Process Execution Language (BPEL), or Web Services BPEL (WS-BPEL), is the standard for specifying workflow process definition using web services. Research on formal modelling and verification of BPEL has largely concentrated on control flow and data flow, while security related properties have received little attention. In this work, we present a formal framework that integrates Role Based Access Control (RBAC) into BPEL and allows us to express authorisation constraints using temporal logic. Using this framework, we show how model-checking can be applied to verify that a given BPEL process satisfies the security constraints.

Download:

Version Published by Springer:

• PDF - Access Restricted UNU-IIST Academics and Authorised Users
• PDF - Internal Access from UNU-IIST LAN: ~antonio/unuiist/share/papers/ZCK-final.pdf