Probabilistic model checking of anonymity communication system 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.