基于用户同意的隐私保护协议形式化描述与验证  

Formalization and Verification of Privacy Preserving Protocol Based on User Consent

作　　者：马丽[1] 姜火文[1] 彭云[2] MA Li;JIANG Huo-wen;PENG Yun(School of Big Data Science,Jiangxi Science&Technology Normal University,Nanchang,Jiangxi 330038,China;School of Digital Industry,Jiangxi Normal University,Nanchang,Jiangxi 330022,China)

机构地区：[1]江西科技师范大学大数据科学学院,江西南昌330038 [2]江西师范大学数字产业学院,江西南昌330022

出　　处：《电子学报》2023年第7期1842-1849,共8页Acta Electronica Sinica

基　　金：江西省社会科学基金项目(No.21TQ08D);江西省高校人文社会科学研究项目(No.JC22115);江西省自然科学基金项目(No.20224BAB202013)。

摘　　要：将用户同意与访问控制相结合是解决隐私保护的主要方法之一.然而,现有的隐私保护访问控制方法仅从数据控制者的角度,不考虑个人对访问决策的参与,无法满足自主可控的需求.为了解决这个问题,本文提出了一种基于用户同意的隐私保护访问控制协议,将用户同意转化为一种同意权限,形成一种同意加授权的双重访问控制机制.本文给出协议的语法、语义及安全性定义和分析,并采用模型检测的方法对协议应满足的性质进行验证,最终证明本文的设计可以从访问控制的角度满足个人信息保护法规的要求.The combination of user consents and access control is one of the main approaches to address privacy pro⁃tection today.However,most of privacy protection access control approaches are from the perspective of the data control⁃ler,without considering individual participation in access decisions,and can not meet the need for privacy protection in terms of autonomy and control.In order to solve this problem,this paper proposes a privacy-preserving access control pro⁃tocol based on user consents,which transforms user consents into a kind of consent authority and forms a dual access con⁃trol mechanism of consent plus authorization.The syntax,semantics and security of the protocol are defined and analyzed.The properties that the protocol should satisfy are verified with the model checking method,which finally proves that the de⁃sign of this paper can comply with personal information protection regulations from the perspective of access control.

关 键 词：个人数据保护 隐私保护模型 隐私保护协议 访问控制 隐私授权 TLA+(Temporal Logic of Actions plus) 

分 类 号：TP309.2[自动化与计算机技术—计算机系统结构]