网络安全协议的形式化分析与验证 作者 李建华 第七章 电子商务安全协议及其分析.pptVIP

PIData和OIData分别表示支付信息和订单信息。订单信息是想让商家了解的，而支付信息只希望让支付网关得到。订单信息的双重签名包括了订单信息，以及支付信息的哈希值。持卡人将支付信息的哈希及订单信息的哈希串联并使用自己的私钥签名，形成支付信息的双重签名。其中 PIData = PIHead, PANData PIHead = LID_M, XID, HOD, PurchAmt, M, Hash(XID, CardSecret) PANData = PAN, PANSecret，PAN指的是信用卡信息，而PANSecret表示 PAN密钥。 OIData = XID, Chall_C, HOD, Chall_M HOD = Hash(OrderDesc, PurchAmt) 表示订单描述和购买量的哈希，以供商家核实。 7.3.3 数字信封 SET协议的每一个参与者都使用DES、RSA等密码系统来对交易进行加密。 SET协议中的信息加密采用数字信封技术，使用公钥和私钥相结合的方法进行加密。数字信封的原理如下图所示。 SET消息采用DES对称密码体制加密，而DES加密所用的密钥则用RSA公钥密码体制加密，所传送的消息是这两部分密文信息的串联。 SET协议浅析： 由于功能非常强大，SET协议是目前为止最为完善的电子商务安全协议。但是，它也有缺点： 首先，SET交易过程十分复杂，在对于安全性要求相对较低的环境下，人们通常更倾向于开销小很多的SSL协议。 其次，SET系统需要建立一个为商家、银行、发卡机构和消费者普遍认可的CA认证体系，这是一个敏感的商业问题，牵涉到多方利益，很难协调。 最后，作为一种卡支付协议，它对别的安全协议，如SSL、IP sec/VPN、S/MIME等都不兼容。 7.3.4 SET协议的形式化分析 SET协议十分复杂，其形式化分析也显得异常复杂。主要的证明方法有推理构造方法，（如Kailar逻辑等），其他的证明方法如Isabelle分析器和进程代数演算等。本节将具体介绍基于Kailar逻辑的证明方法。 Kailar逻辑能够分析协议的可追究性，但不能分析协议的公平性。 一个公平的交易协议是指能够保证任何一方在电子商务交易中都不能够通过欺诈、欺骗或者提前结束协议的手段从另一方得到利益的协议。 有时达到以上的目的是不可能的，遇到这种情况时可以采用弱一点的目标，即在协议进行的时候收集证据，这样诚实的一方就能用来为自己作证。 结合SET协议流程对Kailar逻辑进行扩充。 1．Kailar逻辑的扩充 （1）扩充的基本语句 A Sent x：A 发送了消息x。 A Received x：A接收到了消息x。 A Has x：A拥有了消息x。 （2）扩充的基本推理规则 1）认证规则 Auth： 由于CA扮演了一个可信的第三方的角色，因此，如果CA对某一个私钥负责，而B收到一个使用Ka-1签名的消息时，B可以证明这个消息确实是由A发出的。 2）接收规则。 Rec： 在SET协议中公钥为大家所共有，因此，这条规则特别地应用于此协议的证明中，它表示收到签名的消息时也收到了此条消息。 3）解密规则。 Dec： 在此协议中，当某一方收到用自己的公钥加密的消息时，就相当于收到了这条消息。 2．SET协议模型 SET协议的形式化分析是十分困难的。其中，面临的第一个问题就是协议的描述文件长达1000多页，协议本身也异常复杂，使得手工或自动化分析工具难以对SET协议进行分析。 SET协议一般包括5个步骤。由于其复杂性，本章只对其中的一步——购买阶段进行形式化分析。 SET的购买阶段不仅有着大量的加密签名操作，并且还包括了SET协议的双重签名。分析中，我们在保留SET原有性质的基础上，省略了证书，并且将PKCS数字信封用简单的公钥加密取代，从而将SET的购买阶段表示成一个6步骤模型。 SET购买阶段的6步骤模型 （0）初始购物协定 在这个步骤中，持卡人和商家在订单描述（OrderDesc）以及购买数量（PurchAmt）上达成一致。由于这个过程只是SET购买协议的一个初始化的阶段，因此记为第0步。 （1）购买初始化请求 C—M: LID_M, Chall_C 持卡人给商家发送了一条新鲜的挑战（Chall_C）以及本地交易认证（LID_M）。 （2）购买初始化响应 M—C : (LID_M, XID, Chall_C, Chall_M)priSK M 商家使用一条用自己私钥签名的