SET协议解析.ppt

HCIS Security Team 2010 HCIS CorporationHCIS Security Team 2010 HCIS CorporationSET协议协议电子商务安全协议电子商务安全协议电子商务安全协议电子商务安全协议HCIS Security Team 2010 HCIS CorporationHCIS Security Team 2010 HCIS CorporationSETSET协议系统结构协议系统结构基本原理基本原理SETSET协议的形式化分析协议的形式化分析SETSET协议的完善与协议的完善与改进改进小结小结目目录录CONTENTSHCIS Security Team 2010 HCIS CorporationHCIS Security Team 2010 HCIS Corporation基本原理基本原理关于电子商务安全协议关于电子商务安全协议 电子商务协议用来保证电子商务的安全，早期电子商电子商务协议用来保证电子商务的安全，早期电子商务安全协议有务安全协议有Digicash协议，协议，FirstVirtual协议协议,Netbill协协议，现在有议，现在有SET协议，协议，IBS协议，协议，ISI协议，在线数字货币协议，在线数字货币协议，离线数字货币协议等，无论那种电子商务协议都协议，离线数字货币协议等，无论那种电子商务协议都要有如下特点：要有如下特点：HCIS Security Team 2010 HCIS CorporationHCIS Security Team 2010 HCIS Corporation11信息的保密性信息的保密性1 1：必须保证商家和顾客的订购，支付等：必须保证商家和顾客的订购，支付等信息的机密性。信息的机密性。22所有传输数据的完整性：保证所有在网络上传输的数所有传输数据的完整性：保证所有在网络上传输的数据都是未经篡改的。据都是未经篡改的。33信用卡用户合法身份鉴别：提供身份鉴别服务以减少信用卡用户合法身份鉴别：提供身份鉴别服务以减少冒认或者顶替事件的发生。冒认或者顶替事件的发生。HCIS Security Team 2010 HCIS CorporationHCIS Security Team 2010 HCIS Corporation44商家的合法身份和真实性鉴别商家的合法身份和真实性鉴别2 2：顾客必须能够鉴别与：顾客必须能够鉴别与之进行交易的商家是否是真实可信的。之进行交易的商家是否是真实可信的。55独立性：安全协议不能依赖特定的软件和硬件；安全独立性：安全协议不能依赖特定的软件和硬件；安全协议必须能在纯粹的协议必须能在纯粹的TCP/IPTCP/IP协议下运行，同时，安全协协议下运行，同时，安全协议也应该和其他的协议，如议也应该和其他的协议，如IPSecIPSec3 3,TLS,TLS4 4等协议联合使用。等协议联合使用。HCIS Security Team 2010 HCIS CorporationHCIS Security Team 2010 HCIS Corporation基本原理基本原理SET协议：SET 为 Secure Electronic Transaction 的缩写，由 Visa和MasterCard两大信用卡组织联合开发电子商务安全协议。SET协议也是一个基于可信的第三方认证中心的方案，采用公钥密码体制和X.509数字证书标准，主要应用于B2C5模式中保障支付信息的安全性。HCIS Security Team 2010 HCIS CorporationHCIS Security Team 2010 HCIS Corporation SET SET协议保证支付信息的机密，支付过程的完整，协议保证支付信息的机密，支付过程的完整，商家机持卡人的合法身份，以及可操作性。商家机持卡人的合法身份，以及可操作性。SET SET协议中的核心技术主要有非对称秘钥加密，协议中的核心技术主要有非对称秘钥加密，双重签名技术双重签名技术，安全数字安全数字证书证书，数字信封数字信封，数字时数字时间戳间戳等等。HCIS Security Team 2010 HCIS CorporationHCIS Security Team 2010 HCIS CorporationSETSET协议系统结构协议系统结构Internet持卡人商家认证中心支付网关银行网络收单银行发卡银行HCIS Security Team 2010 HCIS CorporationHCIS Security Team 2010 HCIS Corporation1，持卡人到发卡银行申请电子商务活动软件，并且到，持卡人到发卡银行申请电子商务活动软件，并且到CA申请数字证书。申请数字证书。2，商家也到，商家也到CA申请数字证书，鉴别不是申请数字证书，鉴别不是“黑店黑店”。3，发卡银行是负责为持卡人建立帐户并发放支付卡的金，发卡银行是负责为持卡人建立帐户并发放支付卡的金融机构。发卡银行在分理行和当地法规的基础上保证信融机构。发卡银行在分理行和当地法规的基础上保证信用卡支付的安全性。用卡支付的安全性。HCIS Security Team 2010 HCIS CorporationHCIS Security Team 2010 HCIS Corporation4，收单银行是商家建立帐户并处理支付卡认证和支付，收单银行是商家建立帐户并处理支付卡认证和支付的金融机构。的金融机构。5，支付网关是在银行与，支付网关是在银行与 Internet 之间专用系统，负之间专用系统，负责接收处理从商家传来的扣款信息，并通过专线送给责接收处理从商家传来的扣款信息，并通过专线送给银行；银行对支付信息的处理结果再通过这个专用系银行；银行对支付信息的处理结果再通过这个专用系统反馈回商家。统反馈回商家。HCIS Security Team 2010 HCIS CorporationHCIS Security Team 2010 HCIS Corporation6，为了保证，为了保证 SET 交易的安全，交易的安全，SET 协议规定参加交协议规定参加交易的各方都必须持有数字证书，在交易过程中，每次易的各方都必须持有数字证书，在交易过程中，每次交换信息都必须向对方出示自己的数字证书，而且都交换信息都必须向对方出示自己的数字证书，而且都必须验证对方的数字证书。必须验证对方的数字证书。CA 的主要工作是负责的主要工作是负责 SET 交易数字证书的发放、更新、废除、建立证书黑交易数字证书的发放、更新、废除、建立证书黑名单等各种证书管理。名单等各种证书管理。HCIS Security Team 2010 HCIS CorporationHCIS Security Team 2010 HCIS Corporation持卡人通过浏览器选择在线商店里自己需要的商品，放入持卡人通过浏览器选择在线商店里自己需要的商品，放入购物篮。购物篮。持卡人填写订单信息，并选择支付方式。持卡人填写订单信息，并选择支付方式。HCIS Security Team 2010 HCIS CorporationHCIS Security Team 2010 HCIS Corporation持卡人将订单信息和支付信息发送给商家，这里订单信息持卡人将订单信息和支付信息发送给商家，这里订单信息和支付指令由消费者进行数字签名，同时利用双重签名技术和支付指令由消费者进行数字签名，同时利用双重签名技术保证商家看不到消费者的账号信息及银行看不到消费者的订保证商家看不到消费者的账号信息及银行看不到消费者的订单信息。单信息。HCIS Security Team 2010 HCIS CorporationHCIS Security Team 2010 HCIS Corporation商家接受订单量信息后，与支付网关进行通信，请求授权商家接受订单量信息后，与支付网关进行通信，请求授权认证。认证。支付网关通过收单银行向持卡人的发卡银行请求进行支付支付网关通过收单银行向持卡人的发卡银行请求进行支付确认。确认。发卡银行同意支付，将确认信息通过支付网关返回给商家。发卡银行同意支付，将确认信息通过支付网关返回给商家。HCIS Security Team 2010 HCIS CorporationHCIS Security Team 2010 HCIS Corporation商家发送订单确认信息给持卡人，持卡人端软件可记录交商家发送订单确认信息给持卡人，持卡人端软件可记录交易日志，以备将易日志，以备将来查询。来查询。商家发送货物或提供服务。商家发送货物或提供服务。商家向持卡人的发卡银行请求支付，即实现支付获取、完商家向持卡人的发卡银行请求支付，即实现支付获取、完成清算。成清算。HCIS Security Team 2010 HCIS CorporationHCIS Security Team 2010 HCIS Corporation在处理过程中，通信协议、请求信息的格式、数据类型的定在处理过程中，通信协议、请求信息的格式、数据类型的定义等，义等，SET SET 都有明确的规定。在操作的每一步，消费者、商都有明确的规定。在操作的每一步，消费者、商家、网关都通过家、网关都通过 CA CA 来验证通信主体的身份，以确保通信的来验证通信主体的身份，以确保通信的对方不是对方不是冒名顶替冒名顶替。HCIS Security Team 2010 HCIS CorporationHCIS Security Team 2010 HCIS Corporation数字信封SETSET消息采用消息采用DESDES对称密码体制加密，而对称密码体制加密，而DESDES加密所用的加密所用的密钥则用密钥则用RSARSA公钥密码体制加密（接收者的公钥），所公钥密码体制加密（接收者的公钥），所传送的消息是这两部分密文信息的串联。传送的消息是这两部分密文信息的串联。HCIS Security Team 2010 HCIS CorporationHCIS Security Team 2010 HCIS Corporation数字信封数字信封的好处是提高了加密速度，避免了对称密钥的分数字信封的好处是提高了加密速度，避免了对称密钥的分发，保证了数据的机密性。只有用接收者的私钥才能够打发，保证了数据的机密性。只有用接收者的私钥才能够打开此数字信封，确保只有接收者才能对消息密文解密。多开此数字信封，确保只有接收者才能对消息密文解密。多用于一些电子商务用于一些电子商务交易中交易中。HCIS Security Team 2010 HCIS CorporationHCIS Security Team 2010 HCIS Corporation双重数字签名1 1，数字签名介绍，数字签名介绍鲍勃鲍勃的公钥鲍勃的私钥鲍勃一把私钥，一把公钥杰克道格帕蒂杰克，道格，帕蒂每人一把鲍勃的公钥HCIS Security Team 2010 HCIS CorporationHCIS Security Team 2010 HCIS Corporation消息Hash加密消息摘要私钥加密数字签名签名和消息一起鲍勃通过数字签名发信息给杰克鲍勃通过数字签名发信息给杰克杰克通过公钥解密得到消息摘要确定消息是鲍勃发送的杰克通过公钥解密得到消息摘要确定消息是鲍勃发送的签名和消息一起公钥解密消息摘要HCIS Security Team 2010 HCIS CorporationHCIS Security Team 2010 HCIS Corporation消息Hash加密消息摘要1数字签名公钥消息摘要2 杰克通过验证杰克通过验证消息经消息经hashhash加密加密后的消息摘要后的消息摘要1 1和数字签名通过和数字签名通过公钥解密得到数公钥解密得到数字签名字签名2 2比较，比较，如果一致表明消如果一致表明消息未经修改过。息未经修改过。HCIS Security Team 2010 HCIS CorporationHCIS Security Team 2010 HCIS Corporation如果道格用自己的公钥换走了杰克电脑里鲍勃的如果道格用自己的公钥换走了杰克电脑里鲍勃的公钥冒充鲍勃，那么道格就可以使用自己的私钥公钥冒充鲍勃，那么道格就可以使用自己的私钥做成数字签名，发送信息给杰克，杰克使用欺骗做成数字签名，发送信息给杰克，杰克使用欺骗的公钥可以解密。的公钥可以解密。道格道格的公钥杰克HCIS Security Team 2010 HCIS CorporationHCIS Security Team 2010 HCIS CorporationCA认证中心CA私钥数字证书CACA认证中心将鲍勃的公钥和一些鲍勃的相关信认证中心将鲍勃的公钥和一些鲍勃的相关信息通过认证中心的私钥加密，生成数字证书。息通过认证中心的私钥加密，生成数字证书。HCIS Security Team 2010 HCIS CorporationHCIS Security Team 2010 HCIS Corporation数字证书CA的公钥鲍勃的公钥数字签名消息摘要杰克收到鲍勃附有数字签名和数字证书的消息，就可杰克收到鲍勃附有数字签名和数字证书的消息，就可以通过使用以通过使用CACA中心的公钥解密数字证书得到鲍勃的公中心的公钥解密数字证书得到鲍勃的公钥，然后解密数字签名得到摘要，确认消息来自鲍勃。钥，然后解密数字签名得到摘要，确认消息来自鲍勃。HCIS Security Team 2010 HCIS CorporationHCIS Security Team 2010 HCIS Corporation数字证书内部格式是数字证书内部格式是CCITT X.509CCITT X.509国际标准所规定的，主要包国际标准所规定的，主要包括以下几点：括以下几点：1.1.数字证书拥有者的姓名数字证书拥有者的姓名2,2,数字证书拥有者的公共秘钥数字证书拥有者的公共秘钥3 3，公共秘钥的有效期，公共秘钥的有效期4 4，颁发数字证书的单位，颁发数字证书的单位5 5，数字证书的序列号，数字证书的序列号6 6，颁发数字证书单位的数字签名，颁发数字证书单位的数字签名HCIS Security Team 2010 HCIS CorporationHCIS Security Team 2010 HCIS Corporation数字证书的类型有三种：数字证书的类型有三种：个人证书：仅仅是为某一用户提供凭证，帮助其个人在网上个人证书：仅仅是为某一用户提供凭证，帮助其个人在网上进行安全交易操作。个人身份的数字证书通常安装在客户端进行安全交易操作。个人身份的数字证书通常安装在客户端的浏览器内。并通过安全的电子邮件（的浏览器内。并通过安全的电子邮件（S/MIMES/MIME7 7）来进行交易）来进行交易操作。操作。企业（服务器）证书：通常是为了网上某个企业（服务器）证书：通常是为了网上某个WEBWEB服务器提供服务器提供凭证，拥有凭证，拥有webweb服务器的企业就可以用具有凭证的万维网站服务器的企业就可以用具有凭证的万维网站点进行安全电子交易。有凭证的点进行安全电子交易。有凭证的webweb服务器会自动将其与客服务器会自动将其与客户端户端webweb浏览器通信的信息加密。浏览器通信的信息加密。HCIS Security Team 2010 HCIS CorporationHCIS Security Team 2010 HCIS Corporation软件（开发者）证书：通常为软件（开发者）证书：通常为InternetInternet中被下载的软件提中被下载的软件提供凭证，该凭证用于和微软公司供凭证，该凭证用于和微软公司AuthenticodeAuthenticode技术（合法技术（合法化软件）结合的软件，以使用户在下载软件时获得所需的化软件）结合的软件，以使用户在下载软件时获得所需的信息。信息。上述三类证书中前二类是常用的证书，第三类则用于较特上述三类证书中前二类是常用的证书，第三类则用于较特殊的场合，大部分认证中心提供前两类证书，能提供各类殊的场合，大部分认证中心提供前两类证书，能提供各类证书的认证中心并不普遍。证书的认证中心并不普遍。HCIS Security Team 2010 HCIS CorporationHCIS Security Team 2010 HCIS Corporation数字证书在数字证书在httpshttps协议中的应用协议中的应用首先，客户端向服务器发出加密请求。首先，客户端向服务器发出加密请求。HCIS Security Team 2010 HCIS CorporationHCIS Security Team 2010 HCIS Corporation服务器用自己的私钥加密网页以后，连同本身的数服务器用自己的私钥加密网页以后，连同本身的数字证书，一起发送给客户端。字证书，一起发送给客户端。HCIS Security Team 2010 HCIS CorporationHCIS Security Team 2010 HCIS Corporation客户端（浏览器）的客户端（浏览器）的 证书管理器证书管理器，有，有 受信任受信任的根证书颁发机构的根证书颁发机构 列表。客户端会根据这张列列表。客户端会根据这张列表，查看解开数字证书的公钥是否在列表之内。表，查看解开数字证书的公钥是否在列表之内。HCIS Security Team 2010 HCIS CorporationHCIS Security Team 2010 HCIS Corporation如果数字证书记载的网址，与你正在浏览的网址不如果数字证书记载的网址，与你正在浏览的网址不一致，就说明这张证书可能被冒用，浏览器会发出一致，就说明这张证书可能被冒用，浏览器会发出警告。警告。HCIS Security Team 2010 HCIS CorporationHCIS Security Team 2010 HCIS Corporation如果这张数字证书不是由受信任的机构颁发的，如果这张数字证书不是由受信任的机构颁发的，浏览器会发出另一种警告。浏览器会发出另一种警告。HCIS Security Team 2010 HCIS CorporationHCIS Security Team 2010 HCIS Corporation如果数字证书是可靠的，客户端就可以使用证书如果数字证书是可靠的，客户端就可以使用证书中的服务器公钥，对信息进行加密，然后与服务中的服务器公钥，对信息进行加密，然后与服务器交换加密信息。器交换加密信息。HCIS Security Team 2010 HCIS CorporationHCIS Security Team 2010 HCIS Corporation2，双重数字签名介绍，双重数字签名介绍双重数字签名是双重数字签名是SETSET协议的创新技术，发送者寄出两协议的创新技术，发送者寄出两个相关信息给接收者。接收者只能解读其中一组，个相关信息给接收者。接收者只能解读其中一组，另一组只能传给第三方接收者，不能打开看其内容。另一组只能传给第三方接收者，不能打开看其内容。这时，发送者需要分别加密两组密文，做两组数字这时，发送者需要分别加密两组密文，做两组数字签名，故称为双重数字签名签名，故称为双重数字签名。HCIS Security Team 2010 HCIS CorporationHCIS Security Team 2010 HCIS Corporation2，双重数字签名介绍，双重数字签名介绍双重数字签名的实现步骤如下:信息发送者甲对发给乙的信息 1生成信息摘要 A1。信息发送者甲对发给丙的信息 2生成信息摘要 A 2。信息发送者甲把信息摘要 A1和信息摘要 A 2合在一起,对其生成信息摘要 A 3,并使用自己的私钥签名信息摘要 S(A 3)。信息发送者甲把信息 1、信息摘要 A2和信息摘要 3的签名 S(A3)发给乙,乙不能得到信息 2。信息发送者甲把信息 2、信息摘要 A1和信息摘要 3的签名 S(A3)发给丙,丙不能得到信息 1。乙接收信息后,对信息 1生成信息摘要 A 1,把这信息摘要和收到的信息摘要 A2合在一起,并对其生成新的信息摘要 A3,同时使用信息发送者甲的公钥对信息摘要 3的签名进行验证,以确认信息发送者甲的身份;同时比较新的信息摘要 A3 与用甲的公钥解密出来的签名 A 3;若 A3=A3,则信息没有被修改过。丙接收信息后,对信息 2生成信息摘要 A2,把这信息摘要和收到的信息摘要 A1合在一起,并对其生成新的信息摘要A3 ,同时使用信息发送者甲的公钥对信息摘要 3的签名进行验证,以确认信息发送者甲的身份;同时比较新的信息摘要 A3 与用甲的公钥解密出来的签名 A3;若 A3 =A3,则信息没有被修改过。HCIS Security Team 2010 HCIS CorporationHCIS Security Team 2010 HCIS Corporation2，双重数字签名介绍，双重数字签名介绍SETSET协议双重数字签名的产生过程：协议双重数字签名的产生过程：OIPIMDBMDCMDBCDSPVAOI为持卡用户订购信息，PI为支付信息，PVA为持卡人A的私钥HCIS Security Team 2010 HCIS CorporationHCIS Security Team 2010 HCIS Corporation2，双重数字签名介绍，双重数字签名介绍采用双重数字签名技术的协议执行过程如下采用双重数字签名技术的协议执行过程如下9 9：(1)A-B:OI,Hash(PI),(Hash(OI),Hash(PI)priSK A,(PI)pubEK C(2)B-C:Hash(OI),(Hash(OI),E(PI)priSK A,(PI)pubEK C（A为持卡人，为持卡人，B为商家，为商家，C为银行，为银行，priSK A 表示表示A的私钥，的私钥，pubEK C表示表示C的公钥的公钥）这样，既可以实现确认持卡人的身份，又可以确保信息未被这样，既可以实现确认持卡人的身份，又可以确保信息未被篡改过篡改过。HCIS Security Team 2010 HCIS CorporationHCIS Security Team 2010 HCIS Corporation数字时间戳：数字时间戳：数字时间戳技术是数字签名技术一种变种的应用。在电数字时间戳技术是数字签名技术一种变种的应用。在电子商务交易文件中，时间是十分重要的信息。在书面合子商务交易文件中，时间是十分重要的信息。在书面合同中，文件签署的日期和签名一样均是十分重要的防止同中，文件签署的日期和签名一样均是十分重要的防止文件被伪造和篡改的关键性内容。数字时间戳服务（文件被伪造和篡改的关键性内容。数字时间戳服务（DTSDTS：digital time stamp servicedigital time stamp service）是网上电子商务安全）是网上电子商务安全服务项目之一，能提供电子文件的日期和时间信息的安服务项目之一，能提供电子文件的日期和时间信息的安全保护，由专门的机构提供。全保护，由专门的机构提供。HCIS Security Team 2010 HCIS CorporationHCIS Security Team 2010 HCIS Corporation如果在签名时加上一个时间标记，即是有数字时间戳如果在签名时加上一个时间标记，即是有数字时间戳的数字签名。时间戳是一个经加密后形成的凭证文档，的数字签名。时间戳是一个经加密后形成的凭证文档，它包括三个部分：它包括三个部分：需加时间戳的文件的摘要（需加时间戳的文件的摘要（digestdigest）；）；DTS DTS 收到文件的日期和时间；收到文件的日期和时间；DTS DTS 的数字签名。的数字签名。HCIS Security Team 2010 HCIS CorporationHCIS Security Team 2010 HCIS Corporation一般来说，时间戳产生的过程为：用户首先将需要加时一般来说，时间戳产生的过程为：用户首先将需要加时间戳的文件用间戳的文件用 Hash Hash 算法加密形成摘要，然后将该摘要算法加密形成摘要，然后将该摘要发送到发送到 DTSDTS，DTS DTS 在加入了收到文件摘要的日期和时间在加入了收到文件摘要的日期和时间信息后再对该文件加密（数字签名），然后信息后再对该文件加密（数字签名），然后送回用户送回用户。HCIS Security Team 2010 HCIS CorporationHCIS Security Team 2010 HCIS CorporationSETSET协议的形式化分析协议的形式化分析一，形式化方法在网路安全协议中的作用主要体现：一，形式化方法在网路安全协议中的作用主要体现：1 1，能使分析概念清晰，能使分析概念清晰2 2，能发现协议设计中的错误，能发现协议设计中的错误3 3，能证明协议的正确性，能证明协议的正确性4 4，能作为安全协议自动化分析，设计技术的理论指导，能作为安全协议自动化分析，设计技术的理论指导电子商务协议往往要求具有不可否认性和可追究性等安全电子商务协议往往要求具有不可否认性和可追究性等安全属性。所谓可追究性，是指某个主题可以向第三方证明另属性。所谓可追究性，是指某个主题可以向第三方证明另一方对某个动作或对象的发起负有责任，一方对某个动作或对象的发起负有责任，KailarKailar逻辑恰恰逻辑恰恰是针对此类安全属性而开发的形式化分析工具。是针对此类安全属性而开发的形式化分析工具。HCIS Security Team 2010 HCIS CorporationHCIS Security Team 2010 HCIS Corporation二，二，KailarKailar逻辑基本语句：逻辑基本语句：（1 1）强证明：）强证明：A CanProve xA CanProve x（2 2）弱证明：）弱证明：A CanProve x to BA CanProve x to B（3 3）签名认证：）签名认证：K Authenticates AK Authenticates A（4 4）消息解释：）消息解释：x in mx in m（5 5）声明：）声明：A says xA says x（6 6）消息接收：）消息接收：A Receives m SignedWith KA Receives m SignedWith K-1-1（7 7）信任：）信任：A Is TrustecOn xA Is TrustecOn x扩充语句：扩充语句：（8 8）A Sent x:AA Sent x:A发送了消息发送了消息x x（9 9）A Received xA Received x：A A接收了消息接收了消息x x（1010）A Has x:AA Has x:A拥有了消息拥有了消息x xHCIS Security Team 2010 HCIS CorporationHCIS Security Team 2010 HCIS Corporation三，分析假设三，分析假设在采用在采用Kailar逻辑分析协议的可追究性是基于以下假设成立前提逻辑分析协议的可追究性是基于以下假设成立前提下下：1，数字签名算法，数字签名算法假定数字签名算法不会被破解，对数字签名的验证不需要经过假定数字签名算法不会被破解，对数字签名的验证不需要经过签名者的同意，通过数字签名算法能够确保消息源的认证，消签名者的同意，通过数字签名算法能够确保消息源的认证，消息内容的完整性和消息发送者的不否认性。息内容的完整性和消息发送者的不否认性。2，信任，信任假装主题是可靠的。在公钥密码体制中，主体不会泄露私钥信假装主题是可靠的。在公钥密码体制中，主体不会泄露私钥信息；在对称密码体制中，主体不会伪装成其他共享秘钥的主体。息；在对称密码体制中，主体不会伪装成其他共享秘钥的主体。HCIS Security Team 2010 HCIS CorporationHCIS Security Team 2010 HCIS Corporation3，消息的完整性，消息的完整性假设消息的完整性可以得到保证，既不可能利用部分消息伪造签名消假设消息的完整性可以得到保证，既不可能利用部分消息伪造签名消息，也不可能计算出其他主体的私钥并伪造签名。息，也不可能计算出其他主体的私钥并伪造签名。4，服务的可用性，服务的可用性不存在拒绝服务问题，或此类问题得到解决，保证服务的可用性。不存在拒绝服务问题，或此类问题得到解决，保证服务的可用性。5，证书的撤销，证书的撤销公钥证书和权限证书的撤销是强制实施的，采用过期证书不能验证消公钥证书和权限证书的撤销是强制实施的，采用过期证书不能验证消息的有效性。息的有效性。HCIS Security Team 2010 HCIS CorporationHCIS Security Team 2010 HCIS Corporation 三，三，KailarKailar逻辑推理规则：逻辑推理规则：（1 1）联接：）联接：A CanProve x;A CanProve yA CanProve x;A CanProve y A CanProve(xy)A CanProve(xy)（2 2）蕴涵：）蕴涵：A CanProve x;x=yA CanProve x;x=y A CanProve y;A CanProve y;（3 3）签名的可追究性：）签名的可追究性：A Receives(m SignedWith K A Receives(m SignedWith K-1-1);x in m;A CanProve(K Authenticates B);x in m;A CanProve(K Authenticates B)A CanProve(B Says x)A CanProve(B Says x)（4 4）信任：）信任：A CanProve(B Says x);A CanProve(B IsTrustedOn x)A CanProve(B Says x);A CanProve(B IsTrustedOn x)A CanProve x A CanProve x HCIS Security Team 2010 HCIS CorporationHCIS Security Team 2010 HCIS Corporation(5)(5)认证规则：认证规则：Auth:CA Is TrustedOn KaAuth:CA Is TrustedOn Ka-1-1;B Receives x SignedWith Ka;B Receives x SignedWith Ka-1-1 B CanProve(Ka B CanProve(Ka-1-1 Authenticated A)Authenticated A)(6)(6)接收规则：接收规则：Rec:A Receives x SignedWith KRec:A Receives x SignedWith K-1-1 A Receives x A Receives x(7)(7)解密规则：解密规则：Dec:A Received XDec:A Received Xkaka A Receives XA Receives XHCIS Security Team 2010 HCIS CorporationHCIS Security Team 2010 HCIS Corporation四，四，SETSET协议形式化模型协议形式化模型SETSET协议异常复杂，这里只针对购买阶段的形式化分析。协议异常复杂，这里只针对购买阶段的形式化分析。在保留在保留SETSET原有性质的基础上，省略证书，将数字信封原有性质的基础上，省略证书，将数字信封用简单的公钥保密取代。用简单的公钥保密取代。（1）C-M:LID_M,Chall_C （购买初始化请求）（购买初始化请求）（1-1）M Receives(LID_M,Chall_C)LID_M是本地交易认证，是本地交易认证，Chall_C挑战挑战（2）M-C:(LID_M,XID,Chall_C,Chall_M)priSK M （购买初始化相应）（购买初始化相应）（2-1）C Receives(LID_M,XID,Chall_C,Chall_M)SignedWith KM-1 XID是购买的时间戳是购买的时间戳（3）C-M:PIDualSign,OIDualSign（购买请求）（购买请求）（3-1）M Receives h(PI)SignedWith KC-1（3-2）M Receives OI SignedWith KC-1（3-3）M Receives OIDualSign SignedWith KC-1HCIS Security Team 2010 HCIS CorporationHCIS Security Team 2010 HCIS Corporation（4 4）M-PM-P:(PI,PIDUALsIGN,h(OI)k:(PI,PIDUALsIGN,h(OI)kS,S,(K(KS S)kckc-1-1)k)kPGPG（认证请求）（认证请求）（4-14-1）PG Receives(PI)kPG Receives(PI)kS S)k)kPGPG（4-24-2）PG Receives(PIDualSign)kPG Receives(PIDualSign)kS S)k)kPGPG（4-34-3）PG Receives(h(OI)kPG Receives(h(OI)kS S)k)kPGPG（4-44-4）PG Receives(KPG Receives(KS S SignedWith KSignedWith KC C-1-1)K)KPGPG（5 5）P-MP-M(LID_M,XID,PurchAmt,authCode)(LID_M,XID,PurchAmt,authCode)priSK PpriSK P)pubEK MpubEK M（认证响应）（认证响应）（5-15-1）M Receives(LID_M,XID,PurchAmt,authCode)M Receives(LID_M,XID,PurchAmt,authCode)SignedWith KSignedWith KPGPG-1-1)K)KM M（6 6）M-C:(M-C:(LID_M,XID,Chall_C,Hash(PurchAmt)LID_M,XID,Chall_C,Hash(PurchAmt)priSK MpriSK M（购买响应）（购买响应）（6-16-1）C C ReceivesReceives(LID_M,XID,Chall_C,Hash(PurchAmt)LID_M,XID,Chall_C,Hash(PurchAmt)SignedWith K SignedWith KM M-1-1HCIS Security Team 2010 HCIS CorporationHCIS Security Team 2010 HCIS Corporation五，协议目标五，协议目标（G1G1）M CanProve(C Sent OI)M CanProve(C Sent OI)（G2G2）C CanProve(M Receives OI)C CanProve(M Receives OI)（G3G3）PG CanProve(C Sent PI)PG CanProve(C Sent PI)（G4G4）C CanProve(PG Receives PI)C CanProve(PG Receives PI)HCIS Security Team 2010 HCIS CorporationHCIS Security Team 2010 HCIS Corporation六