Verifying BPEL Workflows Under Authorisation Constraints

Abstract. Business Process Execution Language (BPEL), or Web Ser-vices BPEL (WS-BPEL), is the standard for specifying workflow process definition using web services. Research on formal modelling and verifi-cation 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 Ac-cess 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 sat-isfies the security constraints