arXiv CSopen access

Multiparty Session Types for GDPR Purpose Compliance

Multiparty Session Types for GDPR Purpose Compliance Evangelia Vanezi

Dimitrios Kouzapas

Anna Philippou

Department of Computer Science, University of Cyprus, Nicosia, Cyprus {vanezi.evangelia,kouzapas.dimitrios,philippou.anna}@ucy.ac.cy

The General Data Protection Regulation (GDPR) establishes purpose limitation as a fundamental constraint on personal data processing: personal data must be collected, stored, and processed strictly in accordance with explicitly specified purposes. Therefore, systems are required not only to declare the purposes under which personal data are processed, but also to ensure that their runtime behaviour remains aligned with the declared purposes. Yet, in mainstream software engineering practice, purposes are often treated as informal declarations, largely disconnected from system behaviour and, therefore, not amenable to rigorous reasoning about purpose compliance. This gap becomes particularly problematic in distributed systems, where personal data may flow across multiple entities and evolve through complex communication patterns. To address this challenge, recent works propose a more elaborate treatment of purposes based on structured, action-oriented representations of the data-processing interactions involved in their fulfilment. Building on these insights, we introduce a formal, purpose-aware framework grounded in multiparty session types in which purposes are modelled as structured interaction protocols among system entities. Within our framework, system implementations are specified using a process calculus that captures the semantics of distributed interactions and features private data as a first-class entity. Furthermore, we define a type system that verifies compliance between declared purposes and system models, and we establish subject reduction and purpose fidelity results, thereby ensuring that well-typed systems do not deviate from their specified purposes during execution. We demonstrate our approach through a case study involving a healthcare system. Ultimately, our objective is to evolve this formal framework into a softwareengineering-oriented approach that unifies purpose modelling and compliance verification within a lifecycle-driven methodology, thus enabling a practically applicable privacy-by-design process.

1

Introduction

The increasing use of software systems that store and process personal data raises major concerns about data privacy. In response, governments and legal institutions have enacted regulations such as the European Union General Data Protection Regulation (GDPR) [9]. A key concept in the GDPR and other privacy directives is purpose limitation, which requires that personal data be collected for specified and explicit purposes, and not further processed in a manner incompatible with those purposes. Therefore, systems are required to specify the processing purposes they may pursue when handling personal data. For example, in healthcare, a doctor may process a patient’s medical data for the purpose of performing a diagnosis, while the accounting department may use the patient’s address for the purpose of issuing an invoice. In contrast, repurposing the same medical records for an unrelated objective, such as marketing, would constitute a purpose incompatible with the original intent of collection and would thus be disallowed under the principle of purpose limitation. While purposes can be specified at the policy level, ensuring that the actual behaviour of a system remains aligned with the declared purposes is considerably more complex. Yet, in mainstream software engineering practice, existing approaches often treat purposes as informal declarations, e.g., as simple textual labels [27, 4], disconnected from system behaviour and lacking formal guarantees. V. de Paiva; T.A. de Lima (Eds.): 21st International Symposium on Logical and Semantic Frameworks, with Applications (LSFA 2026) EPTCS 449, 2026, pp. 259–277, doi:10.4204/EPTCS.449.16

© E. Vanezi, D. Kouzapas & A. Philippou This work is licensed under the Creative Commons Attribution License.

260

MPST for GDPR Purpose Compliance

To address this challenge, the need of providing formal semantics to the notion of purpose has been strongly advocated and, in the formal landscape, several works have adopted such semantics based on structured, action-oriented representations of the data-processing interactions involved in a purpose fulfilment [25, 29, 30, 15], Building on this perspective and informed by GDPR analysis [35], in our recent work we have defined purposes as structured interaction protocols over data [32, 33, 34]. Under this approach purposes are captured as scenarios of communication actions and interactions between system entities, that specify the patterns of exchange, storage, reading, and writing of personal data. Practical applicability in software engineering is demonstrated through purpose-aware UML sequence diagrams [32, 33], which constitute our proposed modelling notation for representing and reasoning about purposes at the design level (see Fig. 1 and relevant discussion below). The current work provides a formal foundation for this definition by modelling purposes as global types within a purpose-aware multiparty session type framework. System implementations are specified using a process calculus that captures the semantics of distributed interactions, and features private data as a first-class entity. Unlike standard uses of multiparty session types, where global types specify only communication correctness, here they additionally encode purpose constraints: they restrict not only the flow of messages, but also the flow, access, and usage of personal data, including interactions with data stores. We then define a type system that verifies compliance between declared purposes and system models and establish subject reduction and purpose fidelity results, thereby ensuring that well-typed systems do not deviate from their specified purposes during execution. An example of purpose. A representative example of purpose is a diagnostic process taking place in a medical system, where personal data are exchanged between multiple parties. In this purpose, a patient provides their data (e.g., basic information and symptoms), and requests a diagnosis. These data should only be processed and accessed according to the purposes specified in the system’s privacy policy, to initiate, execute, and fulfil the requested process. Such a process might involve additional participants, such as a nurse or a general practitioner, and operations such as reading symptoms or ordering a laboratory test, while different interactions might occur depending on intermediate decisions. In any case, every action and interaction must follow the specified purpose protocol. Furthermore, while some entities may need to process the data to perform their task, others may only relay or store information without accessing its contents.

Figure 1: Part of the diagnostic purpose illustrated via a purpose-aware sequence diagram [33]

E. Vanezi, D. Kouzapas & A. Philippou

261

Figure 1 presents part of such a diagnostic purpose via a purpose-aware sequence diagram [32, 33]. Participants, represented by lifelines, include system entities and additionally personal data repositories called stores (specified through the stereotype «store»). Such repositories belong to a specific actor (specified by the stereotype «owner»), and hold data of a specific type defined in brackets, e.g., (basicInfo). Store names (e.g., info), called references, are used to interact with them. Exchanges with such repositories signify accessing personal data. Such a diagram illustrates how personal data are intended to be exchanged between the participants, and how access to data is dictated by the defined purpose, including branching interactions which determine how additional entities are involved. The purpose illustrated above specifies that a patient first communicates their basic information via the corresponding reference (info) to a nurse practitioner, followed by writing their symptoms in the corresponding personal data repository (sympt), and forwards them to the nurse. In turn, the nurse practitioner reads both pieces of personal data from the repositories, and then decides whether a laboratory exam is needed, in which case the nurse prescribes the order in the corresponding repository (labOrder) and forwards its reference to the lab; or, if a laboratory exam is not needed, the nurse proceeds with sending the symptoms repository reference to the general practitioner to perform a diagnosis. Our aim in this paper is to formalize the approach through multiparty session types and evolve it into a framework that enables providing formal guarantees of purpose compliance. The complete case study is detailed in Section 6. Related Work. Existing approaches for reasoning about purposes in software engineering such as [7, 21, 36] describe purposes using informal or semi-formal specification with limited semantic grounding, while others represent and handle purposes through textual labels [27, 4]. Such approaches do not provide a basis for precise analysis of whether system behaviour conforms to purpose-based specification. To address this need, several formal approaches have also been proposed, approaching purposes as workflows. The work in [25] models purposes as Petri net workflows and verifies compliance against actor models using model checking. Markov Decision Processes are employed in [29, 30], while a planning-based formalism is proposed to audit systems against privacy policies. A similar approach is adopted in [6], where purposes are identified with business processes, and formal models of interprocess communication are used to derive or audit privacy policies. In [14], the authors introduce a semantic model for purpose-based privacy policies, together with a modal logic and the corresponding model-checking procedure for compliance verification. Other works like [8] define temporal logic-based semantics and run-time monitoring methodologies for the enforcement of purpose-based privacy policies. Complementing and extending these approaches, our work models purposes as structured communication protocols between interacting entities. It captures personal data flows and access patterns, and enables static verification of purpose compliance at design time through a type system grounded in multiparty session types. Additionally, the practical application of our approach in software engineering practice is direct, through purpose-aware UML sequence diagrams [32, 33], enabling future integration into a lifecycle-driven methodology. Contribution. This work presents the following contributions: 1. Formal modelling of systems using a process calculus that explicitly captures personal data processing (Sect. 2); 2. Formal specification of processing purposes through a purpose-aware type language (Sect. 3); 3. Formal verification of system compliance with declared purposes via a type system (Sect. 4), supported by proofs for subject reduction and purpose fidelity (Sect. 5);

262

MPST for GDPR Purpose Compliance

4. A realistic case study, demonstrating compliant and non-compliant behaviours captured by our framework (Sect. 6). Section 7 discusses conclusions and future work. Detailed proofs, auxiliary lemmas, and typing of the case study, are presented in [31].

2

The Calculus

In this section we present a process calculus for modelling systems that process personal data. The calculus integrates (i) the notions of personal data and personal data stores [19], to capture personal data processing operations, and (ii) multiparty session types (MPST) [37], to structure interactions as communication protocols among participants. MPSTs provide a typed foundation for specifying structured communication among distributed entities, ensuring properties such as communication safety and progress. The goal of the calculus is to provide a formal model in which both communication and personal data manipulation can be explicitly represented and analysed. In particular, it enables us to model systems as workflows of message-passing actions and data-processing operations, forming the basis for reasoning about purpose compliance. In contrast to standard MPST-based calculi, our model explicitly incorporates personal data stores and controlled data access via references. Based on [19] and following the GDPR, we assume that personal data are data associated to individuals. As such, we model personal data as structures that associate constants, that is, pieces of information, with identifying pieces of information, which we simply refer to as identities. Such personal data used in an information system are typically stored within a database of the system. We capture such databases as a collection of stores, where a store is encoded as a high-level process term associated with operations for the manipulation of personal data. This manipulation takes place with the use of a special kind of names called references. In the sequel, we describe these concepts within a multi-party, synchronous, session types framework. For simplicity, we eliminate shared channels for session initiations. However, the framework can be easily extended to accommodate multiple sessions.

2.1

Syntax

Figure 2 defines the syntax of the proposed calculus. The calculus assumes the following basic structures: i) the set of session participants p, q, . . .; ii) the set of variables V , ranged over by x, y, z, . . .; iii) the set of store references R, ranged over by r, r ′ , . . .; iv) the set of constants C , ranged over by c, . . .; v) the set of identities Ids, ranged over by id, id1 , id2 , . . ., with the anonymous identity _ supporting personal data anonymisation; and vi) the set of labels L , ranged over by ℓ, ℓ1 , ℓ2 , . . . . Values include constants c and references r. Terms t include values and variables x, whereas store terms u include references and variables. Metavariable ι ranges over identities, id, and the anonymised identity _. The symbol k is a variable placeholder for personal data, ranged over by x ⊗ y and _ ⊗ x. The symbol v ranges over personal data ι ⊗ c, associating data c with an identity ι, signifying the owner of the data, and personal data variable k. Personal data of the form _ ⊗ c, denote anonymised personal data. Processes implement the behaviour of participants. Process p!⟨t⟩.P sends term t to participant p and continues as P, whereas process p?(x).P denotes receiving a value from participant p, substituting it into variable x, and continuing as P. The select process p ◁ ℓ.P selects a label ℓ on participant p and continues as P. Dually, the branch process p ▷ {ℓi : Pi }i∈I waits for the selection of one of the labels ℓi from participant p and then proceeds with the corresponding process Pi , i ∈ I. Personal data processing uses the special store references (r), which provide access to processes that store personal data. Processes

E. Vanezi, D. Kouzapas & A. Philippou

263

v

::=

c | r

(values)

t

::=

v | x

(terms)

u

::=

r | x

(store terms)

ι

::=

id | _

(identity)

k

::=

x⊗y | _⊗x

(placeholders)

d

::=

ι ⊗c | k

(data terms)

P

::=

p!⟨t⟩.P | p?(x).P | p ◁ ℓ.P | p ▷ {ℓi : Pi }i∈I

(processes)

|

u!⟨d⟩.P | u?(k).P | if a = b then P else P

|

X | µX.P | 0

::=

p ▶ [P] | r ▶ [id ⊗ c] | M | M

M

(networks)

Figure 2: Syntax of the calculus do not exchange personal data directly; instead, they exchange references. Any process with access to a store reference can use it to write data to or read data from the corresponding store. Process u!⟨d⟩.P represents storing personal data d on reference u and continuing as P. Dually, process u?(k).P denotes reading personal data via reference u and substituting the retrieved data within P before continuing. The matching construct if a = b then P else Q evolves as P if the condition a = b holds, and as Q otherwise, where a and b range over values (e.g., constants). A conditional is used to decide internal process control. When combined with subtyping, a conditional is the mechanism for performing internal choice, i.e., allowing multiple select labels. Process X ranges over recursion variables, and process µX.P is a recursive process. Finally, 0 represents an inactive process. A role network, p ▶ [P], associates a participant p with a process P. The notation r ▶ [id ⊗ c] represents a personal data store, where personal data are accessed through the references r. The syntax supports the parallel composition of networks, M1 | M2 . Example 1 (Simplified Medical Workflow Network). We illustrate the use of the calculus through a simplified fragment of the diagnostic workflow introduced in Section 1 and developed fully in Section 6. In network M1 below, a patient sends a reference (rs ) to a data store containing their symptoms (id ⊗ sympt1 ) to a nurse, who then accesses the personal data from the store and proceeds with further actions. M1 = patient ▶ [nurse!⟨rs ⟩.P] | nurse ▶ [patient?(z).z?(y ⊗ xsympt ).Q] | rs ▶ [id ⊗ sympt] A variation of the above example ensures that the personal data read by the nurse is anonymised: M2 = patient ▶ [nurse!⟨rs ⟩.P] | nurse ▶ [patient?(z).z?(_ ⊗ xsympt ).Q] | rs ▶ [id ⊗ sympt] The next network demonstrates a choice implemented via select and branch processes: M3 = nurse ▶ [practitioner ◁ lab.0] | practitioner ▶ [nurse ▷ {lab : P1 , noLab : P2 }] Network M3 demonstrates the case in which the practitioner is expecting from the nurse either the decision that laboratory exam is needed (label lab) and proceed as P1 , or the decision that no exam will take place (label noLab), in which case it will proceed as P2 . At the same time the nurse makes the choice that a lab exam is needed, by sending label lab to the practitioner.

264

2.2

MPST for GDPR Purpose Compliance

Operational Semantics

The semantics of the process calculus define substitution in two cases: (i) P{v /x }, which substitutes all free occurrences of x in P with v ; and (ii) P{ι⊗c /k }, which substitutes all free occurrences of k in P with ι ⊗ c. The definitions can be found in [31]. In particular, we note that substitution on private-data placeholders accounts for anonymous substitution: x ⊗ y{ι⊗c /x⊗y } = ι ⊗ c

_ ⊗ y{ι⊗c /_⊗y } = _ ⊗ c

z ⊗ w{ι⊗c /x⊗y } = z ⊗ w if z ̸= x or w ̸= y. Figure 3 presents the operational semantics of the process calculus, defined in terms of a structural congruence relation ≡. Structural congruence is the least relation generated by the rules in the first two lines of Figure 3. It establishes the associativity and commutativity of the parallel composition operator and treats a terminated role of the form p ▶ [0] as a neutral element.

M | p ▶ [0] ≡ M (M1 | M2 ) | M3 ≡ M1 | (M2 | M3 ) [Comm]

M1 | M2 ≡ M2 | M1   p ▶ [µX.P] | M ≡ p ▶ P{µX.P /X } | M

p ▶ [q!⟨v⟩.P1 ] | q ▶ [p?(x).P2 ] | M −→ p ▶ [P1 ] | q ▶ [P2 {v /x }] | M

[BranchSel] p ▶ [q ◁ ℓj .P] | q ▶ [p ▷ {ℓi : Pi }i∈I ] | M −→ p ▶ [P] | q ▶ [Pj ] | M j ∈ I

[SInp]

p ▶ [r!⟨ι ⊗ c⟩.P] | r ▶ [id ⊗ c′ ] | M −→ p ▶ [P] | r ▶ [id ⊗ c] | M   p ▶ [r?(k).P] | r ▶ [id ⊗ c] | M −→ p ▶ P{id⊗c /k } | r ▶ [id ⊗ c] | M

[True]

p ▶ [if a = a then P else Q] | M −→ p ▶ [P] | M

[False]

p ▶ [if a = b then P else Q] | M −→ p ▶ [Q] | M

[SOut]

[Struct]

M1 ≡ M1′

M1′ −→ M2′ M1 −→ M2

a ̸= b

M2′ ≡ M2

Figure 3: Structural Congruence and Operational Semantics Rule [Comm] describes message communication between two parallel roles. Role p sends a value v to role q, which receives it in variable x. After the interaction, the former proceeds as p ▶ [P1 ], and the latter as q ▶ [P2 {v /x }], where all free occurrences of x in P2 are substituted by x. Rule [BranchSel] describes synchronisation between two parallel roles to execute a choice interaction. Role p sends a label ℓj to role q, while role q receives the label from role p. After the interaction, the former proceeds as p ▶ [P], and the latter as q ▶ [Pj ], following label ℓj . Rule [SOut] describes a role storing a value id ⊗ c in the store corresponding to reference r. After the storing action, the store updates its data value, while the role proceeds as p ▶ [P]. Rule [SInp] describes a role reading a value id ⊗ c into variable k from the  store corresponding to reference r. After the read action, the role proceeds as p ▶ {id⊗c /k } , with k substituted by id ⊗ c. Finally, rule [Struct] defines reduction under structural equivalence. We write −→∗ for the reflexive and associative closure of relation −→.

E. Vanezi, D. Kouzapas & A. Philippou

265

Example 2 (Simplified Medical Workflow Network Transition). We demonstrate the application of the transition rules [Comm] and [SInp], to networks M1 and M2 from Example 1, as follows: M1

=

patient ▶ [nurse!⟨rs ⟩.P] | nurse ▶ [patient?(z).z?(y ⊗ xsympt ).Q] | rs ▶ [id ⊗ sympt]

−→ patient ▶ [P] | nurse ▶ [rs ?(y ⊗ xsympt ).Q] | rs ▶ [id ⊗ sympt] h i −→ patient ▶ [P] | nurse ▶ Q{id⊗sympt /y⊗xsympt } | rs ▶ [id ⊗ sympt] M2

=

patient ▶ [nurse!⟨rs ⟩.P] | nurse ▶ [patient?(z).z?(_ ⊗ xsympt ).Q] | rs ▶ [id ⊗ sympt]

−→ patient ▶ [P] | nurse ▶ [rs ?(_ ⊗ xsympt ).Q] | rs ▶ [id ⊗ sympt] h i −→ patient ▶ [P] | nurse ▶ Q{id⊗sympt /_⊗xsympt } | rs ▶ [id ⊗ sympt] Note that the substitution function ensures that in the continuation process of the nurse in M2 the patient’s data are read anonymized.

3

Defining Purposes via a Type Language

We now proceed to propose a formal type language to rigorously model purposes. The language extends multiparty session types, enabling the definition of a purpose by formalising how personal data flows among system entities in order to achieve the purpose. In particular, we represent a purpose by means of a global type, which specifies the interaction protocol that participants must follow to achieve the intended objective. Subsequently, local types serve to characterise the role-specific realisation of the purpose. The relationship between global and local types is established through projection.

3.1

Global and Local Types

Figure 4 presents the syntax of the proposed global and local types. The type system assumes a set of ground types, ranged over by g, including int and bool. Type i denotes the type of data-subject identities, whereas _ denotes the anonymous identity type. The metasymbol ti ranges over both i and _. An exchange type U ranges over either ground types g, or personal data store types of the form α[ti ⊗ g]. Personal data store types α[ti ⊗ g] are parameterised by an identity type ti and a data type, g, and are decorated with annotations, ranged over by α, β, and γ. These annotations enable reasoning about the manipulation of private data through the corresponding database stores. We assume that each data store is decorated with a static annotation α. This annotation is part of the purpose definition and is not dynamically introduced by processes. We further assume that annotations uniquely determine the type of stored data. That is, for a given annotation α, if a global type specifies two types α[ti ⊗ c1 ] and α[ti ⊗ c2 ] then c1 = c2 , Global types G define the interaction between the participants of a system. Global type p → q:⟨U⟩. G denotes the transmission of a value of type U from participant p to participant q and proceeding with global type G. Global type α → p:⟨ti ⊗ g⟩. G denotes participant p reading from a store with annotation α a value of type ti ⊗ g before proceeding with G. Global type p → α:⟨ti ⊗ g⟩. G, denotes participant p storing a value of type ti ⊗ g to personal data store annotated as α before proceeding with G. Global type p → q : {ℓi : G i }i∈I denotes participant p transmitting to participant q a label ℓi , and the protocol proceeding with the respective global type G i . Recursive protocols are modelled using µt.G. Finally, global type end denotes the end of a global type.

266

MPST for GDPR Purpose Compliance

α, β, γ, . . .

(annotations)

g

::=

int | bool | . . .

(Ground Types)

ti

::=

i | _

(Id Types)

U

::=

g | α[ti ⊗ g]

(Exchange Types)

G

::=

p → q:⟨U⟩. G

(Value Exchange)

|

α → p:⟨ti ⊗ g⟩. G

(Personal Data Read)

|

(Personal Data Storage)

|

p → α:⟨ti ⊗ g⟩. G p → q : {ℓi : G i }i∈I

(Select/Branch)

|

t | µt.G

(Recursion)

|

end

(Inact)

::=

p?U.T

(Value Input)

|

p!U.T

(Value Output)

|

α?ti ⊗ g.T

(Personal Data Value Input)

|

α!ti ⊗ g.T

(Personal Data Value Output)

|

p ⊕ {ℓi : Ti }i∈I

(Selection)

|

p&{ℓi : Ti }i∈I

(Branching)

|

t | µt.T

(Recursion)

|

end

(Inact)

T

Figure 4: Global and Local Types Example 3 (Simplified Medical Workflow Purpose). The following global types capture the purposes corresponding to the networks defined in Example 1: G 1 = patient → nurse:⟨α[i ⊗ sympt]⟩. α → nurse:⟨i ⊗ sympt⟩. T

(1)

G 2 = patient → nurse:⟨α[i ⊗ sympt]⟩. α → nurse:⟨_ ⊗ sympt⟩. T

(2)

Global type G 1 specifies that participant nurse accesses personal data of type i ⊗ sympt from a store decorated with annotation α, after receiving such store reference type from patient. Similarly, global type G 2 describes an anonymous personal data access. Local types, denoted by T , define communication interactions from the perspective of a single participant. Local type p?U. T denotes an input of a value of type U from participant p. Local type p!U. T denotes an output of a value of type U, towards participant p. Local type α?ti ⊗ g. T denotes the input of a personal data value of type ti ⊗ g from a personal data store annotated with α. Dually, local type α!ti ⊗ g. T denotes the storing of a personal data value of type ti ⊗ g to a personal data store annotated with α. The select local type p ⊕ {ℓ i :Ti }i∈I denotes the selection of a label ℓ i from the offered set and its transmission to participant p, before proceeding with type Ti . Dually the branch local type p&{ℓ i :Ti }i∈I , denotes the input of a label ℓi from participant p and proceeding according to type Ti . Recursion is

E. Vanezi, D. Kouzapas & A. Philippou

267

modelled by the local type µt.T, assuming equi-recursive type variable substitution, µt.T = T{µt.T /t }. Finally, local type end denotes the end of the local type.

3.2

Local Projection of Global Types

In this work we adopt the projection and merging operators from [11], extended to handle the newlyintroduced data-flow constructs: Definition 1. The projection of a global type G onto a participant q, denoted as G⌉q, is a partial relation defined as follows, where pts(G) denotes the set of participants of G:  ′   p !U.G⌉q ′ (p → p :⟨U⟩. G)⌉q = p?U.G⌉q   G⌉q ( α?ti ⊗ g.G⌉q (α → p:⟨ti ⊗ g⟩. G)⌉q = G⌉q ( α!ti ⊗ g.G⌉q (p → α:⟨ti ⊗ g⟩. G)⌉q = G⌉q  ′   p ⊕ {ℓ i : Gi ⌉q}i∈I (p → p′ : {ℓi : G i }i∈I ⌉)q = p&{ℓ i : Gi ⌉q}i∈I   ⊓i∈I (G i ⌉q)

if q = p, if q = p′ , otherwise if q = p otherwise if q = p otherwise if q = p if q = p′ otherwise

end⌉q = end Above, ⊓ is a partial merging operator on local types, defined as follows: ( T1 ⊓ T2 =

T1

if T1 = T2 ,

T3

if T1 = p&{ℓ i : Ti }i∈I , T2 = p&{ℓ j : T j } j∈J and T3 = p&{ℓ k : Tk }k∈I∪J ,

Projection allows a participant to observe different actions in different branches of a choice even if that participant is not itself involved in the choice. This is essential for realistic workflows in which different branches involve different participants. For example, in the case study presented in Section 6, in a healthcare setting a laboratory may be involved only when a lab test is required, while in alternative branches, it does not participate at all. Example 4 (Simplified Medical Workflow Projection). As an example, projecting on nurse the global type defined in Example 3, yields the following local type: G 1 ⌉nurse = patient?α[ti ⊗ sympt].α?i ⊗ sympt.G 1 ⌉nurse The nurse is receiving a store reference α from the patient and proceeds with reading the symptoms.

268

3.3

MPST for GDPR Purpose Compliance

Subtyping

Subtyping, denoted by ⩽, is the largest relation between session types coinductively defined by the rules in Figure 5, adapted from [11]. The subtyping relation preserves the usual safe substitutability principles for session types. The relation is defined over value types, private data types, and local session types. Base types, such as int and bool, are subtypes only of themselves, as specified by rules [SubInt] and [SubBool]. Private-data types ti ⊗ g are covariant in the ground type g of the stored value. Rule [SubEnd] states that the inactive local type end admits only reflexive subtyping, i.e., it is a subtype only of itself. Rule [SubOut] defines output local types as covariant both in the communicated type, U ⩽ U′ , and in the continuation type, T ⩽ T ′ . Conversely, rule [SubInp] defines input local types as contravariant in the communicated type, U′ ⩽ U, and covariant in the continuation type, T ⩽ T ′ . Rules [SubPDOut] and [SubPDInp] extend the same principles to private-data communication. Privatedata output is covariant in the private-data payload and in the continuation. Private-data input is contravariant in the private-data payload and covariant in the continuation. Rule [SubSel] states that selection types are covariant and admit width subtyping on the right: a selection offering fewer labels may be used where a larger selection type is expected. Dually, rule [SubBranch] states that a branch type accepting more labels may be used where a branch type accepting fewer labels is expected.

[SubInt] int ⩽ int

[SubEnd] end ⩽ end

[SubBool] bool ⩽ bool U ⩽ U′ T ⩽ T ′ [SubOut] ============== p!U.T ⩽ p!U ′ .T ′

ti ⊗ g ⩽ ti ′ ⊗ g′

T ⩽ T′

[SubPDOut] ======================

α!ti ⊗ g.T ⩽ α!ti ′ ⊗ g′ .T ′

I⊆J

∀i ∈ I.Ti ⩽ Ti′

[SubSel] =============================

p ⊕ {ℓi : Ti }i∈I ⩽ p ⊕ {ℓj : T j′ } j∈J

g ⩽ g′ [SubPD] ============ ti ⊗ g ⩽ ti ⊗ g′ U′ ⩽ U T ⩽ T ′ [SubInp] =============== p?U.T ⩽ p?U ′ .T ′ ti ′ ⊗ g′ ⩽ ti ⊗ g

T ⩽ T′

[SubPDInp] =======================

α?ti ⊗ g.T ⩽ α?ti ′ ⊗ g′ .T ′ J⊆I

∀ j ∈ J.T j ⩽ T j′

[SubBranch] ============================

p&{ℓi : Ti }i∈I ⩽ p&{ℓj : T j′ } j∈J

Figure 5: The subtyping relation

4

Type Checking Purpose Compliance

In this section, we present the type system of our calculus, which verifies whether a system implementation conforms to a declared purpose expressed as a global type via a set of rules for checking whether a process or a network uses names and variables according to their types and follows the prescribed protocol associated with the purpose. The typing rules use typing environment Γ, which associates references u to personal data types of the form α[ti ⊗ g], variables to ground types g, placeholders k to personal data types ti ⊗ g, and recursion variables to local types T.

E. Vanezi, D. Kouzapas & A. Philippou

269

Γ ::= 0/ | Γ, u : α[ti ⊗ g] | Γ, x : g | Γ, k : ti ⊗ g | Γ, X : T Figure 6 defines the rules of the type system. The first two lines specify the rules for asserting the types of store references, personal data variables, recursion variables, and value variables. The next five lines define the typing rules for processes. Each rule has the form Γ ⊢ P: T, meaning that under environment Γ process P has type T. The last line defines the typing rule for networks.

[TData] Γ ⊢ c : g

[TVd] Γ ⊢ id : i

[TPlc] Γ, k : ti ⊗ g ⊢ k : ti ⊗ g [TInact]Γ ⊢ 0 : end

[TInpPD] [TBranch]

[TVRec] Γ, X : T ⊢ X : T [TOut]

[TOutPD]

[THd] Γ ⊢ _ : _

Γ ⊢ t : U Γ ⊢ P: T Γ ⊢ p!⟨t⟩.P: p!U.T

∀i ∈ I, Γ ⊢ Pi : Ti Γ ⊢ p ▷ {ℓi :Pi }i∈I : p&{ℓi :Ti }i∈I

[TInp]

Γ, X : T ⊢ P: T Γ ⊢ µX.P : T

[TSel]

[TIf ] [TSub]

∀i ∈ I, Γ ⊢ Pi : G⌉pi [TNet]

[TPd] Γ, u : α[ti ⊗ g] ⊢ u : α[ti ⊗ g] Γ, x : U ⊢ P: T Γ ⊢ p?(x).P: p?U.T

Γ ⊢ u : α[i ⊗ g] Γ ⊢ ι : ti Γ ⊢ c : g Γ ⊢ P: T Γ ⊢ u!⟨ι ⊗ c⟩.P: α!ti ⊗ g.T

Γ ⊢ u : α[i ⊗ g] Γ, k : ti ⊗ g ⊢ P: T Γ ⊢ u?(k).P: α?ti ⊗ g.T

[TRec]

[TVar] Γ, x : g ⊢ x : g

Γ ⊢ P: T Γ ⊢ p ◁ ℓ.P: p ⊕ {ℓ:T }

Γ ⊢ P1 : T Γ ⊢ P2 : T Γ ⊢ if a = b then P1 else P2 : T

Γ ⊢ P: T T ⩽ T′ Γ ⊢ P: T ′

pts(G) ⊆ {pi }i∈I

∀ j ∈ J, Γ ⊢ rj : αj [i ⊗ g j ] ∧ Γ ⊢ c j : g j rj : αj [i ⊗ g j ] ∈ Γ =⇒ j ∈ J Γ ⊢ ∏i∈I pi ▶ [Pi ] | ∏ j∈J rj ▶ [i ⊗ c j ] : G

Figure 6: Typing rules for Constants, References, Variables, Private data, Processes, and Network Starting with the rules for typing constants, references, and variables: Rule [TData] assigns a constant c to a ground type g, based on the type of the constant (e.g., integer, boolean). Similarly, rules [TVd] and [THd] assign the types i and _ to non-anonymous identities and the anonymous identity, respectively. Rule [TVar] types variables with ground types, according to Γ. Subsequently, rules [TPlc], [TVRec], and [TPd] type personal data variables k, recursion variables X, and store terms u according to Γ. Moving on to processes, typing rule [TInact] types the inactive process with local type end. Typing rule [TOut] types processes that send a value of type U to participant p with local type p!U.T, where T is the type of the continuation process. Respectively, typing rule [TInp] types processes that read a value of type U from participant p with local type p?U.T. Typing rule [TOutPD] types a process that writes a personal data value of type ti ⊗ g to a store via a reference of type α[i ⊗ g], with type α!ti ⊗ g.T. Similarly, typing rule [TInpPD] types a process that inputs a value of type ti ⊗ g via a store reference of type α[i ⊗ g], with local type α?ti ⊗ g.T. In both cases, T is the type of the continuation processes. Furthermore, the use of i and ti , in the value and store types of the rule, accounts to the fact that data

270

MPST for GDPR Purpose Compliance

manipulation may be anonymized. Typing rule [TSel] types a process that sends a label ℓ to participant p with local type p ⊕ {ℓ:T }. Typing rule [TBranch] types a process that receives and matches a label from a choice of labels ℓi , i ∈ I, from participant p, with local type p&{ℓi : Ti }i∈I . Finally, rule [TSub] captures subsumption: if P is well-typed with type T and T is a subtype of T ′ , then P is also well-typed with type T ′. Moving to the typing rule for networks, typing rule [TNet] types a network to a global type G assuming that the participant processes composed in parallel are well-typed according to their local type projection of G, all store processes in the network are well-typed according to Γ, and all stores in Γ are present in the network. Moreover, the requirement that pts(G) ⊆ {pi }i∈I , allows to type networks with participants of the form p ▶ [0], thus ensuring that typing remains invariant under structural congruence.

5

Subject Reduction and Purpose Fidelity

We establish subject reduction and purpose fidelity for our framework. We first present the Subject reduction Theorem (Theorem 1), stating that the execution of a typed network, according to the operational semantics, preserves the overall typing of the network. Moreover, the Purpose Fidelity Theorem (Theorem 2) states that the communication sequence of a process follows the purpose declared. In order to state the Subject Reduction Theorem we need to define how global types are modified during the evolution of networks. Definition 2 (Global type consumption and reduction). The consumption of an action act in a global type G (notation G \ act) is defined co-inductively as follows. ℓ

U

k act ::= p → q | p → q

|

t ⊗g

t ⊗g

i i α → p | p → α

U

p → q:⟨U⟩. G \ p → q = G

ℓ

k q = Gk k ∈ I p → q : {ℓi : G i }i∈I \ p →

t ⊗g

i α → p:⟨ti ⊗ g⟩. G \ α → p=G

t ⊗g

i p → α:⟨ti ⊗ g⟩. G \ p → α=G

U

ℓ

t ⊗g

t ⊗g

k pts(p → q) = pts(p → q) = {p, q} i i pts(α → p) = pts(p → α) = {p, α}

G \ act = G ′ {p1 , q1 } ∩ pts(act) = 0/ ===================================== p1 → q1 :⟨U1 ⟩. G \ act = p1 → q1 :⟨U1 ⟩. G ′ ∀i ∈ I, G i \ act = G ′i {p1 , q1 } ∩ pts(act) = 0/ ==================================== ========= p1 → q1 : {ℓi : G i }i∈I \ act = p1 → q1 : ℓi : G ′i i∈I G \ act = G ′ {α, p} ∩ pts(act) = 0/ ======================================= α → p:⟨ti ⊗ g⟩. G \ act = α → p:⟨ti ⊗ g⟩. G ′ G \ act = G ′ {p, α} ∩ pts(act) = 0/ ======================================= p → α:⟨ti ⊗ g⟩. G \ act = p → α:⟨ti ⊗ g⟩. G ′

Assume a global type G. The reduction of G is defined co-inductively as the smallest pre-order relation closed under the rule G −→ G ′ , where G \ act = G ′ for some G ′ and act. Theorem 1 (Subject Reduction). Assume a network M such that Γ ⊢ M : G. If M executes a computation step M −→ M ′ , then the resulting system M ′ is also typed with Γ ⊢ M ′ : G ′ such that G −→ G ′ . Proof. The proof is done by induction on the definition of the operational semantics relation. The details of the proof can be found in [31].

E. Vanezi, D. Kouzapas & A. Philippou

271

Theorem 2 (Purpose Fidelity). Assume Γ ⊢ M : G. • If G = 0 then M ≡ 0; U

• If there exists G ′ such that G \ p → q = G ′ then there exists M ′ , G ′′ such that M −→ M ′ with Γ ⊢ M ′ : G ′′ and either G ′ = G or G ′ = G ′′ ; t ⊗g

i • If there exists G ′ such that G \ p → α = G ′ then there exists M ′ , G ′′ such that M −→ M ′ with ′′ ′ ′ ′ Γ ⊢ M : G and either G = G or G = G ′′ ;

t ⊗g

i • If there exists G ′ such that G \ α → p = G ′ then there exists M ′ , G ′′ such that M −→ M ′ with ′′ ′ ′ ′ Γ ⊢ M : G and either G = G or G = G ′′ ;

ℓ

ℓ

k m q = G ′′ then there exists G ′ , ℓm such that G \ p → q = G ′ , and • If there exists G ′′ such that G \ p → ′′′ ′′′ ′ ′ ′ ′ ′ there exists M , G such that M −→ M with Γ ⊢ M : G and either G = G or G = G ′′′ .

Proof. We note that in the last four clauses G = G ′ may arise due to conditional statements, whereas, in the last clause, G ′′′ may arise due to subtyping. The details of the proof can be found in [31]. Intuitively, these two results establish our goal of assuring that an implementation is purpose compliant. In particular, recall that a multiparty purpose protocol (a global type) in our framework provides a structured specification of a privacy purpose. Such a protocol describes how multiple participants exchange information and coordinate control over private data and private data stores (e.g., databases). Assume a program M handling private data adheres to a purpose G under an environment Γ, i.e., Γ ⊢ M : G. The Subject Reduction Theorem ensures that all execution steps of M conform to the purpose G: every interaction performed by M is prescribed by G in the sense that after evolution M remains welltyped by a global type to which G can reduce. In other words, the program cannot exhibit behaviour outside the specified protocol. Conversely, the Purpose Fidelity Theorem guarantees that M is never stuck when the purpose G prescribes an interaction: whenever G can consume an action, the program can perform a corresponding computation step. Together, these results establish a tight correspondence between programs and purposes: Soundness (Subject Reduction): programs do not exceed the specified purpose. Completeness (Purpose Fidelity): programs can realise all interactions required by the purpose. Hence, the theory provides strong guarantees that purpose specifications are both safe (no unintended behaviour) and enforceable (all intended behaviour is executable) for programs handling private data.

6

Case Study: Medical Diagnostics Workflow

To illustrate the expressiveness of our calculus and the applicability of our typing and compliance framework, we present a case study based on a medical diagnostics workflow, inspired by common healthcare scenarios in the formal privacy and purpose-limitation literature [30, 15, 16]. The case study demonstrates how intended processing purposes are specified, how system implementations are modelled, and how both compliance and violations are detected by our type system.

272

6.1

MPST for GDPR Purpose Compliance

Case Study Overview and Intended Purpose

The workflow concerns a patient undergoing a diagnostic process managed by a digital healthcare system. The diagnostic process unfolds as follows: The patient (participant patient) initially sends their personal information (via store r i ), writes and sends their symptoms (via store r s ), both to be received by a nurse practitioner (participant nurse). The nurse reads the data from the two stores and performs an initial screening, determining whether further laboratory testing is required before forwarding the case to the general practitioner (participant practitioner). Depending on the decision, if a lab test is needed, the nurse creates and sends a laboratory order (store r o ) to the lab (participant lab), who reads the order, performs the test, writes down the results (store r r ), and sends them to the nurse. In both cases, the nurse sends the symptoms (store r s ) to the general practitioner, and if there was a lab test also the results (store r r ). The general practitioner then reads the received data, performs a diagnostic assessment, and records the diagnosis (store r d ), which is returned to the nurse. The nurse then forwards the diagnosis (store r d ) to the patient. Throughout this workflow, access to personal data is restricted to what is necessary for performing the diagnostic process, in accordance with the intended purpose.

6.2

System Participants and Data Stores

The workflow involves the following participants: patient (patient), nurse practitioner (nurse), laboratory (lab), and general practitioner (practitioner). As discussed in Section 2, personal data are stored in dedicated data stores, which are accessed via references. The following store references and types appear: • r i (demographic and administrative information e.g., age, patient ID), of type info[id ⊗ basicInfo], i.e., decorated with the static annotation info and holding data of type (id ⊗ basicInfo); • r s (symptoms reported by the patient), with type symptoms [id ⊗ sympt] • r o (laboratory test order), with type lorder [id ⊗ labOrder] • r r (laboratory results), with type results [id ⊗ labRes] • r d (final diagnostic report), with type diagnosis [id ⊗ diagnReport]

6.3

Formal Specification of Processing Purposes

The diagnostic processing purpose of the workflow is formalised as the following global type (G diagnostic ), which specifies the allowed interaction patterns and data accesses between participants in compliance with the intended diagnostics purpose. For readability reasons, we factor the final diagnostic continuations into ‘withLab’ and ‘noLab’. The specification distinguishes between diagnostic paths that require laboratory testing and those that do not, while ensuring that personal data are accessed only by specified entities and only when required by the diagnostic purpose. For brevity, when exchanging store references, we write only the annotation, omitting the full type info. For example, we write patient → nurse:⟨info⟩. G instead of patient → nurse:⟨info[id ⊗ basicInfo]⟩. G. G diagnostic = patient → symptoms:⟨id ⊗ sympt⟩. patient → nurse:⟨info⟩. patient → nurse:⟨symptoms⟩. info → nurse:⟨id ⊗ basicInfo⟩. symptoms →  nurse:⟨id ⊗ sympt⟩. noLab : noLab, nurse → lab : lab : withLab

E. Vanezi, D. Kouzapas & A. Philippou

273

  noLab : nurse → practitioner:⟨symptoms⟩.         symptoms → practitioner:⟨id ⊗ sympt⟩.       practitioner → diagnosis:⟨id ⊗ diagnReport⟩. noLab = nurse → practitioner : practitioner → nurse:⟨diagnosis⟩.           nurse → patient:⟨diagnosis⟩.     end

withLab = nurse → lorder:⟨id ⊗ labOrder⟩. nurse → lab:⟨lorder⟩. lorder → lab:⟨id ⊗ labOrder⟩. lab → results:⟨id ⊗ labRes⟩. lab → nurse:⟨results⟩.   lab : nurse → practitioner:⟨symptoms⟩.         nurse → practitioner:⟨results⟩.         symptoms → practitioner:⟨id ⊗ sympt⟩.       results → practitioner:⟨id ⊗ labRes⟩. nurse → practitioner : practitioner → diagnosis:⟨id ⊗ diagnReport⟩.           practitioner → nurse:⟨diagnosis⟩.         nurse → patient:⟨diagnosis⟩.     end We now project the global type, into local types for each participant. We demonstrate below the local type for participant practitioner. The projection reflects that practitioner receives a label from nurse, and subsequently receives and accesses the corresponding data depending on the diagnostic path, and performs a diagnosis.  lab :       

 nurse?symptoms.nurse?results.     symptoms?(id ⊗ sympt). results?(id ⊗ labRes).    diagnosis!⟨id ⊗ diagnReport⟩. nurse!diagnosis.end, G⌉practitioner = nurse & noLab : nurse?symptoms.           symptoms?(id ⊗ sympt). diagnosis!⟨id ⊗ diagnReport⟩.     nurse!diagnosis.end The complete set of the projected local types can be found in [31].

6.4

Modelling a Purpose-Compliant Implementation

We use the calculus syntax to model a system implementation that follows the interaction prescribed by the diagnostic purpose global type, and is thus intended to be type-compliant with G diagnostic . We present the process for the practitioner, as well as the network. All other participants are defined analogously and conform to their projected local types and can be found in [31].   nurse?(xs ).nurse?(xr ).xr ?(xid1 ⊗ zr ).xs ?(xid1 ⊗ zs ).  lab :  rd !⟨xid1 ⊗ diagn1 ⟩.nurse!⟨rd ⟩.0, D = nurse ▷   noLab : nurse?(xs ).xs ?(id ⊗ zs ).r d !⟨id ⊗ diagn1 ⟩.nurse!⟨rd ⟩.0 M = nurse ▶ [A] | patient ▶ [B] | lab ▶ [C] | practitioner ▶ [D] | r i ▶ [id 1 ⊗ basicInfo] | r s ▶ [id 1 ⊗ w1 ] | r o ▶ [id 1 ⊗ w2 ] | r r ▶ [id 1 ⊗ w3 ] | r d ▶ [id 1 ⊗ w4 ]

274

MPST for GDPR Purpose Compliance

Compliance Verification via Type Checking. Using our type system, we may check whether the system’s behaviour complies with the specified purpose. Demo application of the typing rules can be found in [31]. By applying the typing rules, we observe that the process of each participant corresponds to the associated projected local type from G diagnostic . Consequently, network M is typable under the declared global type G diagnostic . Therefore, M is purpose-compliant.

6.5

Modelling and Detection of Non-Compliant Behaviour

We introduce a deviation of the model in which the general practitioner (practitioner) accesses the patient’s medical data without completing the diagnostic process, resulting in processing that does not fulfil the declared purpose.   lab : nurse?(xs ).nurse?(xr ).xr ?(id ⊗ zr ).xs ?(id ⊗ zs ).0, Dnc = nurse ▷ noLab : nurse?(xs ).xs ?(id ⊗ zs ).0 Mnc = nurse ▶ [A] | patient ▶ [B] | lab ▶ [C] | practitioner ▶ [Dnc ] | r i ▶ [id 1 ⊗ basicInfo] | r s ▶ [id 1 ⊗ w1 ] | r o ▶ [id 1 ⊗ w2 ] | r r ▶ [id 1 ⊗ w3 ] | r d ▶ [id 1 ⊗ w4 ] Violation Detection via Type Checking. In this case, application of the typing rules indicates that all participants except practitioner correspond to their roles in the projected local types. The type system detects this unauthorised interaction, and the network Mnc is rejected as non-compliant.

7

Conclusions

Aiming to address the GDPR purpose limitation principle which mandates that systems should collect and process personal data according to explicitly specified purposes, and building upon our previous work of [32, 33] and relevant literature, we have presented a formal, purpose-aware framework grounded in multiparty session types. The presented approach allows the specification of purposes in systems as structured interaction protocols, the modelling of system implementations that process personal data using a process calculus, and the compliance verification between the two, recognising and reporting non-compliant system implementations through a type system. To achieve this, the framework integrates the notion of personal data [19] into multiparty session types [26, 12, 13]. We establish subject reduction and purpose fidelity results. Our approach bears promise for practical applicability in software engineering through the direct correspondence between the proposed global types for capturing purposes and purpose-enhanced UML sequence diagrams [32, 33]. As future work, we plan to extend the type system with a linear dimension to ensure properties such as uniqueness of store references. We also aim to support additional analyses, including model checking, to validate further properties of purposes and other GDPR requirements. Moreover, we plan to extend the calculus to support more complex system definitions, such as multiple parallel sessions and dynamic store creation. Ultimately, our objective is to evolve this work into a software-engineeringoriented approach that unifies purpose modelling and compliance verification within a lifecycle-driven methodology, enabling end-to-end purpose compliance validation. As such, we envision the development of a tool that will automate the formal purpose-compliance validation process, and support its integration into software engineering practice, alongside sequence diagrams, thereby advancing a practical privacyby-design approach.

E. Vanezi, D. Kouzapas & A. Philippou

275

References [1] Amir Shayan Ahmadian, Daniel Strüber & Jan Jürjens (2019): Privacy-enhanced system design modeling based on privacy features. In: Proceedings of the 34th ACM/SIGAPP Symposium on Applied Computing, pp. 1492–1499, doi:10.1145/3297280.3297431. [2] Hanaa Alshareef, Sandro Stucki & Gerardo Schneider (2021): Refining privacy-aware data flow diagrams. In: Proceedings of the 19th International Conference on Software Engineering and Formal Methods (SEFM 2021), LNCS, Springer, pp. 121–140, doi:10.1007/978-3-030-92124-8_8. [3] Hanaa Alshareef, Sandro Stucki & Gerardo Schneider (2021): Transforming Data Flow Diagrams for Privacy Compliance. In: Proceedings of the 9th International Conference on ModelDriven Engineering and Software Development (MODELSWARD 2021), SCITEPRESS, pp. 207–215, doi:10.5220/0010255002070215. [4] Hanaa Alshareef, Katja Tuma, Sandro Stucki, Gerardo Schneider & Riccardo Scandariato (2022): Precise Analysis of Purpose Limitation in Data Flow Diagrams. In: Proceedings of the 17th International Conference on Availability, Reliability and Security (ARES 2022), ACM, pp. 17:1–17:11, doi:10.1145/3538969.3539010. [5] Theodor Angergård & Tobias Karlsson (2022): Realizing Privacy-Aware Data Flow Diagrams in Java. Master’s thesis, Chalmers University of Technology, Gothenburg, Sweden. [6] David Basin, Søren Debois & Thomas Hildebrandt (2018): On Purpose and by Necessity: Compliance under the GDPR. In: Proceedings of the 22nd International Conference on Financial Cryptography and Data Security (FC 2018), LNCS 10957, Springer, pp. 20–37. [7] M Emilia Cambronero, Miguel A Martínez, Luis Llana, Ricardo J Rodríguez & Alejandro Russo (2024): Towards a GDPR-compliant cloud architecture with data privacy controlled through sticky policies. PeerJ Computer Science 10, p. e1898, doi:10.7717/peerj-cs.1898. [8] Riccardo De Masellis, Chiara Ghidini & Silvio Ranise (2015): A Declarative Framework for Specifying and Enforcing Purpose-Aware Policies. In: Proceedings of the 11th International Workshop on Security and Trust Management (STM 2015), LNCS 9331, Springer, pp. 55–71, doi:10.1007/978-3-319-24858-5_4. [9] European Parliament and Council of the European Union (2015): General Data Protection Regulation. Official Journal of the European Union. [10] Pietro Ferrara, Fausto Spoto et al. (2018): Static analysis for GDPR compliance. In: CEUR Workshop Proceedings, 2058, CEUR Workshop Proceedings, pp. 1–10. [11] Silvia Ghilezan, Svetlana Jakšić, Jovanka Pantović, Alceste Scalas & Nobuko Yoshida (2019): Precise subtyping for synchronous multiparty sessions. Journal of Logical and Algebraic Methods in Programming 104, pp. 127–173, doi:10.1145/3434297. [12] Kohei Honda, Vasco T Vasconcelos & Makoto Kubo (1998): Language primitives and type discipline for structured communication-based programming. In: Proceedings of the 7th European Symposium on Programming (ESOP 1998), Springer, pp. 122–138, doi:10.1007/bfb0053567. [13] Kohei Honda, Nobuko Yoshida & Marco Carbone (2008): Multiparty asynchronous session types. In: Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2008), ACM, pp. 273–284, doi:10.1145/2827695. [14] Mohammad Jafari, Philip W.L. Fong, Reihaneh Safavi-Naini, Ken Barker & Nicholas Paul Sheppard (2011): Towards Defining Semantic Foundations for Purpose-Based Privacy Policies. In: Proceedings of the 1st ACM Conference on Data and Application Security and Privacy (CODASPY 2011), ACM, pp. 213–224, doi:10.1145/1943513.1943541. [15] Mohammad Jafari, Reihaneh Safavi-Naini, Philip WL Fong & Ken Barker (2014): A framework for expressing and enforcing purpose-based privacy policies. ACM Transactions on Information and System Security 17(1), pp. 3:1–3:31, doi:10.1145/2629689.

276

MPST for GDPR Purpose Compliance

[16] Mohammad Jafari, Reihaneh Safavi-Naini & Nicholas Paul Sheppard (2009): Enforcing purpose of use via workflows. In: Proceedings of the 8th ACM Workshop on Privacy in the Electronic Society (WPES 2009), ACM, pp. 113–116, doi:10.1145/1655188.1655206. [17] Florian Kammüller, Oladapo O Ogunyanwo & Christian W Probst (2019): Designing data protection for GDPR compliance into IoT healthcare systems. arXiv preprint arXiv:1901.02426. [18] Dimitrios Kouzapas, Ornela Dardha, Roly Perera & Simon J Gay (2016): Typechecking protocols with Mungo and StMungo. In: Proceedings of the 18th International Symposium on Principles and Practice of Declarative Programming (PPDP 2016), ACM, pp. 146–159, doi:10.1145/2967973.2968595. [19] Dimitrios Kouzapas & Anna Philippou (2017): Privacy by typing in the π-calculus. Logical Methods in Computer Science 13(4), doi:10.23638/LMCS-13(4:27)2017. [20] Eirini Mougiakou & Maria Virvou (2017): Based on GDPR privacy in UML: Case of e-learning program. In: Proceedings of the 8th International Conference on Information, Intelligence, Systems & Applications (IISA 2017), IEEE, pp. 1–8, doi:10.1109/IISA.2017.8316456. [21] Gabriel Pedroza, Victor Muntes-Mulero, Yod Samuel Martin & Guillaume Mockly (2021): A Modelbased approach to realize privacy and data protection by design. In: Proceedings of IEEE European Symposium on Security and Privacy Workshops (EuroS&PW 2021), IEEE, pp. 332–339, doi:10.1109/EuroSPW54576.2021.00042. [22] Neda Peyrone & Duangdao Wichadakul (2022): Formal models for consent-based privacy. Journal of Logical and Algebraic Methods in Programming 128, p. 100789, doi:10.1016/j.jlamp.2022.100789. [23] Benjamin C Pierce (2002): Types and programming languages. MIT Press. [24] Mushfiqur Rahman (2017): A Petri Nets Semantics for Privacy-Aware Data Flow Diagrams. Master’s thesis, University of Gothenburg, Gothenburg, Sweden. [25] Shahrzad Riahi, Ramtin Khosravi & Fatemeh Ghassemi (2017): Purpose-Based Policy Enforcement in ActorBased Systems. In: Proceedings of the 7th International Conference on Fundamentals of Software Engineering (FSEN 2017), LNCS 10522, Springer, pp. 196–211. [26] Kaku Takeuchi, Kohei Honda & Makoto Kubo (1994): An interaction-based language and its typing system. In: Proceedings of the 6th International Conference on Parallel Architectures and Languages Europe (PARLE 1994), Springer, pp. 398–413, doi:10.1007/3-540-58184-7_118. [27] Shukun Tokas & Olaf Owe (2020): A formal framework for consent management. In: Proceedings of the 40th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE 2020), LNCS 12136, Springer, pp. 169–186, doi:10.1007/978-3-030-50086-3_10. [28] Damiano Torre, Mauricio Alferez, Ghanem Soltana, Mehrdad Sabetzadeh & Lionel Briand (2020): Model driven engineering for data protection and privacy: Application and experience with GDPR. arXiv preprint arXiv:2007.12046. [29] Michael Carl Tschantz, Anupam Datta & Jeannette M Wing (2011): On the semantics of purpose requirements in privacy policies. arXiv preprint arXiv:1102.4326, doi:10.48550/arXiv.1102.4326. [30] Michael Carl Tschantz, Anupam Datta & Jeannette M. Wing (2012): Formalizing and Enforcing Purpose Restrictions in Privacy Policies. In: Proceedings of the IEEE Symposium on Security and Privacy (SP 2012), IEEE Computer Society, pp. 176–190, doi:10.1109/SP.2012.21. [31] Evangelia Vanezi (2026): Multiparty Session Types for GDPR Purpose Compliance. https://students.cs.ucy. ac.cy/~evanez01/Multiparty_Session_Types_for_GDPR_Purpose_Compliance.pdf. Accessed: 2026-06-08. [32] Evangelia Vanezi, Georgia Kapitsaki & Anna Philippou (2024): What’s Your Purpose? An Approach to Incorporating GDPR Purposes into Requirements Analysis. In: Proceedings of the 10th International Conference on Information Systems Security and Privacy (ICISSP 2024), Scitepress, pp. 907–914, doi:10.5220/0012474400003648. [33] Evangelia Vanezi, Georgia Kapitsaki & Anna Philippou (2025): Privacy-Enhanced Software Design: Purpose-Aware UML Diagrams. In: Proceedings of the 26th International Conference on Product-Focused

E. Vanezi, D. Kouzapas & A. Philippou

277

Software Process Improvement (PROFES 2025), Springer, pp. 429–439, doi:10.1007/978-3-032-12089-2_28. [34] Evangelia Vanezi, Georgia M Kapitsaki, Dimitrios Kouzapas, Anna Philippou & George A Papadopoulos (2020): Diálogop-A language and a graphical tool for formally defining GDPR purposes. In: Proceedings of the 14th International Conference on Research Challenges in Information Science (RCIS 2020), LNBIP 385, Springer, pp. 569–575, doi:10.1007/978-3-030-50316-1_40. [35] Evangelia Vanezi, Dimitrios Kouzapas, Georgia M Kapitsaki, Theodora Costi, Alexandros Yeratziotis, Christos Mettouris, Anna Philippou & George A Papadopoulos (2019): GDPR Compliance in the Design of the INFORM e-Learning Platform: a Case Study. In: Proceedings of the 13th International Conference on Research Challenges in Information Science (RCIS 2019), IEEE, pp. 1–12, doi:10.1109/RCIS.2019.8877022. [36] Tong Ye, Yi Zhuang & Gongzhe Qiao (2023): MBIPV: a model-based approach for identifying privacy violations from software requirements. Software and Systems Modeling 22(4), pp. 1251–1280, doi:10.1145/3538969.3539010. [37] Nobuko Yoshida & Lorenzo Gheri (2020): A very gentle introduction to multiparty session types. In: Proceedings of the 16th International Conference on Distributed Computing and Internet Technology (ICDCIT 2020), LNCS 11969, Springer, pp. 73–93. [38] Nobuko Yoshida & Vasco T Vasconcelos (2007): Language primitives and type discipline for structured communication-based programming revisited: Two systems for higher-order session communication. Electronic Notes in Theoretical Computer Science 171(4), pp. 73–93, doi:10.1016/j.entcs.2007.02.056.