匿名協(xié)議wongoo的概率模型驗(yàn)證分析-資料下載頁(yè)
2025-05-30 01:43本頁(yè)面
【正文】 性隨路徑長(zhǎng)度的變化關(guān)系。表4通過(guò)調(diào)整轉(zhuǎn)發(fā)概率Pf的大小來(lái)調(diào)整路徑長(zhǎng)度。表5通過(guò)調(diào)整固定節(jié)點(diǎn)數(shù)fixedNodeNum來(lái)調(diào)整路徑長(zhǎng)度?？梢钥闯?，隨著匿名路徑的增長(zhǎng)，驗(yàn)證概率降低，從而系統(tǒng)的匿名性得到了提高。表4 不同轉(zhuǎn)發(fā)概率下的驗(yàn)證概率（fixedNodeNum=4, FwLength=5, Totalrun=3）Table 4 Probabilities of detecting the initiator decrease with increasing forward probabilities WonGooPF 10 honest, 1 corruptPr(%)15 honest, 2 corruptPr(%)10 honest, 2 corruptPr(%)15 honest, 3 corruptPr(%)20 honest, 4 corruptPr(%)25 honest, 5 corruptPr(%)表5 不同固定節(jié)點(diǎn)數(shù)下的驗(yàn)證概率（PF=, FwLength=5, Totalrun=3）Table 5 Probabilities of detecting the initiator decrease with increasing fixed node numbersWonGoofixedNodeNum2468101210 honest, 1 corruptPr(%)15 honest, 2 corruptPr(%)10 honest, 2 corruptPr(%)15 honest, 3 corruptPr(%)20 honest, 4 corruptPr(%)25 honest, 5 corruptPr(%)7 結(jié)論形式化方法是對(duì)安全協(xié)議進(jìn)行驗(yàn)證的一種有力工具。如何利用已有的形式化方法對(duì)匿名協(xié)議進(jìn)行分析是一個(gè)極具挑戰(zhàn)的問(wèn)題。概率模型驗(yàn)證是一種十分有效的協(xié)議形式化分析工具。本文利用PRISM模型驗(yàn)證器對(duì)匿名通信協(xié)議WonGoo進(jìn)行了分析。WonGoo通過(guò)隨機(jī)轉(zhuǎn)發(fā)和分層加密建立匿名通信路徑。因此，我們把WonGoo的路徑建立過(guò)程模型化為一個(gè)離散時(shí)間Markov鏈，并在攻擊者可以識(shí)別出兩條鏈路是否源自同一發(fā)送者的假設(shè)下，分析了攻擊者識(shí)別出一條匿名路徑的發(fā)起者的概率。WonGoo協(xié)議的分析表明了利用概率模型驗(yàn)證技術(shù)分析安全協(xié)議的可行性。References:[1] T. Lu, B. Fang, Y. Sun, X. Cheng. WonGoo: A PeertoPeer Protocol for Anonymous Communication, In Proceedings of the 2004 International Conference on Parallel and Distributed Processing Techniques and Applications (PDPTA04), June 2004: 11021106.[2] D. Chaum. Untraceable electronic mail, return addresses and digital pseudonyms. Communications of the ACM, February 1981, 24(2): 8488. [3] M. K. Reiter and A. D. Rubin. Crowds: Anonymity for Web Transactions. ACM Transactions on Information and System Security, November 1998, 1(1): 6692.[4] A. Pfitzmann and M. K246。hntopp. Anonymity, Unobservability, and Pseudonymity – A Proposal for Terminology, Draft . , May 2003.[5] H. Hansson and B. Jonsson. A logic for reasoning about time and reliability. Formal Aspects of Computing, 1994, 6(5): 512535. [6] ~dxp/prism[7] . Clarke, . Emerson, and . Sistla. Automatic verification of finitestate concurrent systems using temporal logic specification. ACM Trans. on Programming Languages and Systems, 1986, 8(2): 244263.[8] . Implementation of Symbolic Model Checking for Probabilistic Systems. . Thesis, University of Birmingham, August 2002.[9] V. Shmatikov. Probabilistic Analysis of Anonymity. In Proc. 15th IEEE Computer Security Foundations Workshop (CSFW39。02), June 2002: 119128.[10] Y. Guan, X. Fu, R. Bettati, and W. Zhao, An Optimal Strategy for Anonymous Communication Protocols, in Proceedings of the 22nd IEEE International Conference on Distributed Computing Systems (ICDCS 2002), July 2002: 257266.9 / 9
規(guī)章制度相關(guān)推薦
鄂ICP備17016276號(hào)-1