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 disclosure 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.
Automated synthesis and ranking of secure BPMN orchestrators
F Martinelli;I Matteucci;M Petrocchi;
2014
Abstract
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 disclosure 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.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
