# Formalising privacy regulations with bigraphs

## TL;DR

This paper introduces a formal method using diagrams to help ensure systems comply with data privacy laws by modeling and verifying privacy policies.

## Contribution

A novel framework using bigraphs and formal methods to model and verify compliance with privacy regulations.

## Key findings

- The framework models privacy concepts like consent and data sharing using bigraphical reactive systems.
- Privacy properties are expressed in computation tree logic and verified via model checking.
- The approach is demonstrated on two real-world systems: a bank notification system and a healthcare app.

## Abstract

With many governments regulating the handling of user data—the General Data Protection Regulation, the California Consumer Privacy Act, and the Saudi Arabian Personal Data Protection Law—ensuring systems comply with data privacy legislation is of high importance. Checking compliance is a tricky process and often includes many manual elements. We propose that formal methods, that model systems mathematically, can provide strong guarantees to help companies prove their adherence to legislation. To increase usability we advocate a diagrammatic approach, based on bigraphical reactive systems, where privacy experts can explicitly visualise the systems and describe updates, via rewrite rules, that describe system behaviour. The rewrite rules allow flexibility in integrating privacy policies with user-specified systems. We focus on modelling notions of providing consent, withdrawing consent, purpose limitations, the right to access and sharing data with third parties, and define privacy properties that we want to prove within the systems. Properties are expressed using the computation tree logic and proved using model checking. To show the generality of the proposed framework, we apply it to two examples: a bank notification system, inspired by Monzo’s privacy policy, and a cloud-based home healthcare system based on the Fitbit app’s privacy policy.