匿名通信协议MACP概率模型检验

Probabilistic model checking of anonymity communication system MACP

匿名通信技术是保护互联网用户隐私的最有力手段之一,但匿名通信协议的形式化验证仍是亟待解决的难题。对P2P匿名通信协议MACP进行了形式化验证与分析,将MACP协议的匿名路径建立过程模型化为一个离散时间马尔可夫链;然后利用概率计算树逻辑PCTL描述MACP协议的匿名性质,并采用概率模型检验器对MACP协议的匿名性进行检验。检验结果表明,通过增加匿名通道数,提高了MACP协议的匿名等级和抗攻击能力;MACP协议的匿名性随着规模的增大而增强,并没有因控制匿名路径的长度而降低。

Anonymity is one of most effective privacy enhancing technologies.However,formal verification of anonymous communication technologies is still a hard and open problem.This paper formally verified and analyzed MACP,a P2P anonymous communication protocol.It modeled the construction process of anonymous path of the MACP protocol as a discrete time Markov chain.Then it used PCTL to describe the MACP protocol＇s anonymity,and used the probability model checker to inspect it.The results show that,with the increasing number of anonymous channels,the proposed method improves anonymity level and anti-attack capability of MACP protocol are also improved.And with the expansion of the network size,it enhances the anonymity of the MACP protocol not affected by controlling length of anonymity path.