Advancements in information technology have led to the sharing of users' data across borders, raising privacy concerns, particularly when destination countries lack adequate protection measures. Regulations like the European General Data Protection Regulation (GDPR) govern international data transfers, imposing significant fines on companies failing to comply. To achieve compliance, we propose a privacy framework based on Milner's Bigraphical Reactive Systems (BRSs), a formalism modelling spatial and non-spatial relationships between entities. BRSs evolve over time via user-specified rewriting rules, defined algebraically and diagrammatically. In this paper, we rely on diagrammatic notations, enabling adoption by end-users and privacy experts without formal modelling backgrounds. The framework comprises predefined privacy reaction rules modelling GDPR requirements for international data transfers, properties expressed in Computation Tree Logic (CTL) to automatically verify these requirements with a model checker and sorting schemes to statically ensure models are well-formed. We demonstrate the framework's applicability by modelling WhatsApp's privacy policies.

翻译：信息技术的进步导致用户数据跨境共享，引发了隐私担忧，尤其在目的地国家缺乏充分保护措施的情况下。诸如《欧盟通用数据保护条例》（GDPR）等法规对国际数据传输进行规制，对未能合规的企业处以巨额罚款。为实现合规，我们提出一种基于米尔纳Bigraph反应系统（BRS）的隐私框架，该形式化方法能够建模实体间的空间与非空间关系。BRS通过用户定义的代数与图示重写规则随时间演化。本文采用图示表示法，使不具备形式化建模背景的终端用户和隐私专家也能理解应用。该框架包含预定义的隐私反应规则，用于建模GDPR对国际数据传输的要求；通过计算树逻辑（CTL）表达属性，以借助模型检查器自动验证这些要求；并采用分类方案静态确保模型的形式正确性。我们通过建模WhatsApp隐私政策，验证了该框架的适用性。