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