Automated Synthesis and Ranking of Secure BPMN Orchestrators

We describe a formal methodology for the automatic synthesis of a secure orchestrator for a set of BPMN processes. The synthesized orchestrator is able to guarantee that all the processes that are started reach their end, and the resulting orchestrator process is secure, that is, it does not allow discloure of certain secret messages. In this work we present an implementation of a forth and back translation from BPMN to crypto-CCS, in such a way to exploit the PaMoChSA tool for synthesizing orchestrators. Furthermore, we study the problem of ranking orchestrators based on quantitative valuations of a process, and on the temporal evolution of such valuations and their security, as a function of the knowledge of the attacker.