%0 Journal Article
%T Probabilistic model checking of anonymity communication system MACP<br>匿名通信协议MACP概率模型检验
%A XU Jing
%A WANG Zhen-xing
%A ZHANG Lian-cheng
%A <br>徐　静
%A 王振兴
%A 张连成
%J 计算机应用研究
%D 2012
%I 
%X 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.
%K anonymous communication
%K peer-to-peer（P2P）
%K MACP
%K probabilistic model checking<br>匿名通信
%K P2P
%K MACP
%K 概率模型检验
%U http://www.alljournals.cn/get_abstract_url.aspx?pcid=5B3AB970F71A803DEACDC0559115BFCF0A068CD97DD29835&cid=8240383F08CE46C8B05036380D75B607&jid=A9D9BE08CDC44144BE8B5685705D3AED&aid=F6B2E1193D3BD8E6BEA4D47B525D6C3F&yid=99E9153A83D4CB11&vid=771469D9D58C34FF&iid=708DD6B15D2464E8&sid=11FE01C693053C08&eid=21BF9BE2D0451BEE&journal_id=1001-3695&journal_name=计算机应用研究&referenced_num=0&reference_num=9