计算机科学 ›› 2015, Vol. 42 ›› Issue (9): 118-126.doi: 10.11896/j.issn.1002-137X.2015.09.023
刘海,彭长根,张 弘,任祉静
LIU Hai, PENG Chang-gen, ZHANG Hong and REN Zhi-jing
摘要: 博弈逻辑ATL和ATEL可以对传统安全协议的公平性、安全性等性质进行分析与验证。但在理性环境中,由于参与者对知识的自利性,ATL和ATEL都不能形式化分析与验证理性安全协议。因此在CEGS中引入效用函数和偏好关系知识,得到新的rCEGS,并在合作模态算子《Γ》中加入行为ACT参数,提出新的可形式化分析理性安全协议的交替时序认知逻辑rATEL-A。然后运用rATEL-A构建两方理性安全协议的形式化模型,并基于rCEGS的等价扩展式博弈,对具体的两方理性交换协议进行形式化分析,结果表明构建的形式化模型可以有效地形式化分析理性安全协议的正确性、理性安全性和理性公平性。
[1] Syverson P.Weakly secret bit commitment:applications to lotteries and fair exchange[C]∥Proceedings of 11th IEEE Computer Security Foundations Workshop.United States:IEEE,1998:2-13 [2] Halpern J,Teague V.Rational secret sharing and multipartycomputation:extended abstract[C]∥Proceedings of the Thirty-Sixth Annual ACM Symposium on Theory of Computing(STOC’04).New York:ACM,2004:623-632 [3] Alur R,Henzinger T,Kupferman O.Alternating-time temporal logic[C]∥38th Annual Symposium on Foundations of Compu-ter Science.United States:IEEE,1997:100-109 [4] Alur R,Henzinger T,Kupferman O.Alternating-time temporal logic[M].Springer Berlin Heidelberg,1998:23-60 [5] Alur R,Henzinger T,Kupferman O.Alternating-time temporal logic[J].Journal of The ACM(JACM),2002,9(5):672-713 [6] Mahimkar A,Shmatikov V.Game-Based Analysis of Denial-of-Service Prevention Protocols[C]∥Proceedings of the 18th IEEE Computer Security Foundations Workshop(CSFW’05).United States:Institute of Electrical and Electronics Engineers Compu-ter Society,2005:287-301 [7] 文静华,张梅,李祥.基于博弈的电子商务协议分析[J].通信学报,2006,27(3):73-78 Wen Jing-hua,Zhang Mei,Li Xiang.Formal Analysis of E-commerce Protocols Based on Game[J].Journal on Communications,2006,27(3):73-78 [8] 张梅,文静华,张焕国.基于ATL方法的电子商务协议FONRP分析[J].计算机工程,2008,34(3):151-153 Zhang Mei,Wen Jing-hua,Zhang Huan-guo.Analysis of E-commerce Protocol FONRP Based on ATL[J].Computer Enginee-ring,2008,34(3):151-153 [9] Long Shi-gong,Luo Wen-jun.Model Checking Alternating-time Temporal Logics of Knowledge[C]∥4th International Confe-rence on Wireless Communications,Networking and Mobile Computing,2008(WiCOM’08).United States:IEEE,2008:1-3 [10] Long Shi-gong.Protocol Analysis Through Alternating-timeTemporal Logic and Timed Petri Net Models[C]∥5th International Conference on Wireless Communications,Networking and Mobile Computing,2009(WiCom’09).United States:IEEE,2009:1-4 [11] Zhang Ying,Zhang Chen-yi,Pang Jun,et al.Game-based Verification of Multi-party Contract Signing Protocols[M]∥ Formal Aspects in Security and Trust.Springer,2010:186-200 [12] Zhang Ying,Zhang Chen-yi,Pang Jun,et al.Game-based Verification of Contract Signing Protocols with Minimal Messages[J].Innovations in Systems and Software Engineering,2012,8(2):111-124 [13] Jamroga W,Mauw S,Melissen M.Fairness in Non-Repudiation Protocols[M]∥Security and Trust Management.Springer,2012:122-139 [14] Jiang Yun,Gong Hua-ping.Modeling and Formal Analysis of Communication Protocols Based on Game[J].Information Technology Journal,2012,12(3):470-473 [15] Van Der Hoek W,Wooldridge M.Tractable multiagent planning for epistemic goals[C]∥Proceedings of the First International Joint Conference on Autonomous Agents and Multiagent Systems:Part 3(AAMAS’02).New York:ACM,2002:1167-1174 [16] Jamroga W.Some remarks on alternating temporal epistemiclogic[C]∥Proceedings of Formal Approaches to Multi-Agent Systems(FAMAS 2003).2004 [17] Agotnes T.Action and knowledge in alternating-time temporal logic[J].Synthese,2006,149(2):375-407 [18] Buttyan L,Hubaux J,Capkun S.A formal model of rational exchange and its application to the analysis of syverson’s protocol[J].Journal of Computer Security-JCS,2004,12(3/4):551-587 [19] Alcide A.Rational exchange protocols[D].Leganés:Universidad Carlos III Department,2008 [20] Van Otterloo S,Van Der Hoek W,Wooldridge M.Preferences in game logics[C]∥Proceedings of the Third International Joint Conference on Autonomous Agents and Multiagent Systems(AAMAS’04).United States:IEEE,2004:152-159 [21] Van Benthem J,Van Otterloo S,Roy O.Preference Logic,Conditionals and Solution Concepts in Games[M]∥Lindstrm S,Lagerlund H,Sliwinski R,eds.Modality matters.Festschrift for krister segerberg,University of Uppsala,2005:61-67 [22] Walther D,Van Der Hoek W,Wooldridge M.Alternating-time temporal logic with explicit strategies[C]∥Proceedings of the 11th Conference on Theoretical Aspects of Rationality and Knowledge(TARK’07).New York:ACM,2007:269-278 [23] Goranko V,Van Drimmelen G.Complete axiomatization and decidability of alternating-time temporal logic[J].Theoretical Computer Science-TCS,2006,353(1-3):93-117 [24] Goranko V.Coalition games and alternating temporal logics[C]∥Proceedings of the 8th Conference on Theoretical Aspects of Rationality and Knowledge(TARK’01).San Francisco:Morgan Kaufmann Publishers Inc,2001:259-272 [25] Van Der Hoek W,Jamroga W,Wooldridge M.A logic for strategic reasoning[C]∥Proceedings of the Fourth International Joint Conference on Autonomous Agents and Multiagent Systems(AAMAS’05).New York:ACM,2005:157-164 [26] Van Der Hoek W,Wooldridge M.Cooperation,knowledge,and time:alternating-time temporal epistemic logic and its applications[J].Studia Logica-An International Journal for Symbolic Logic-SLOGICA,2003,75(1):125-157 [27] Buttyan L,Hubanux J.Toward a formal model of fair ex-change——a game theoretic approach[R].Switzerland:Swiss Federal Institute of Technology,2000 [28] Canetti R,Rosen A.Cryptography and Game Theory[M/OL].2009.http://www.cs.tau.ac.il/~canetti/f09-cgt.html [29] 薛瑞,冯登国.安全协议的形式化分析技术与方法[J].计算机学报,2006,29(1):1-20 Xue Rui,Feng Deng-guo.The Approaches and Technologies for Formal Verification of Security Protocols[J].Chinese Journal of Computers,2006,29(1):1-20 [30] 徐亮,余建平.改进的验证正确性ACTL性质的限界模型检测方法[J].计算机科学,2013,40(6A):99-102 Xu Liang,Yu Jian-ping.Improved Bounded Model Checking on Verification of Valid ACTL Properties[J].Computer Science,2013,40(6A):99-102 [31] Jamroga W,Bulling N.A logic for reasoning about rational agents[M]∥Computational Logic in Multi-Agent Systems-CLIMA.Berlin:Springer,2007:42-61 [32] Bulling N,Jamroga W.Rational play and rational beliefs under uncertainty[C]∥8th International Joint Conference on Autonomous Agents&Multiagent Systems/Agent Theories,Architectures,and Languages.2009:257-264 [33] Andreas H,Emiliano L,Dirk W.Logic.Reasoning about Actions Meets Strategic Logics[M]∥Logic,Rationality,and Interaction:4th International Workshop(LORI 2013).Hangzhou,China:Springer Verlag,Tiergartenstrasse 17,Heidelberg,D-69121,Germany,2013:162-175 [34] Nils B,Wojciech J.Comparing variants of strategic ability:how uncertainty and memory influence general properties of games[J].Autonomous Agents and Multi-Agent Systems,2014,28(3):474-518 |
No related articles found! |
|