Modeling of Personalized Privacy Disclosure Behavior: A Formal Method Approach

TL;DR

This paper introduces a formal method using UPPAAL to model, verify, and analyze individual privacy disclosure behaviors, aiming to improve personalized privacy management tools.

Contribution

It presents a novel formal modeling and verification approach for personalized privacy behavior using extended finite state automata and model checking.

Findings

Effective modeling of user privacy behavior with UPPAAL

Verification of privacy properties via CTL formulas

Potential for designing user-centric privacy tools

Abstract

In order to create user-centric and personalized privacy management tools, the underlying models must account for individual users' privacy expectations, preferences, and their ability to control their information sharing activities. Existing studies of users' privacy behavior modeling attempt to frame the problem from a request's perspective, which lack the crucial involvement of the information owner, resulting in limited or no control of policy management. Moreover, very few of them take into the consideration the aspect of correctness, explainability, usability, and acceptance of the methodologies for each user of the system. In this paper, we present a methodology to formally model, validate, and verify personalized privacy disclosure behavior based on the analysis of the user's situational decision-making process. We use a model checking tool named UPPAAL to represent users' self-reported privacy disclosure behavior by an extended form of finite state automata (FSA), and perform reachability analysis for the verification of privacy properties through computation tree logic (CTL) formulas. We also describe the practical use cases of the methodology depicting the potential of formal technique towards the design and development of user-centric behavioral modeling. This paper, through extensive amounts of experimental outcomes, contributes several insights to the area of formal methods and user-tailored privacy behavior modeling.