Presenter
Martin Farkas
BME, Budapest
Authors
Martin Farkas, Dr. Imre Kocsis
Abstract
A BPMN collaboration is a model of a business process performed by several organizations. Traditional verification of such models tends to focus on traces in which every participant plays by the rules laid out by the standard BPMN semantics. Our goal is to extend the analysis to scenarios where adversaries also participate. A dishonest procurement coordinator, for instance, may decide to award a contract to two different suppliers simultaneously instead of one, to hedge its own supply chain risk. Standard semantics rule out this trace, so existing verification tooling does not even look for it. On a platform that merely authenticates messages this scheme is executable. This gap is not specific to BPMN. Whatever a checker proves about a multi-party model holds only for runs in which every party keeps to the model.
In this tutorial, we reason about those traces with Tamarin, a prover used to verify security protocols. The BPMN process is encoded as a Tamarin theory through the correspondence between place/transition nets, the usual semantics of BPMN, and multiset rewriting, the language of Tamarin. In that encoding, a dishonest participant is a rewriting rule set that may emit any message the platform accepts, not just the ones allowed by the process. The model has two layers: the process, and the platform that carries the messages between participants. Swapping either layer lets us test one process over a range of orchestration platforms, and one platform against many processes. The takeaways are the prover, its Petri-net reading, and a question worth asking of any multi-party model: what does its verification results quantify over, and where could it be broken? A 20-minute take-home exercise with a Docker image has attendees write one platform layer themselves, predict which of the collaboration's security properties survive, then run the prover. No prior exposure to Tamarin or BPMN is assumed.
Slides
TBA