Modeling of Personalized Privacy Disclosure Behavior: A Formal Method Approach
Modeling of Personalized Privacy Disclosure Behavior: A Formal Method Approach
复制标题
DOI：
10.1145/3465481.3470102
复制
发表时间：
2021-06
期刊：
影响因子：
--
通讯作者：
Nuhil Mehdy;Hoda Mehrpouyan
中科院分区：
文献类型：
--
作者：
Nuhil Mehdy;Hoda Mehrpouyan
为了创建以用户为中心的个性化隐私管理工具，底层模型必须考虑到个人用户的隐私期望、偏好以及他们控制信息共享活动的能力。现有的用户隐私行为建模研究试图从请求的角度来构建问题，这缺乏信息所有者的关键参与，导致策略管理的控制有限或没有。此外，他们很少考虑到正确性，可解释性，可用性和接受的系统的每个用户的方法方面。在本文中，我们提出了一种方法来正式建模，验证和验证个性化的隐私泄露行为的基础上分析用户的情景决策过程。我们使用一个名为UPPAAL的模型检测工具来表示用户的自我报告的隐私泄露行为的有限状态自动机（FSA）的扩展形式，并进行可达性分析的隐私属性验证通过计算树逻辑（CTL）公式。我们还描述了实际的使用案例的方法描绘的潜力，正式技术的设计和开发以用户为中心的行为建模。本文通过大量的实验结果，为形式化方法和用户定制隐私行为建模领域提供了一些见解。
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.