计算机科学 ›› 2015, Vol. 42 ›› Issue (9): 118-126.doi: 10.11896/j.issn.1002-137X.2015.09.023

• 信息安全 • 上一篇    下一篇

一种理性安全协议的博弈逻辑描述模型

刘海,彭长根,张 弘,任祉静   

  1. 贵州大学理学院 贵阳550025;贵州大学密码学与数据安全研究所 贵阳550025,贵州大学理学院 贵阳550025;贵州大学密码学与数据安全研究所 贵阳550025,贵州大学计算机科学与技术学院 贵阳550025,贵州大学理学院 贵阳550025;贵州大学密码学与数据安全研究所 贵阳550025
  • 出版日期:2018-11-14 发布日期:2018-11-14
  • 基金资助:
    本文受国家自然科学基金项目(61262073,61363068),全国统计科学研究计划项目(2013LZ46),贵州省自然科学基金项目(20092113,20132112),贵州省高层次人才科研条件特助经费项目(TZJF-2008-33)资助

Game Logic Formal Model of Rational Secure Protocol

LIU Hai, PENG Chang-gen, ZHANG Hong and REN Zhi-jing   

  • Online:2018-11-14 Published:2018-11-14

摘要: 博弈逻辑ATL和ATEL可以对传统安全协议的公平性、安全性等性质进行分析与验证。但在理性环境中,由于参与者对知识的自利性,ATL和ATEL都不能形式化分析与验证理性安全协议。因此在CEGS中引入效用函数和偏好关系知识,得到新的rCEGS,并在合作模态算子《Γ》中加入行为ACT参数,提出新的可形式化分析理性安全协议的交替时序认知逻辑rATEL-A。然后运用rATEL-A构建两方理性安全协议的形式化模型,并基于rCEGS的等价扩展式博弈,对具体的两方理性交换协议进行形式化分析,结果表明构建的形式化模型可以有效地形式化分析理性安全协议的正确性、理性安全性和理性公平性。

关键词: ATEL,博弈论,理性安全协议,形式化分析,理性安全性,理性公平性

Abstract: The fairness and security properties of traditional secure protocol can be analyzed and verified by the game logics,alternating-time temporal logic and alternating-time temporal epistemic logic.However,for the formal analysis of rational secure protocol,taking players’ selfishness to knowledge into consideration,ATL and ATEL can not formally analyse and verify rational secure protocol.So by introducing utility function and preference relation in the concurrent epistemic game structure,new concurrent epistemic game structure rCEGS can be gotten.By introducing action ACT parameter in the cooperation modality operator 《Γ》,a novel alternating-time temporal epistemic logic rATEL-A can be gotten that can be used to formally analyse rational secure protocol.Then,rATEL-A was used to construct formal mo-del of two-party rational secure protocol.Based on extensive form game of equivalent to rCEGS,two-party rational exchange protocol was formally analysed,which shows that the formal model can formally analyse correctness,rational security and rational fairness of rational secure protocol effectively.

Key words: Alternating-time temporal epistemic logic(ATEL),Game theory,Rational secure protocol,Formal analysis,Rational security,Rational fairness

[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]∥Lindstrm 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!
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
No Suggested Reading articles found!