安全电子商务交易协议的设计及其形式化分析
2012-10-13黄寄洪甘金明
黄寄洪，甘金明
（梧州学院 计算机科学系，广西 梧州 543002）
所谓安全协议，是在协议中应用加密解密的手段隐藏或获取信息，达到认证以及消息正确发送的目的。运用安全协议，人们可以解决一系列的安全问题，如：对信息源和目标的认证、信息的完整性、时效性等。因此，安全协议是通讯和网络安全体系、分布式系统和电子商务的关键组成部分，是安全系统的主要保障手段和工具。
然而，要设计一个没有漏洞的安全协议实属不易。目前，协议中的漏洞大多是通过形式化方法发现的。而在各种协议的形式化分析方法中，值得注意的是串空间（Strand Space）模型，它具有简洁明了的特点，主要依靠一定的因果关系将协议执行过程表示为图结构，并建立了在网络通信中可能传输的信息的代数，在认证协议和密钥分配协议的研究中，有着较大的影响。
1 相关工作
大量的安全协议设计似乎是依赖于设计者的技巧和独创性。其中最著名的是Abadi和Needham[4]。他们提出了一系列关于怎样使密码协议正确的方法以及如何使密码协议准确完成其安全目标。但是他们的理论不能系统化，也不能基于某种使协议目标正确的理论。
Butty'an等人[6]基于类BAN逻辑设计了一个协议设计方法，但这种方法很难从他们所给的例子中抽象出来。
Song[5]基于串空间理论设计了一种逻辑，再以此为模型得到一个协议自动检测算法－Athena。这种算法在一定条件下能处理状态空间爆炸的问题，而且可以用于协议的生成。可是这种方法还不能利用子协议的独立性去分解协议的设计过程，然后再把那些安全的小协议合成为完整的大协议。
我们设计的SECT协议是为了在三方协议交互中，使任意两方享有某些信息的机密性保护，并提供相互认证功能。同时，SECT还能提供有效的非否认证明。
2 符号与假设
参与者有三个不同的角色，类似于顾客，商店和银行，我们将分别表示为C，M，B。当然，即使是同一个参与者在不同的协议中可担任不同的角色。比如：当一家商店向另一家商店订货时，就分别作为C和M；而一家银行向商店购物时，就会作为C。我们将用P，Q泛指协议中任意两个参与者。
在三者之间，有一些信息是共享的，比如：三者的标识符和C向M提交的购物金额。但还有一些信息只限于两方知道，第三方不知道的，比如：C向M所购买的商品就与B无关；另外C的信用卡号最好不要让M知道；而M与B之间的交易手续费用属于商业机密，不应该让C知道。参与者P发送给Q的机密信息记为MsgP,Q；而P的所有可以共享的信息记为PubP。
信息t被P的密钥KP加密记为tP。把hash函数h作用于信息t所得的值记为h（t）。而所有能够证明攻击者所不能得到的密钥称为安全密钥，记为Safe。
3 串空间
下面介绍串空间模型的一些基本概念。
定义3.1 串空间（strand space）[1]是一个二元组（∑，tr）。其中∑是一个串（strand）的集合，这里的串可以用来表示任何序列。在协议分析中我们用它表示协议参与者或攻击者的行为序列。如果参与者是诚实的，就叫作正规串；如果参与者是不诚实的，就叫入侵者串。tr是一个映射，表示为：
这里A表示一个集合，（＋A）*表示由A中元素组成的有限序列。我们称这样的一个映射为迹映射，映射的像称作原像的迹（trace）。
定义3.2 对于一个串空间∑，定义节点为n＝
定义3.3 输出测试（outgoing test）令发出的加密包{…a…}K中包含一个唯一生成值a，其中K-1∈Safe，如果接收回一个不同的加密包{… a…}K1，则这个包首先是由一个正规的参与者生成的。图1表示了[3]命题19的简化形式。
定义3.4 输入测试（incoming test）[2]如果接收到一个加密包{… a…}K，其中K∈Safe，并且a从来没有以这样的加密形式发送过，则这个包首先是由一个正规的参与者加密的。图2表示了[3]命题20的简化形式。
图1：输出认证测试
图2：输入认证测试
定义 3.5 主动测试（unsolicited test）[2]：如果接收到term={|h|}K，并且密钥K∈Safe，则{|h|}K产生于某个正规的串。
4 SECT协议目标
（1）机密性：所有的加密交互信息保持机密性，发给另一方的信息不能给第三方解密。
（2）一类认证：参与者P能收到来源于Q的关于接收到P发送给Q的信息的证明。
（3）非否认性：每个参与者P都能向第三方证明其一类认证。
（4）二类认证：参与者Q能收到一个证明，证明如果其接收到声称是由另一个参与者所发的信息，则这个信息确是由P在当前这轮协议运行中所发出的。
5 两方子协议
图3：P，Q两方子协议
参与者 P 的数据就是两个值：MsgP，Q和 PubP。这两个值在传输过程中显然应该用Q的密钥加密，根据输入认证测试，这个过程要把一次性随机数NP，Q和{|MsgP，Q^PubP|}Q 一起传输。如果把 NP，Q也同时用Q的密钥加密，则子协议的这一步也可同时作为输出测试。当Q接收到P的信息后，返回的认证信息应该包含{… NP，Q…}Q。有时我们也需要返回包含MsgP，Q和PubP的信息，比如：当我们发出一个订单，那返回信息中就希望看到对货物的确认。所以Q返回的信息中包含{… NP，Q^t…}Q，其中 t包含 MsgP，Q和PubP的信息。在这里我们选择了 h（MsgP，Q^PubP），考虑到以后P和Q都可是C，M或者B，这样共有6种可能。为了将彼此区分开来，在协议每一步加入标识 ci，i从 1到 6。同时加上 F，S，T 作为子协议中各步的标识。
当P=C，Q=M时，在商务流程是这样的：当商店收到订单后，首先解密，检查订单是否正确，核实货物和单价；然后送到财务部，财务部hash MsgP，Q和PubP；然后签字，接着执行下一步。
为了完成二类认证目标，根据对Q的输入认证测试，Q向P发送一次性随机数NQ，P，因为P的签名密钥是安全的，当 Q 收到{|…^NP，Q^NQ，P^h（MsgP，Q^PubP)|}P后完成了一次输入测试。
协议的正确性由输入认证测试，输出认证测试和主动测试得知所设计的子协议满足上面所说的四个协议目标。
6 三方协议
定义6.1 强分离加密：n1是子协议∑1的节点，n2是子协议∑2的节点，如果{|h|}K⊂（n1）则{|h|}K（n2），称∑1和∑2满足强分离加密。
根据串空间理论，当子协议∑1和∑2满足强分离加密时，∑1和∑2是独立的，即∑1不论子协议∑2是否正在运行，都能实现其原定的安全目标。由图3的数据结构能够知道所设计的P，Q两方子协议满足强分离加密条件，所以当多个两方子协议同时运行时，不影响各自的安全目标。
对三方协议，要求遵循如下原则：
（1）对C和M以及C和B的子协议，都将首先由C开始第一步。当M和B分别接收到C和M的信息时才开始执行子协议的下一步。
（2）每个参与者只处理每个子协议中的确是发给自己的本协议的信息。
（3）如果一个参与者收到不是发给自己的信息，则转发给下一个参与者。
（4）
图4 SECT协议流程图
P，Q均表示为C，M，B其中之一；
SECT协议的四个安全目标的证明类似于双方子协议。
7 小结
文章中，我们利用串空间理论构造了一个电子商务协议SECT，展示了怎样利用协议的形式化分析工具来设计安全协议。协议的设计过程分为以下几步：
（1）明确表示出协议将要完成的目标。把某些仅由其中一部分参与者完成的目标设计成子协议。
（2）对于每个目标，选择一种认证方式来完成。验证每个子协议是否实现了独立的安全目标。再用分离加密保证协议的独立性。
（3）把子协议组合成完整的大协议，最后检验其安全性。
［1］F.Javier Thayer F'abrega，Jonathan C.Herzog，and Joshua D.Guttman.Strand Spaces:Why is a security protocol corrSECT？In Proceedings of the 1998 IEEE Symposium on Security and Privacy， pages 160-171.IEEE Computer Press，1998.
［2］Guttman，J.D.and F.J.Thayer F'abrega，Authentication tests， in:Proceedings， 2000 IEEE Symposium on Security and Privacy，May 2000.
［3］Joshua D.Guttman and F.Javier Thayer F'abrega.Authentication tests and the structure of bundles.Theoretical Computer Science，2002.
［4］M.Abadi and R.Needham.Prudent engineering practice for cryptographic protocols.In Proceedings，1994 IEEE Symposium on Research in Security and Privacy，pages 122-136.IEEE，IEEE Computer Society Press，1994.
［5］D.X.Song.Athena:a new efficient automated checker for security protocol analysis.In Proceedings of the 12th IEEE Computer Security Foundations Workshop.IEEE Computer Society Press，June 1999.
［6］L.Butty'an，S.Staamann，and U.Wilhelm.A simple logic for authentication protocol design.In 11th IEEE Computer Security Foundations Workshop，pages 153-162，1998.
