A Petri Nets Semantics for Privacy-Aware Data Flow Diagrams

Abstract

Privacy of personal data in information systems is gaining importance rapidly. Although data flow diagrams (DFDs) are commonly used for designing information systems, they do not have appropriate elements to address privacy of personal data. Privacy-aware data flow diagrams (PA-DFDs) were introduced recently to tackle this issue. However, they lack the concrete semantics to be formally verifiable. On the other hand, Petri net is a well-known mathematical modeling language that has all the necessary supporting elements for formal verification. In this work, we present appropriate transformations for PA-DFDs to Petri nets and therefore, provide a Petri nets semantics for them. Firstly, we clearly identify different elements of PA-DFDs. Then, we take a modular approach where for each element of PA-DFDs we present an algorithm which transforms that element to a Petri nets representation. Secondly, we demonstrate the effectiveness of the transformations on a case study, where we transform a PA-DFD to a corresponding Petri nets model. The case study is quite elaborate and covers most of the important aspects of PA-DFDs. Finally, we perform verification tasks on the obtained Petri nets model from the case study where we check privacy properties such as purpose limitation and accountability of the data controller. The Petri nets semantics along with the rest of the supporting work constitute a step forward when it comes to privacy of personal data in an information system.