Research On Privacy Preserving In Social Network Based On Stochastic Model Checking

Through the social network had made a great development,social networks not only become an important communication medium in people's daily life,but also play an important role in the country's political public opinion.However,due to the uncertainty of the operating environment of social networks and the characteristics of multi-source data fusion,there is a lack of internal safety in social networks.The static privacy policy currently provided for users in social networks is difficult to protect users' privacy information in random environment.At the same time,there are a lot of potential malicious users in the social networks.They use more confidential attack methods to steal users' privacy information,which leads to the problem of insufficient external confidentiality.The above two kinds of problems lead to the leakage of users' privacy information in social networks from time to time,which not only causes huge economic losses,but also seriously endangers the national public security.This paper mainly aims at the problems of internal safety and external security of social networks,and put forward the corresponding solutions:(1)This paper proposed a dynamic privacy preserving framework(DPF),in which the social networks is modeled as DTMC(Discrete Time Markov Chains),The current static privacy policy is improved to a rule-based dynamic privacy strategy with trigger conditions,and the dynamic privacy policy is formally expressed as PCTL(Probabilistic Computing Tree Logic)formula.According to the user's privacy protection intention,it can be divided into dynamic privacy strategy based on time,location and events.It further improves the stability,flexibility and consistency of social network privacy policy,reduces the probability of user privacy information leakage in the random operation environment of social network,and enhances the privacy security of social network.(2)A PCTL conversion algorithm based on KBL(Knowledge-Based Logic)is proposed.KBL can be used to represent the state of user's knowledge base in social networks because it can realize first-order knowledge logic reasoning,but it can't be directly applied to PRISM.Through this algorithm,we can set K operator for KBL and convert it to PCTL.It can be directly identified by PRISM to realize the automatic verification of privacy protection in social networks.It makes the whole verification process more automatic and quantitative(3)This paper proposed an intrusion detection method for malicious users to grab user's privacy information.The malicious users and monitors under the dynamic privacy protection framework are modeled as CSMG(Concurrent Stochastic Multiplayer Games)model.The behavior strategy set is set for both sides of the game,and the optimal defense strategy selection of the monitor is continuously improved through the dynamic game process of both sides.With the help of automated game verification tool PRISM-Games,the privacy protection effect of social networks is verified under the continuous attack of malicious users.