论文研究匿名通信协议MACP概率模型检验.pdf

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