User Tools

Site Tools


leakage-detection

Leakage Detection

Leakage detection TODO stuff from the deliverable

Types of Checks

Task Verification

Is it ever possible that a given task T contains the set of data D? Here the user chooses the participant and the data as an input.

Participant Verification

Is it ever possible that a given participant T has the set of data D?

For example, when we ask this question about data object X and Y but they are received in exclusive branches of the process execution then the answer is no. However, if they are received consecutively or together or in non-exclusive parallel branches then the analyzer should find these cases.

For example, this can be used to verify if some privacy technology is broken for a concrete party - e.g. that party has all the shares of some secret value.

Secret Sharing Violation Verification

Is it ever possible that the SSSharing is violated in the model?

We assume that secret sharing is violated if someone has enough shares to reconstruct the secret but does not have the reconstruction task (so it is not clear that they are supposed to be able to reconstruct) and they did not produce the shares (a party always has all the shares after SSSharing operation and it is not a leakage because they knew the value that is shared).

Recall that every SSsharing task has a parameter, called \textit{threshold}, which defines how many shares are needed to reconstruct the secret. Essentially a secret sharing protocol with threshold t is violated when:

  • A party P has n>=t shares of a secret and it is not either the one that creates it (it has the SSsharing task) nor the one that has to reconstruct it (it has the SSReconstruction task).
  • A party P has n>=t computed shares (i.e. output coming from different SScomputation tasks) and the conditions are the same as above (no SSsharing and no SSreconstruction task).

This verification includes SS/AddSS/FunSS* verification.

Secret Sharing Reconstructability Verification

Is reconstruction always possible?

In models with many branches it might happen that the process goes out of sync and at some point we may have a reconstruction task that receives shares that may or may not be shares of the same value. This analyzer checks if there are in fact executions of the process where this reconstruction is not possible because there exists an execution where the inputs to the reconstruction are not belonging to the same shared value.

Encryption Violation Verification

Is it ever possible that the PK/SK encryption is violated in the model?

We assume that there is a violation if some party has the decryption key and the ciphertext but is not explicitly decrypting the data in the process nor have they created the ciphertext.

Usage

Leakage detection is available from PE-BPMN view for valid PE-BPMN models.

Modeling restrictions

  • imposing gateways in each process to form single-entry-single-exit fragments (well-structured or block-structured model)
  • Use plain tasks (e.g. no sending tasks)

Examples

leakage-detection.txt · Last modified: 2020/04/01 10:37 by pullonen