PE-BPMN stereotypes define various rules that need to be obeyed when adding the stereotypes to the model in order for the model to have a reasonable semantics. Some rules are stereotype specific, e.g. the number of inputs and outputs a stereotypes task needs is defined under each stereotype and it can be easily verified when adding the stereotype to the model. Other checks apply to several stereotypes at once and therefore require the general context of the process model to verify important properties. An intermediate model with only some stereotypes may not yet be complete enough to check them while adding the stereotypes. For example, OTSend and OTReceive stereotypes need to be grouped together to have a valid model, but when adding the first stereotype then we can not take the group restriction into account yet. Hence, these checks are not reasonable to do when adding the stereotypes, but they are carried out before the model is used for analysis. In the following we introduce two main model-wide checks: input-output type checking and correctly formed groups check.
Note that also for checks that do not need the model context its important to verify them before the analysis as the model may have changed after introducing the stereotypes. There are also rules to check for model structural changes and data tampering. In case a task has a stereotype that requires inputs that must be recognized as a key or a ciphertext and these inputs have been differentiated as needed, but one of these input elements is actually deleted from the model, we let the user know that one of the inputs that has previously existed is now missing. Also, the stereotype parameters that can be assigned through stereotype options must be consistent with the model. The interface does not let the user to insert incorrect values, however we also verify these requirements in the validation process in case the model has been tampered with by assigning these parameters through editing the model file directly.
The stereotypes have specific integrity constraints that should be followed for the privacy model to be syntactically correct. They require inputs and generate outputs that need to be consistent to capture the meaning of the stereotyped activity. For instance, PKEncrypt requires an input of data in plaintext and a publicKey and results in a ciphertext, encryptedData . We expect that the public key input to PKEncrypt is fixed as PKPublic . In addition, for many stereotypes we also need to verify that the input is indeed of the type claimed on the model. e.g. that an input to PKDecrypt has indeed come from PKEncrypt or PKComputation and is a ciphertext. Under each stereotype it is described the input and output types that the tasks expect and it can be used as a reference to see which sequences of stereotypes are valid on the model. The label data can apply to any data object on the model meaning that there are no restrictions on the inputs and the output is treated as having no protection mechanism. For PKDecrypt we also require that the private key (of type PKPrivate ) that is used to decrypt forms a key pair with the public key (of type PKPublic ) that was used to initially encrypt the data. For computations of PKComputation type we expect that all ciphertext inputs correspond to encryptions using the same public key and the output is then also considered to use the same key.
In short, it can be said that the protection mechanism (or protection type task) on the model limits the correct processing of the protected data and can define parameters that need to be checked in computation or opening phases. There are also conditions that need to hold for the opening stereotypes to make protected data public or for the computation stereotypes to be able to perform the computations and these are also described under each stereotype.
Stereotypes that belong to groups usually have restrictions to which tasks there need to be in a group. Groups denote computations that somehow belong together. Mostly, we group stereotypes that correspond to separate tasks of collaborative protocols. For example, MPC tasks are grouped together.
We use a different grouping semantics for Intel SGX technology where we group all tasks carried out in a single enclave. For example, tasks with SGXAttestationChallenge stereotype must come in pairs with a task with SGXAttestationEnclave stereotype, while this SGXAttestationEnclave stereotype task can also be in a group with multiple SGXComputation tasks. We expect the SGXAttestationEnclave and SGXComputation to be carried out by the same enclave if grouped together. For tasks that need to be executed in parallel we also require that they are executed by different stakeholders.
A challenge is checking the necessary parallelism of some grouped stereotypes in two cases:
We are also covering minor BPMN standard checks for some stereotypes. For example, we confirm the presence of a start event. If negative, we are unable to check parallelism (concerning reachability of tasks) in models with gateways when we have no start event to begin the check from.
Validation results are reported as a list of errors (coloured red) and warnings (coloured orange) or as a success message “Passed validation”.