作者投稿和查稿 主编审稿 专家审稿 编委审稿 远程编辑

计算机工程 ›› 2021, Vol. 47 ›› Issue (5): 144-153. doi: 10.19678/j.issn.1000-3428.0057769

• 网络空间安全 • 上一篇    下一篇

基于随机模型检验的社交网络隐私保护研究

刘阳, 高世国   

  1. 南京财经大学 信息工程学院, 南京 210046
  • 收稿日期:2020-03-18 修回日期:2020-05-13 发布日期:2021-05-11
  • 作者简介:刘阳(1981-),男,教授、博士,主研方向为形式化验证;高世国,硕士研究生。
  • 基金资助:
    江苏省“六大人才高峰”高层次人才项目(RJFW-014);江苏省高等学校自然科学研究重大项目(17KJA520002);南京市留学人员科技创新项目择优资助计划。

Research on Privacy Protection in Social Network Based on Stochastic Model Checking

LIU Yang, GAO Shiguo   

  1. School of Information Engineering, Nanjing University of Finance and Economics, Nanjing 210046, China
  • Received:2020-03-18 Revised:2020-05-13 Published:2021-05-11

摘要: 针对现有社交网络所提供静态隐私策略的隐私设置不够灵活且难以定量验证问题,提出一种动态隐私保护框架,将社交网络建模为离散时间马尔科夫链模型,通过设置触发条件实现用户动态隐私规约并将其转化为概率计算树逻辑公式,同时结合随机模型检验和运行时验证中的参数化与监控技术,保护社交网络发生随机故障情况下的用户动态隐私信息。在Diaspora开源社交网络上的实验结果表明,与静态隐私保护框架相比,动态隐私保护框架具有更高的安全性和灵活性,能较好满足用户的隐私保护需求。

关键词: 社交网络, 隐私保护, 运行时验证, 随机模型检验, 概率计算树逻辑

Abstract: The privacy settings in static privacy strategies of the existing online social networks are not flexible and hard for quantitative verification.To address the problem,this paper proposes a dynamic privacy protection framework,which models social networks as Discrete Time Markov Chains(DTMC).The dynamic privacy policy for users is realized by adding triggers and transformed into Probabilistic Computation Tree Logic(PCTL) formula.Then the stochastic model-based checking technique and parameterization and monitoring technique in runtime verification are used to protect users' dynamic privacy information in the case of random social network failures.Experimental results on the open-source social network called Diaspora show that compared with the static privacy protection framework,the proposed dynamic privacy protection framework has higher security and flexibility,meeting the privacy protection requirements of users.

Key words: social network, privacy protection, runtime verification, stochastic model checking, Probabilistic Computation Tree Logic(PCTL)

中图分类号: