《电子支付协议是一种特殊的安全协议》由会员分享，可在线阅读，更多相关《电子支付协议是一种特殊的安全协议（14页珍藏版）》请在金锄头文库上搜索。
1、电子支付协议是一种特殊的安全协议，利用形式化方法进行电子支付协议分析是电子支付研究的一个重要方面。电子支付协议结构较认证协议远为复杂， 协议执行不一定是顺序结构， 有时含有条件分支或循环等非顺序执行。一个电子交易协议还可能是若干子协议的复合体。因此，电子支付协议的形式化分析迥异于认证协议，而有其自身特色，需要对形式逻辑进行扩展。目前，安全协议的形式化分析的研究多集中于对认证协议的分析，对电子支付协议的分析则较少。1983 年， Dolev 和 Yao 发表了安全协议发展史上的一篇重要的论文94，将安全协议本身与安全协议所具体采用的密码系统分开，在假定密码系统是“完善”的基础上讨论安全协议本身的
2、正确性、安全性、冗余性等课题；该论文还基于代数模型理论首次建立了攻击者模型。Burrows， Abadi 和 Needham 提出的 BAN 模态逻辑方法95由一些命题和推理规则组成，命题表示主体对消息的知识或者信念，应用推理规则可以从已知的知识和信念推导出新的知识和信念规则。BAN 逻辑假设认证是完整性和新鲜性的函数，使用规则推导协议运行中的属性。BAN 逻辑具有概念清晰、简单、易理解、易应用的特点，可以发现协议中不易察觉的漏洞。R. Kailar 针对 BAN 逻辑不适宜分析电子商务协议的缺陷，提出了一种用于分析要求“责任性”的安全协议的新框架Kailar 逻辑96,97，用于分析电子商务
3、协议的可追究性。Kailar 逻辑着重强调进行电子商务的双方对对方的责任性，即对自己所发的消息的不可否认性。Kailar 逻辑分析电子商务协议比 BAN 逻辑更加自然，但是它对参与方进行初始化假设仍然是非形式化的，而且不能分析协议的公平性，缺乏对签名密文的分析机制。1994 年，Peter Ryan 提出使用 CSP（Communicate Sequence Process）语言和模型检测工具 FDR（Failure Detect Refination）来分析协议98。基于进程代数的模型检测方法 CSP 试图检测或构造协议可能存在的攻击集合， 建立一个运行协议的有限状态系统模型，然后使用状态检
4、测工具 FDR 进行协议安全性分析。状态检测工具需要搜索所有可能的状态： 定义一个状态空间，对该空间进行搜索以判定空间中是否存在攻击者成功攻击协议的攻击路径。FDR 是一个通用工具，其输入是两个 CSP 进程：说明进程和实现进程，然后检测实现进程是否是说明进程的提练(Refinement)。Lowe 在 1996 年使用这样的方法，发现了 NSPK 协议存在的中间人攻击。 N. Heintze等和S. Schneider等分别利用CSP逻辑成功地对 NetBill系统和 DigiCash 系统进行原子性分析99, 100。美国国家海军研究中心的 Meadow等人开发的NRL 协议分析器101是
5、一个有效的安全协议验证工具，使用 Prolog 语言编写，既可以验证安全协议的安全特性，又可以检测协议的漏洞。NRL 采用了 Dolev-Yao 的项重写规则模型。NRL协议分析器可以在多轮协议实例运行的情况下使用后向搜索策略以构造一条从不安全状态到达初始状态的路径，因此可以工作在无限状态空间中。NRL 已经成功的发现了一些安全协议中未知和已知的漏洞102, 103,104。 但是这个工具也存在一个缺陷：需要大量的约化假设以约简状态空间，当使用不断增长的规则集合表达更复杂的算法时，无法清晰的描述什么样的系统规模才够好，而且，NRL 还需要手工推导一些不可达的状态。 在国内，怀进鹏、李先贤提出了
6、一个新的密码代数模型105，并研究了密码协议的一致性问题， 给出了密码协议设计的一般性原则。卿斯汉等对安全协议和不可否认逻辑进行了大量研究106,107,108,109，卿斯汉等分析了Kailar逻辑的缺陷110，对Kailar逻辑进行了改进，并提出了一种新的不可否认逻辑111，给出了类似Kailar逻辑的一系列定义和推理规则，弥补了Kailar逻辑的一些缺陷，使之能够分析电子商务协议的可追究性和公平性。白硕等112,113从通信安全问题具有动态性和非单调性的角度出发，引入非单调逻辑的机制，通过基于“一阶逻辑 +动态逻辑 +非单调逻辑”的公理和推理规则，利用“失败即否定”等原则作为演绎推理的补
7、充， 来验证安全协议的非单调性质， 并用提出的非单调动态逻辑系统 NDL分析电子商务交易协议，已对SET的一部分业务流程成功地进行了NDL验证。J. D. Guttman 和F.J. Thayer Fabrega 等基于消息代数理论，提出新一代安全协议分析方法串空间理论114,115,116,117,118,119,120，结合了 NRL 协议分析器、CSP模型检测技术以及 Paulson 的归纳证明的思想。串空间逻辑简洁易用，而且该方法基于图论，使得分析者可以方便的使用图结构描述协议、攻击、正确性定理和证明中的一些关键步骤。 串空间理论使用”串”的概念描述协议的参与方发送消息和接收消息的行为
8、，不同协议参与方的串组成串空间，表示协议的运行，串空间运行于代数结构上。 消息代数定义了串空间的数据结构， 以及数据项之间的关系。串空间技术给安全协议的形式化分析注入了新的活力。串空间逻辑及其扩展串空间逻辑及其扩展串空间逻辑及其扩展串空间逻辑及其扩展Thayer，Herzog 和Guttman提出了串空间(Strand Space)模型114,115,116，这是一种结合定理证明和协议迹的混合方法。事实证明，串空间模型是分析安全协议的一种实用、直观和严格的形式化方法。串空间理论使用 “串” 的概念描述协议的参与方发送消息和接收消息的行为，不同协议参与方的串组成串空间，表示协议的运行，串空间运行
9、于代数结构上，即消息代数。消息代数定义了串空间的数据结构，以及数据项之间的关系。原始的串空间理论设计用于认证协议的形式化分析， 描述对象和操作类型涉及面较窄。因此，需要根据具体分析目标的进行适当的扩展。1 1 1 1. . . .消息代数消息代数消息代数消息代数原始的消息代数中只包含了原子项、连接项和密文项的描述114,116，我们需要在模型中加入了对散列操作、签名操作以及加密解密等操作的描述，因此也相应的需要加入一些新的数据集合。定义定义定义定义 1 1 1 1 设 A A A A 表示协议的参与者交换的全部消息的集合，称为项空间，A A A A 中的元素称为项，其元素是由下述集合生成：T
10、T T T：协议中的原子项；K K K K：协议使用的密钥项。其中 K K K K，T T T T 两两不相交。在消息空间 A A A A 上的操作包括：加密运算encr：K K K K A A A A A A A A解密运算decr：K K K K A A A A A A A A连接运算join：A A A A A A A A A A A AHASH 运算hash: A A A A A A A A签名运算sign: K K K KA A A A A A A A密钥映射key: A A A A K K K KkK K K K 的逆密钥表示为k-1。对于a,b,mA A A A，kK K K K
11、，我们将encr(k,m)操作表示为mk, 将decr(k,m)操作表示为mk-1, 将join(a,b)表示为(a,b) 或者a b，将hash(a)表示为H(a)， Hash 值的集合称为散列值空间 H H H H； 将sign(k,m)表示为mk。我们将形如mk、H(m)，mk的项称为 A A A A 上的操作项，将 T T T TK K K K 中的项称为原子项，原子项和操作项统称为简单项，使用连接操作的项称为连接项。定义定义定义定义 2 2 2 2 对于项h，g，g，g“A A A A，kK K K K，h称为g的子项，记为hg，如果有：(1)h，g T T T TK K K K 且
12、h=g；(2) 如果g= (g，g“) ，且hg 或hg“ 或h=g；(3) 如果g= gk，且hg或h=g。其中，满足条件(1)、(2)的子项称为明文子项。显然，子项关系是一种传递、自反的关系。在这个项代数的结构上，协议参与者的行为表示发送或接收这些消息项的一个有限动作序列，即一个串s表示为： (， ， )。 其中称为一个有符号项，i+，(1in)分别表示发送和接收，aiA A A A(1in)） ，相应的ai称为无符号项。(A A A A)*表示有符号项的有限序列集，(，)(A A A A)*。协议参与方包括合法方和入侵者，相应的串也分为正常串和入侵串，这些串构成了串空间。2.2.2.2.
13、串空间和丛串空间和丛串空间和丛串空间和丛定义定义定义定义 3 3 3 3令 A A A A 是给定的项空间， A A A A 上的串空间定义为一个具有迹tr的集合，满足tr: (A A A A)*。定义定义定义定义 4 4 4 4给定串空间，以及s，(1) 是 串 上 的 节 点 ， 其 中i表 示 节 点 在s中 的 序 号(1iheight(tr(s)，height(tr(s)表示串s的迹长度)。所有的节点集合表示为N。(2) 对于nN，term(n) = (tr(s)i表示串s上的第i个有符号项，uns_term(n)=(tr(s)i)2表示串s上的第i个无符号项。(3) 对于n1，n2
14、N，n1，n2上存在边n1n2， 当且仅当term(n1) = +a， 且term(n2)= a，其中aA A A A，表示n1先于n2发生，且n1发送的消息被n2接收到。(4) 对于n1，n2N，如果n1=(s，i)，n2=(s，i+1)，则存在边n1n2，表示在串s上，节点n1发生后，n2马上发生了。使用n1+n2表示n1先于n2发生（可能不是马上发生） 。(5) 项t出现于节点n，当且仅当tterm(n)。(6) 假设I是一个无符号项集合，节点n是I的入口点，当且仅当term(n)=+t(tI)，且对于任何满足n+n的n，有uns_term(n)I。(7) 无符号项t源于节点n，当且仅当
15、n是集合I= t:tt的入口点。无符号项t是唯一源于项，当且仅当t源于唯一的节点n。定义 4 中定义了节点集合和节点上存在的两个边关系，这样串空间的基本结构可以表示为一个直连图(N，()。在这个图结构上，就可以形式化描述协议运行的情况。定义定义定义定义 5 5 5 5 已知节点集合N及其上的边构成的图(N，()，假设有NBN，B，B，且B= (NB，(BB)是(N，()的子图，如果B满足：(1)B是有限的；(2) 如果n2NB， 且term(n2)的符号是负的， 则存在唯一的节点n1满足n1Bn2；(3) 如果n2NB，且n1Bn2，则有n1NB；(4)B不是有环的；则称B是一个丛（Bundl
16、e） 。如果n属于丛B的节点集合，则称节点n在丛上，简记为nB；如果串s上的节点都在B的节点集上，则称串s在丛B上，简记为sB。丛是多个节点通过边关系和连接而成的单向图。串s在丛B中的高度即是满足B的最大的i，表示为B-height(s)。串s在B上的迹表示为B-trace(s)=，其中m=B-height(s)定义定义定义定义 6 6 6 6 令D是一个边集合，即D ()， ，则称D是D的传递闭包，D是D的传递自反闭包。对于丛B上的边集合，我们使用B和B表示其上边集合的传递闭包和传递自反闭包。这样我们可以得到以下一些引理。引理引理引理引理 1 1 1 1 假设B是一个丛，则B是一个自反、非对称、传递关系，即一个偏序。B的节点集的
