1、理集合可以推导出缈缈表示矿为定理，亦即由公理本身可以推导出缈因此，上述推理规则表示如果妒是定理，且妒蕴涵，则妒也是定理公理集合中的个公理分别为连接公理，如果既能够证明公式工又能够证明公式，则能够证明公式蕴涵公理，如果彳能够证明公式，且公式蕴涵公式，则能够证明公式签名公理汩置，如果彳拥有用。签名的消息，且能够证明可以用于验证的身份，则么能够证明占对消息负责管辖公理如果彳能够证明丑对公式具有管辖权，且彳能够证明曰对公式负责，则能够证明公式成立密文理解公理如果彳能够证明曰对密文消息切。负责，且爿能够证明对对称密钥负责，则能够证明对消息负责拥有公理彳，押如果彳，女，获得彳，朋二，并用的公开密钥。校验爿签名的有效。
2、>价于下述命题成立∈当且仅当∈。已知∈饼，现考查晓由于晓，且，聊徊，珊盖盎仨晓，因此童谚不成立所以，在信道不可靠的条件下，本协议是非公平的协议分析的例子之二协议以下是协议它可以用于在信道不可靠的条件下签订电子合同。其中。是向发送的消息是彳随机生成的密钥是用加密的加密消息表示向发送消息的承诺是彳提交密钥的证据是确认已经交付密钥的证据是协议中唯的标记，表示这个协议回合中交换的消息是在协议的第步向曰发送与第步，向发送第步向发送与这里Ⅸ是明文传送的，因此，有可能在得到之前获得消息为保证协议的公平性，协议假设彳与之间的通信信道是可恢复的亦即，不可能永远阻止收到彳发送的消息收到消息之后，生成，并在其目录上公布证据，供。
3、了与的致性验证注意，公理卅可用于建立主体的拥有集合因篇幅所限，本文省略了它们的应用应用本文提出的方法，可以分析范围很广的电子商务协议，例如中的些协议近年来，对于公平交换协议，提出了些新的概念例如，对公平性提出了时效性不可滥用性等要求为了减少可信第三方的参与，提出了乐观公平交换协议等全面分析这些复杂的协议，需要应用更为复杂的形式化工具。例如我们提出的种新方法尽管如此，本文提出的方法仍然具有简单实用应用广泛等特点特别地，在设计复杂协议时，可以首先应用本方法分析和检查协议的各种安全性质电子商务协议形式化分析摘要提出了种新颖的形式化方法，可以用于分析电子商务协议的安全性质，例如可追究性和公平性与以前的工作相比较。
4、们得到协议理解假设去掉冗余性以后，协议的第和第步如下，第步与第步不变我们将对修改后的协议进行形式化分析第步，第步彳彳，办∽丘聊碌可追究性分析列举可追究性目标聊分析与的设计是否符合可追究性要求假定∈成立，即，曰∈由，埘，与可得彳聊假定∈口成立，即彳，聊巧∈嗣∈口由，办与可得聊由，肋，与可得，坍由上式。与可得将发送给曰由上式，与可得将发送给由上式，与可得脚由式，与可得，矗沏由上式，与可得，肌由上式，式与可得聊，办脚由上式，式与可得聊，矗由上式，与可得∞因此，改进后的协议的与的设计满足可追究性要求分析协议是否达到可追究性目标因为，饼，谚我们有∈讲∈和∈∈见因此，协议达到可追究性目标公平性分析协议达到公平性目标。
5、析方法，扩展了信念逻辑的分析范围，可以用于分析电子商务协议的可追究性虽然逻辑仍然是形式化分析电子商务协议的主要工具之，但是，逻辑也有些不足之处对逻辑进行改进，提出了种新的逻辑分析方法，可以同时分析电子商务协议的可追究性与公平性本文提出了种新颖的电子商务协议形式化分析方法，与其他相关工作相比较，该方法的特点是以公理系统为基础，由个推理规则和个公理组成对协议主体的拥有集合给出了形式化定义将协议的初始状态假设细粒度化，将它们分为类基本假设可信假设与协议理解假设，避免因非形式化的初始假设而产生的分析对的信任程度进行细粒度的形式化规范，揭示协议的内涵分析步骤与过程简明清晰新的形式化分析方法本文作了如下基本假设通信。
6、最后，通过由口，芷。获得的计算摘要矗朋，并与，聊置中的肌进行比较如果二者致，则断定叫希望发送给的邮件内容为，且愿意接收在这种情形下，向发送消息，亦即发送邮件的非否认证据彳，聊同时，向发送消息，亦即向递交邮件的非否认证据，埘聊。协议的分析分析前，我们引入谓词，用于校验任意消息与其摘要矗所的致性，亦即，厅肌当且仅当对应用单向散列函数时，其结果为∞协议的分析过程如下协议分析准备列出初始拥有集合铹巧，。印诺，巧列出初始状态假设集合基本假设，民，。∞可信假设爿，将发送给柳将发送给矗埘协议理解假设将发送给埘，小，将发送给列举与我们注意到，协议的与的设计存在冗余事实上，令，埘而埘Ⅳ，占，嗣即可满足要求根据以上分析，我。
7、体处取到朋在下列两种情形下，主体可以主动从主体处取到通过次或多次伽操作从主体取得消息这基于励的方法是和提出来的，即在通信信道不可靠的条件下，主体通过多次向进行助操作获取他所需要的消息，以弥补通信信道的不可靠性当任意主体曰公开消息时可以从处取到注意，这里公开也有两种情形任意主体向公众公开消息协议主体仅向参与协议的主体公开消息协议主体的拥有集合假设协议由条语句组成为参与协议的任意主体协议开始时，主体的初始拥有集合为锘协议执行第步后的拥有集合为晓此外，我们将Ⅱ钟记为彳的最终拥有集合当协议运行步后的拥有集合包含其上步的拥有集合和爿在本回合接收和发送的消息随着协议的继续运行，主体的拥有集合单调增加，直至晓圭饼时为。
8、公众进行只读访问第步与第步声和彳分别从处取到证据协议的分析梗概受篇幅所限，本文仅给出该协议的分析梗概首先，引入谓词如下埘当且仅当对密文消息应用对称密钥解密时，其结果为明文消息协议的可信假设是彳，聊协议理解假设是公布，公布该协议的与是通过类似于第节中的分析，不难证明协议的与的设计满足可追究性要求么埘旧埘并且，协议达到可追究性目标此外，由于可恢复信道的假设，不难证明该协议也满足公平性的要求结论通过上述分析，可以发现些协议的冗余性，并揭示了协议的些内涵为了保证协议的可追究性与公平性，在协议中，必须做到将发送给曰，并在发送前检查与矗的致性类似地，在协议中，必须做到公布证据声明负责的密钥是提交的密钥并且对该密钥进。
9、为，或者，且正町，则晓其余情形，晓订逻辑构件我们的方法包含以下个逻辑构件对于任何主体曰可以通过执行系列操作，使相信公式，且不向曰泄漏任何秘密≠爿声明对公式以及所有蕴涵的公式负责在分析过程中，下述蕴涵式成立亦即，如果彳声明对公式∥负责，则彳声明对公式负责彳对公式具有管辖权，即参与协议的主体都相信所声明的公式是正确的拥有消息收到消息在分析过程中，下述蕴涵式成立聊，行，亦即，如果彳收到则收到，是的公开密钥，用于验证彳用签名的消息爿主动取到消息彳在协议回合中新生成消息公理系统我们的公理系统由个推理规则和个公理组成推理规则如下卜妒卜妒妒上述推理规则说明，由伊和卜妒可以得到少这里，是元语言符号妒表示由公式集合以及公。
10、的形式化工具应运而生，其中逻辑方法与类逻辑方法最为着名类逻辑是种模态逻辑，通过主体信念集合的演化推断认证协议的正确性与安全性电子商务协议比认证协议更为复杂，它不仅需要满足认证协议的安全需求，还需要考虑认证协议中未涉及到的若干安全性质，其中最重要的是可追究性与公平性所谓可追究性，是指协议主体应当对自己的行为负责，在发生交易纠纷时，主体可以提供必要的证据以保护自身的利益所谓公平性，是指协议在运行的任何步终止时，参与协议的主体都处于同等的地位，任何方都不占据优势逻辑不能分析电子商务协议的可追究性，因为它用于证明主体相信个公式相反，证明可追究性，则需要向第三方证明另个主体对个公式负有责任因此，提出了种新的逻辑分。
11、止下面给出主体的拥有集合的形式化定义为此，我们需要可构造消息集合这概念定义可构造消息设为消息，为消息集合称是由可构造的，记为叁当且仅当∈肌，∈∈，∈，。乏∈。舍其中，厂是元记号，表示实际上可计算的任意函数定义可构造消息集合设为消息，为消息集合称为的可构造消息集合，当且仅当删童定义主体爿的拥有集合假设协议由胛条语句组成主体的拥有集合晓，门是晓的可构造消息集合晓为行文简捷起见，以下除特别强调之外，我们不区分晓与晓，而是将晓理解为晓当协议由第卜步执行到第步时，主体的拥有集合由晓叫到晓，的改变，遵循以下规则如果协议的第条语句为彳斗曰，为彳新生成的消息，亦即萑三，则三町如果不是新生成的消息，则有叁如果协议的第条语。
12、，主要贡献在于对协议主体的拥有集合给出了形式化定义，且主体的初始拥有集合只依赖于环境将协议的初始状态假设集合分为类基本假设集合可信假设集合和协议理解假设集合，避免了因非形式化的初始假设而产生的分析对可信假设作细粒度的形式化规范，揭示协议的内涵建立公理系统，使新方法更为严格与合理关键词形式化分析电子商务协议可追究性公平性可信第三方近年来，电子商务的交易量迅猛增加，因而电子交易的安全性问题日益受到重视除公开密钥基础设施是保障电子商务安全的重要工具之外，安全的电子商务协议是安全地进行电子交易的基础以往，安全协议的研究重点是认证协议认证协议的设计是个众所周知的难题，常因些细微的问题产生安全缺陷为此，些分析认证协。
参考资料：
1、该文档不包含其他附件(如表格、图纸)，本站只保证下载后内容跟在线阅读一样，不确保内容完整性，请务必认真阅读。
2、有的文档阅读时显示本站（www.woc88.com）水印的，下载后是没有本站水印的（仅在线阅读显示），请放心下载。
3、除PDF格式下载后需转换成word才能编辑，其他下载后均可以随意编辑、修改、打印。
4、有的标题标有”最新”、多篇，实质内容并不相符，下载内容以在线阅读为准，请认真阅读全文再下载。
5、该文档为会员上传，下载所得收益全部归上传者所有，若您对文档版权有异议，可联系客服认领，既往收入全部归您。
电子商务协议形式化分析
