Model-based verification of data protection mechanisms in collaborative business processes

In scenarios where multiple autonomous systems collaborate to execute a business process, it is often necessary for them to exchange confidential or private data. In this setting, mechanisms need to be put in place to ensure that each participant accesses data in a way that respects confidentiality or privacy constraints. The PE-BPMN notation is an extension of the Business Process Model and Notation (BPMN), specifically designed to model collections of autonomous systems that execute collaborative processes under the safeguard of privacy-enhancing technologies. Given a PE-BPMN specification, we address the problem of verifying that the privacy-enhancing technologies captured in the specification are used correctly, and no unexpected data disclosure may happen during process execution. To this end, we formalize the semantics of PE-BPMN collaboration specifications via a translation into process algebraic models. This makes it possible to check the correct usage of different kinds of privacy-enhancing technologies—e.g. secret sharing, encryption and multi-party computation—via model checking techniques. The approach has been implemented on top of the mCRL2 toolset and integrated into the Pleak toolset for privacy-enhanced business process analysis. The proposal has been evaluated using both real and synthetic scenarios.