《公平交换协议的理性模型及其形式化分析-丁洪.docx》由会员分享，可在线阅读，更多相关《公平交换协议的理性模型及其形式化分析-丁洪.docx（69页珍藏版）》请在taowenge.com淘文阁网|工程机械CAD图纸|机械工程制图|CAD装配图下载|SolidWorks_CaTia_CAD_UG_PROE_设计图分享下载上搜索。
1、分类号 ： _T! - 密 级 : 论文编号： 2013021001 _ 贵州大学 2016届硕士研究生学位论文 公平交换协议的理性模型及其形式化分 析 学科专业： 应用数学 研究方向： 密码学理论与工程 导 师： 彭 长 根 教 授 研究生：丁洪 中国贵州贵阳 2016年 5月 目录 目录 . I 摘要 . III Abstract . IV 第 1章绪论 . 1 1.1研究目的及意义 . 1 1.2国内外研究现状及水平 . 3 1.2.1理性交换及其公平性 . 3 1.2.2信誉机制与理性密码学的结合 . 4 1.2.3基于博弈逻辑的形式化分析方法 . 5 1.3主要研究工作 . 6 1.
2、4论文翻结构 . 7 第二章基础知识 . 9 2.1博弈论相关知识 . 9 2.1.1博弈基础概念及纳什均衡定理 . 9 2.1.2混合策略博弈与駿博弈 . 10 2.1.3动态博弈模型 . 11 2.2信息论相关知识 . 12 2.3博弈逻辑 一 ATL . 12 2.4小结 . 15 第三章混合策略下的理性交换协议模型 . 16 3.1理性交换协议的混合策略模型 . 16 3.2 !种新的理性交换协议 . 18 3.3理性交换协议的分析 . 19 3.3.1正确性 . 19 3.3.2可追究性 . 20 3.3.3公平性 . 22 3.4实例分析 . 26 3.5小结 . 26 第四章信誉
3、机制下的理性交换协议模型 . 28 4.1面向理性交换的信誉机制 . 28 4.1.1信誉设计 . 28 4.1.2效用模型 . 30 4.2 基于信誉机制的理性交换协议模型 . 31 4.3信誉机制下 Syverson协议的改进 . 33 4.4实例分析 . 37 4.5小结 . 39 第五章基于博弈逻辑的理性交换协议形式化分析 . 41 5.1博弈逻辑的改进 . 41 5.1.1混合并行认知博弈结构 mCEGS . 41 5.1.2混合并行认知博弈结构的语法和语义 . 43 5.1.3 mATEL与扩展式混合策略博弈 . 45 5.2基于博弈逻辑的理性交换协议形式化模型 . 47 5.3理
4、性交换协议形式化分析 . 49 5.3.1混合策略下理性交换协议的形式化分析 . 49 5.3.2信誉机制下理性交换协议的形式化分析 . 52 5.4小结 . 55 第六章结束语 . 56 6.1主要研究工作总结 . 56 6.2展望 . 57 致谢 . 58 参考文献 . 59 附录：作者在攻读硕士学位期间发表的学术论文及参加的科研项目 . 62 图版 . 63 原仓 1J性声明 . 64 公平交换协议的理性模型及其形式化分析 摘要 在电子商务或网络应用环境中，参与者具有理性特征（称为理性参与者）。通过在 传统的交换协议中引入理性参与者，理性交换协议已经引起过内外学者的关注，是密码 学和博弈
5、论两大学科交叉形成的研宄热点。考虑参与者的自利性，在博弈论基础上建立 公平交换协议的理性模型，约束参与者选择预定的行为，设计理性公平交换协议，具有 重要研宄意义。形式化分析方法是分析密码协议较为有效的一种方法，对所设计的理性 公平交换协议进行形式化分析，显得尤为必要。本文主要研宄内容有： (1) 应用扩展式博弈混合策略理论对交换协议进行建模，并引入熵函数对交换协议 的过程公平性进行描述；在保证过程公平性原则下运用混合策略纳什均衡概念形式化定 义理性公平性，在此模型基础上构造一个新的理性交换协议。 (2) 将参与者的信誉作为其长远利益，并构造恰当的效用函数去描述参与者的收 益；基于重复博弈建立信
6、誉机制下的理性交换协议模型，运用重复博弈的纳什均衡理论 给出了理性公平性的定义；并基于此模型对 Syverson协议进行改进。 (3) 在并行认知博弈结构 (CEGS)的基础上引入混合策略、期望效用和偏好，得到 新的并行认知博弈结构 mCEGS， 提出可以描述混合策略下的理性交换协议的博弈逻辑 mATEL;运用 mATEL形式化定义混合策略理性交换协议；基于 mCEGS的等价扩展式 博弈，对混合策略下的理性交换协议进行形式化分析。 关键词：理性交换，公平性，期望均衡，信誉机制，博弈逻辑 中图分类号： TP309 文献标识符 ： A Rational model of fair exchange
7、 protocol and its formal analysis Abstract In e-commerce or online application environment, participants have the rational characteristics (these participants have been called rational participants). Rational exchange protocol gradually cause the attention of scholars both in the domestic and intern
8、ational by introducing the rational participants in the traditional exchange protocol, becoming the hot topic which comes from the crossing subject of cryptography and game theory. It has important research significance that considering the participants5 self-interest, establishing a rational exchan
9、ge protocol based on game theory and constraint participants choice behavior. Formal analysis is an kind of effective method to analysis the cryptographic protocols through that it is necessary to analyze rational fair exchange protocol. In this paper, the main research work is as follows: Exchange
10、protocol has modeled by extensive mixed strategy game and the entropy function has introduced to discuss the fairness in the process of exchange. In addition, the rational fairness has formally defined by using the concept of mixed strategy Nash equilibrium under the principle of the fairness in the
11、 process, and on the basis of this model to construct a new rational exchange protocol. (2) The reputation of the participants as its long-term interests, and constructs the appropriate utility function to describe the participants benefits. On the other hand, the rational exchange protocol model un
12、der the reputation mechanism has established that based on repeated game, and the rational fairness has formally defined by using the concept of repeated game theory ofNash equilibrium. (3) ATL can analyze and verify the fairness of the traditional security protocol. But considering the participants
13、5 self-interest, ATL can5t formally analyze cryptographic protocols. So by adding mixed strategy, utility and the preference in CEGS, we put forward mATEL and give the formal definition of mixed strategy rational exchange protocol. Finally, a formal analysis of the protocol is given with the mATEL.
14、Key words: rational exchange, fairness, expectations equilibrium, reputation mechanism, game logic 第一章绪论 据统计，中国近年来电子商务增长速度受全球经济的影响有所回落，但年均交易规 模达数万亿元。从发展趋势来看，电子商务的外延在不断扩大，电子商务是未来市场的 重要补充力量。网络和电子商务的广泛应用给人们的工作和生活带来了极大的方便，安 全的电子商务协议是保证电子商务活动正常开展的基石，而交换协议是电子商务协议中 很重要的一类。为了电子商务协议能安全公平的进行，恰当的机制设计，能很好的驱使 参与
15、者遵守协议从而成功的完成交换。根据理性参与者自利性的特点，在协议交换过程 中不需可信第三方的参与，理性交换协议削弱了可信第三方的权利。 在本章中，主要介绍本文的研究目的及意义，同时介绍理性交换及其公平性、信誉 机制以及形式化分析的研究现状及水平，最后给出论文的组织结构。 1.1研究目的及意义 随着信息技术作为工具被引入商贸活动，电子技术和电子商务应运而生。随后电子 政务、电子商务等应用的蓬勃发展，特别是密码学被广泛应用于国际互联网之后，对电 子商务协议的研宄越来越深入。传统密码学通常仅研宄诚实参与者和恶意参与者的行 为，而在实际生产生活中，往往参与者都是理性的（其通常期望最大化自身的利益），
16、这也促使了理性密码学 （ Rational Cryptography )的出现。 在传统交换协议中引入理性参与者，理性交换协议逐步引起国内外学者的关注，成 为由密码学和博弈论两大学科交叉形 成的研宄热点。在研宄理性交换协议执行的过程 中，不可避免的需要研宄理性协议的公平性，针对交换协议的公平性问题，现有的研宄 主要是依赖于两种方法来解决这个问题：一个是公平交换的原则，即保证在公平交换协 议执行的整个过程中，诚实的参与者不会遭受任何损失；另一个是理性交换的原则，即 保证理性参与者不会因不诚实行为而获得更多的其他利益。尽管公平交换协议的公平性 保证要强于理性交换协议，但其需要花费比较大的代价，如：
17、需以可信第三方或非常复 杂的通信为代价。理性交换协议被认为是真公平性与复杂性的一个平衡，也因此在某些 特定的应用中，理性交换协议能提供更合适的解决交换问题的方法。用博弈论中纳什均 衡的相关概念对理性交换进行形式化定义，基于博弈论中的逆向归纳法、动态博弈、纳 什均衡、序贯均衡、机制设计等理论对理性交换进研宄，国内外对理性交换的公平性研 宄已有一些成果1-9。博弈论中的混合策略是呈概率分布的，信息论中的信息熵可以对不 确定性的事物进行度量。目前已有的研宄中，主要是用博弈论中的一些工具对理性交换 协议进行分析。 在对密码协议的研宄中，对交换协议的建模与形式化分析非常 重要。在现有的研宄 中，主要利用
18、博弈论中的均衡理论从理性角度给出理性公平性的形式化定义，但其公平 性的含义基本上只考虑结果的瞬时公平性，很少考虑长远公平性或过程公平性。运用信 息熵对交互过程中的不确定性进行描述，运用带熵博弈论来描述和设计具有公平性质的 密码协议，通过从过程公平的角度设计合理的均衡博弈模型，进一步研宄理性交换协议 的公平性，可为公平交换协议研宄提供一种新的思路，也为密码学基础协议的公平性研 宄提供了新方法。 信誉是对于一个交易者过去行为及未来前景的知觉表现，已被广泛应用于电子商 务、 P2P网 络、网格计算和医疗咨询等各大领域。信誉机制是在电子市场中用于产生和 传播信誉信息的一种工具，可以对交易双方的行为产生
19、约束，降低交易风险，提高交易 成交率，降低交易成本。理性的交易者在合理的信誉机制下，会采取诚信的交易行为， 最大化自己的长期利益，这与理性交换协议中的理性参与者不谋而合。从这个意义上说， 基于信誉机制的理性交换协议研宄具有重要的科学意义。 博弈逻辑 10， n， 12是博弈论和逻辑学相交叉的一个新的研宄领域，博弈逻辑研宄理性 参与者在行为互动过程中的推理过程，因此以博弈逻辑为基础，应用 ATL对理 性交换 议进行形式化分析，对博弈逻辑的发展具有深远的意义，为理性交换协议的形式化分析 提供一种新的形式化分析方法。避免传统形式化分析方法的不足，在设计理性交换协议 时，密码协议的设计难免会有缺陷，因
20、此，应用 ATL形式化分析理性交换协议，为设 计高效、安全和公平的理性交换协议提供保障。 随着计算机网络的迅速发展，电子商务活动越来越受追捧，人们在享受互联网带来 的高效、快捷、便利交易的同时，也希望能以最小的代价最大化自己的利益，最终实现 公平交换。研宄公平交换协议的理性模型并进行形式化分析对电子商务的发展和应用具 有重要的理论指导意义。 1.2国内外研究现状及水平 密码学和博弈论都是关心有潜在利益冲突的互不信任的参与者之间的交互协议。密 码学通常采用最坏情况的观点，密码协议旨在针对有任意（恶意 ） 行为的参与者，保护 每一方的利益。博弈论是研宄多人谋略和决策问题的理论，从博弈论的观点来看参
21、与者 都是理性的，博弈协议是为了防范其他理性参与方偏离协议。理性密码学是一个新兴的 研宄领域 ， 2004年 ， Halpern和Teague8首次提出了理性秘密共享 (Rational Secret Sharing ) 和理性安全多方计算 （ Rational Secure Multiparty Computation)的概念，基于博弈论中 的工具和思想来分析密码学，对理性密码学的研宄产生了极大的影响。传统的密码协议 是假定诚实的参与者是执行协议，恶意的参与者则不执行协议或破坏协议。博弈论的观 点是应该用理性（最大化自身利益）参与者来代替诚实或恶意参与者。近年来，博弈论 与密码学结合的理性密
22、码学研宄取得了一些研宄成果 8,9，理性密码共享的文章有 13,14。 1.2.1理性交换及其公平性 传统公平交换协议通常仅研宄诚实参与者和恶意参与者的行为，而在实际生产生活 中，参与者往往都是理性的（其通常期望自身利益的最大化），这也促使了理性交换 (Rational Exchange)的出现。 1998年 Asokan15在欧洲密码学会上首先将博弈论应用到 公平交换协议的分析设计中，给出了一个两方参与者以公平的方式在网络上相互交换数 字签名的协议。在公平交换协议中是依靠可信第三方来保证真公平性，此外，随着自组 织网络 （ Adhoc)和 P2P网络等的广泛应用，由于这些网络系统没有固定的基
23、础设施， 即参与者所处的环境不固定，因此无法假设可信第三方的存在对这些新的计算模式提出 了新的挑战。频繁和不可预知的断开网络导致不能及时访问节点（可信第三方），这样 使得 TTP能在这样的网络环境中用来保证公平性变得不现实。另一方面，在一些特定应 用（如小额支付 ） 公平交换协议中，依靠 TTP去保证公平性所需的代价高于交换协议本 身的价值。为了满足效率的要求就要牺牲公平性，因此理性交换很适用于这种环境下， 不需要可信第三方的参与。理性交换的概念是 Syverson在 1998年首次提出的，他利用 一种称作弱秘密位承诺的密码技术设计了一个与公平交换协议类似的交换协议。在公平 交换协议领域的研宄
24、已经较为深入，而理性交换逐渐引起国内外学者的关注。 随着理性交换研宄的逐渐深入，理性交换有一个较一致的定义：理性交换即是理性 交换协议保证理性参与者不会因不诚实行为而获得任何利益，但不能保证诚实参与者不 会因其他参与者的不诚实行为而不遭受损失。目前，对于理性交换的形式化研宄主要在 Buttyan和 Alcaide为首的两个学术团队中展开。 Syverson与 1998年对理性交换协议进 行形式化分析 16，设计了一个与公平交换协议类似的交换协议，它并不提供真公平性， 但能保证理性或自利性参与者没有任何理由不遵守此协议，这也意味着欺骗发生的概率 极小，故称理性交换协议。 Buttyan与 200
25、1年用博弈论的方法形式化分析公平性 17，并 研宄公平交换与理性交换的关系，对交换协议进行建模并进一步分析交换协议的性质及 具体的 Syverson协议 18。 Alcaide等人分析了 Syverson理性交换协议的不足并对其进行 改进 4，用动态博弈中的扩展式博弈 1，贝叶斯博弈等对理性交换协议进行了建模 19， 并用元启发式搜索技术进一步研宄多方的理性交换协议 2,3。近年来，随着自组织网络 (Adhoc)、 P2P网络的广泛应用于发展，理性公平交换成为研宄热点。 理性交换协议被认为是真公平性与复杂性的一个平衡，也因此在某些特定应用中， 理性交换协议能提供更合适的解决交换问题的方法。理性
26、交换的非形式化定义与动态博 弈中纳什均衡的概念非常类似，协议本身被描述成一组策略集合 （ 一个策略属于一个协 议参与者 ）， 错误行动即是协议参与 者执行的策略与预定应执行的策略不一致的行动结 果。用博弈论中的相关工具如基于博弈论中的逆向归纳法、动态博弈、纳什均衡、序贯 均衡、机制设计等理论来设计并分析理性交换协议已有一些研宄成果 20,21。 1.2.2信誉机制与理性密码学的结合 在人类社会中，信任 (Trust)和信誉 (Repution)起到了非常重要的作用，早已在社会学、 经济学、管理学等各大领域中受到人们的关注 22。信任是一个参与者对另一个参与者未 来行为的个人期望，是基于两个参与
27、者现在或未来的交互计算出来的个人数量 23。信誉 也叫作信 任值、信誉度，通常指的是一个参与者对另一个参与者的意图的感觉，是对参 与者过去行为及未来前景的知觉表现。信誉机制 (Raputation Mechanism)是在电子市场 (如网上拍卖和网上交易等 ） 中用于产生和传播信誉信息的一种工具 24。 2004年， Ramchum等 25将信誉机制分为个体层和系统层，体现了信誉机制的研宄内容 。 2005年， Fullam等 26为建立信任问题的通用实验平台提出了信誉机制所应满足的要求。信誉机制 的体系结构分为集中式、分布式和混合式三种。传统对信任有两种观点，一种是认知观 点，一种是数值观点
28、。 2006年， Huynh27证明了在开发式、大规模的系统中采用认知观 4 点解决信任问题并不合适。目前对信誉机制研宄仍受到广大学者的青睐，获得了很好的 成果 28-30。 目前，将信誉机制应用于理性密码学的研宄还比较少。 2008年， Nojoumian等 31 提出了一个新的信任函数，能够去给新的参与者创造机会。 2010年， Nojoumian等 32 提出了社会秘密共享 (Social Secret Sharing, SSS)概念，提出了一个无条件安全的社会秘 密共享方案。 2012年， Nojoumian基于参与者在社会环境中与长期的交互活动，提出了 社会理性秘密 (Social
29、Rational Secret Sharing, SRSS)方案 33，同年，他又进一步探讨了基 于信誉机制的动态密码共享方案和多方承诺方案 34。 Nojoumian的相关工作为理性密码 的研宄注入了新的血液，提供了新的思路。 1.2.3基于博弈逻辑的形式化分析方法 对于传统的安全协议，有很多种形式化分析方法，例如 BAN逻辑、 BAN类逻辑。 但是，这些方法并不适用于理性安全协议的形式化分析，因此需要探索新的形式化分析 方法。 Needhan和 Schroeder35被认为是最早提出形式化分析思想的， 1981年 Dolev和 Yao36用算法分析了两类特殊的协议的安全性，被视为对协议的第
30、一个真正的形式化分 析。 1989年， Burrows37等发表了他们的 BAN逻辑并一起广泛的关注。这类逻辑方法 用于证明协议的不可否认性，但难以分析协议的公平性和时限性。 1993年， Bellar和 Rogaway38提出了著名的 OR(Random Oracle， 随机预言 )模型，这个分析方法证明的公 平性不完全是交换协议中的公平性。在 1997年，对于开放系统， Alur等39,40首次提出 了不同于先行时序逻辑 (Linear-Time Temporal Logic)和分支时序逻辑 (Branching-Time Temporal Logic)的博弈逻辑 ATL， 并且分析 AT
31、L符号检测的复杂度。对于系统和环境的 交替行动博弈过程， ATL提供了可能的博弈结构的选择性路径量词。基于并发博弈结构 CGS， 后被称为 ATL系统，定义了 ATL的语法和语义。 2001年 ,ValentinGoranko41发 现了联合博弈逻辑 （ Coalition Game Logic)与 ATL的相似之处，并且证明了它们的语义 是等价的，在 ATL中嵌入联合逻辑，提出了相应逻辑的公理化系统 .2002年，在文献 42 中 ， R. Alur等运用并发博弈结构来解释 ATL和ATL*， 每个参与者的行动导致并发博弈 结构的状态转换。 2004年， Pierre-YvesSchobbens43在每个参与者给定完全和不完全信 息的情况下，研宄相应 ATL的变式。 2005年，基于 Pauly的联合逻辑，在文献 44中， Valentin Goranko 和 Govert van Drimmelen 提出了 ATL 的完备公理化系统。 2006 年， 5