Petri Net Model and Analysis for Electronic Payment Security Protocol 电子支付安全协议的Petri网模型及分析林 松aboc_linsina.com 四川大学信息安全研究所CERNET第十二届学术年会2005年11月3日于大连1主要内容nPetri网简介n电子支付安全协议的Petri网模型n构建电子支付安全协议的可达树n分析电子支付安全协议n小结2前言n电子支付是客户利用电子账户，通过计 算机网络来实施的支付，随着计算机和 通信的发展，电子支付已经成为各银行 生存、发展和参与竞争的重要手段n如果没有安全保障，电子支付很难真正 发展起来n因此电子支付安全协议的研究就成为了 一个重要的课题 3Petri网简介n1962年，德国的C.A. Petri在他的博士论文用 自动机通信中首次使用网状结构模拟通信系 统，这是Petri网建立系统模型的起点 nPetri网兼顾了严格定义与图形语言两个方面， 具有丰富而严格的模型语义，同时又是一种图 形化的语言，具有直观、易懂与易用的优点 n它采用库所(place)、变迁(transition)、弧(arc) 的连接来表示系统的功能和结构 4库所、变迁、弧和托肯的说明n库所表示系统中的条件、资源和信息等可以静 态表达的事物 ，在图形具体表示中，用圆圈 “O”或椭圆表示n变迁表示系统中的变化，如状态的变化、条件 的变化、信息的流动以及资源的消耗和产生等 需要动态表达的事件，用矩形“口”或短棒“I”代 表 n弧表示库所与变迁之间的流关系，用 “”来表 示有向弧，用“”来表示抑制弧(inhibitor arc) n托肯表示库所中代表的事物的数量，用黑点“” 表示库所中含有的托肯5Petri网的特点nPetri网将系统看成一个白盒子，通过对系统内各要 素的抽象，分析这些要素相互作用引起的系统变化 ，是和黑盒子相反的分析方法，白盒子是通过给定 输入信号，根据系统的功能，推导输出信号n只要满足给定的条件或约束，Petri网将会自动进行 状态转换，体现了系统的动态行为特征 nPetri网综合了数据流、控制流和状态变迁，能方便 地描述系统的分布、并发、资源共享、同步、异步 、冲突等重要特性 6SET安全协议研究内容nSET(Secure Electronic Transaction)协议是电 子支付中比较复杂的安全协议之一n对SET协议的安全处理过程进行描述与分析 n重点研究加密和解密的安全处理流程 n分析双重数字签名处理过程n用Petri网理论建立起支付协议的安全模型 7电子支付密码协议的Petri网模型8模型中库所的含义库库所含义义库库所含义义库库所含义义p1初始信息p10发送的消息密文p19对称密钥p2发送的消息明文p11发送方的数字证书p20接收的消息密文p3发送方的私人密钥p12发送的数据p21接收的消息明文p4随机产生的对称密 钥p13发送方的数字证书p22明文中得到消息摘要p5接收方的数字证书p14发送方的公开密钥p23接收成功p6接收方的公开密钥p15接收的数字签名p24接收失败p7发送的数字信封p16签名中得到的消息摘要p25完整的明文信息p8发送的消息摘要p17接收的数字信封p26成功或失败的标识p9发送的数字签名p18接收方的私人密钥9模型中变迁的含义变变迁含义义变变迁含义义变变迁含义义t1对初始数据拆分t7数据打包并且发送t13对明文哈希运算t2对发 送明文哈希运算t8接收并且数据解包t14比较消息摘要t3用私人密钥签 名摘要t9获取发送方公开密钥t15数据完整性判断t4用对称密钥加密明文t10用公开密钥验证签 名t16产生并发送标识t5获取接收方公开密钥t11解密发送方数字信封t17接收标识 的处理t6加密公开密钥t12解密消息密文10发送方加密和接收方解密过程(一)n1.发送方获取自己的以及接收方的数字证书n2.认证接收方的数字证书，获得接收方的公开 密钥 n3.随机生成对称密钥 n4.用接收方公开密钥对随机生成的对称密钥加 密，将随机生成的对称密钥装入数字信封 n5.用随机生成的对称密钥将准备发送的消息明 文进行加密处理，生成消息密文 11发送方加密和接收方解密过程(二)n6.准备发送的消息明文经过哈希运算，得到消 息摘要 n7.用发送方的私人密钥对消息摘要签名处理， 得到数字签名 n8.将数字信封、消息密文、数字签名和发送方 的数字证书进行集成打包 n9.发送打包后的数据 n10.接收发送方的数据 n11.将接收的数据拆分为消息密文、数字信封 、数字签名和发送方的数字证书 12发送方加密和接收方解密过程(三)n12.通过对发送方的数字证书进行认证，获取 发送方的公开密钥 n13.用发送方的公开密钥验证发送方的数字签 名，得到一个消息摘要 n14.用接收方的私人密钥对接收到的数字信封 解密，从数字信封中取出对称密钥 n15. 用对称密钥解密接收到的消息密文，还原 出消息明文 n16.对消息明文进行哈希运算，得到另外一个 消息摘要 13发送方加密和接收方解密过程(四)n17.比较这两个消息摘要，确认消息的完整性 ，如果两个消息摘要相等，则表明接收到了完 整的发送数据，接收数据成功；反之就是数据 接收不完整，接收数据失败 n18. 将接收成功或失败的信息反馈给发送方 n19.发送方根据反馈的信息决定后继处理，如 果反馈回来的是成功的标识，则结束本次处理 ；反之，则继续重复发送上次的明文数据（可 以给重复发送的次数设定一个固定值，超过该 固定值时，则表示系统网络或设备等故障，整 个操作强制结束，不会出现死锁现象）14电子支付安全协议模型说明n用Petri网详细地描述了发送方加密和接收方解 密的处理过程，可以直观地阐述电子支付的安 全处理流程 n其中库所p24到变迁t15的弧为抑制弧(inhibitor arc)，表示只要库所p24有托肯，则变迁t15就不 能激发，库所p24没有托肯时，变迁t15才能激发n可以得出系统的输入、输出以及关联矩阵 n系统将非对称加密和对称加密结合使用：使用 非对称密码体制交换密钥，使用对称密码体制 传递信息正文15可达树的概念n可达树(Reachability Tree) 用来表示标识的可 以变化的过程n以初始标识作为树根，由可到达的标识作为树 的后继结点，每条连接结点的弧表示一个变迁 的点火，它将一个标识变换到另一个标识n给定一个Petri网系统，从初始标识开始，可以 得到数量与有效变迁一样多的新标识16电子支付协议的可达树17电子支付协议的可达树说明n图中“|”表示变迁可以并行引发，无论变迁引发的次序 如何，可达树都归结到同一个标识结点 n初始标识为 =(1,0,0,0,0,0,0,0,0,0,1,0,0,0,0,0,0,1,0,0,0,0,0,0,0,0) n激发t14时，比较两个信息摘要，判断是否接收完整 n当两个消息摘要相同时，表示接收成功，变迁序列 =t1t2t3t4t5t6t7t8t9t10t11t12t13t14t15，成功的终止标识为 =(0,0,0,0,0,0,0,0,0,0,1,0,0,0,0,0,0,1,0,0,0,0,0,0,1,0) n否则变迁序列=t1t2t3t4t5t6t7t8t9t10t11t12t13t14t16t17，将出 错信息反馈给发送方，接收数据失败的终止标识为 =(1,0,0,0,0,0,0,0,0,0,1,0,0,0,0,0,0,1,0,0,0,0,0,0,0,0) n发送方在一定重发次数的限定范围内重新发送上次的 数据 18电子支付协议的可达树分析n可达树中各结点库所包含的托肯数不超过两个 ，因此该电子支付协议是有界的、安全的 n可达树中各变迁至少引发一次，没有从不引发 的变迁，树中每个标号都有后继标号，即每个 标号都是可以引发的，根据活性的定义，可以 得知该网是活的，不会有死锁发生 n对于任意一个变迁，在引发之前，其它变迁都 只能引发有限次，因此该Petri网是公平的 n整个电子支付过程是可达的 19双重数字签名介绍n电子支付系统中，持卡人向特约商户提出购物 信息的同时，也给银行付款信息，以便开户行 付款，但是持卡人不希望特约商户知道自己的 银行账号信息，只需按照金额进行借记或者贷 记账户 n双重数字签名能够满足需要发送两个相关的信 息给接收者，接收者只能打开一个，而另一个 只需转发，不能打开看其内容的安全需求20双重数字签名的Petri网模型21双重数字签名模型中库所的含义库库所含义义库库所含义义库库所含义义 p1订货信息OIp16持卡人给商户的信息p31商户给银 行的信息p2支付信息PIp17接收的商户密文EMBp32接收的银行密文EMCp3订货消息摘要MDBp18接收的数字签名DSp33接收的数字签名DSp4支付消息摘要MDCp19数字签名的摘要MDBCp34数字签名的摘要MDBCp5订货和支付摘要MDBCp20接收的银行信封MDCp35接收的商户信封MDBp6数字签名DSp21商户订货 信息B(OI)p36银行支付信息C(PI)p7商户订货 信息B(OI)p22计算的订货摘要MDBp37计算的支付摘要MDCp8PBA和SCAp23计算的混合摘要MD*BCp38计算的混合摘要MD*BCp9PBB和SCAp24摘要相符接收正确p39摘要相符接收正确p10银行支付信息C(PI)p25摘要不符接收失败p40摘要不符接收失败p11PBC和SCAp26接收的PBA和SCAp41接收的PBA和SCAp12商户的密文EMBp27接收的商户信封DEBp42接收的银行信封DECp13银行的密文EMCp28利用PVB解密得SK1p43利用PVC解密得SK2p14银行的数字信封DECp29接收的银行信封DECp15商户的数字信封DEBp30接收的银行密文EMC22双重数字签名模型中变迁的含义变变迁含义义变变迁含义义变变迁含义义t1哈希运算订货 信息t9发送数据集成t17混合成消息摘要MD*BCt2哈希运算支付信息t10商户接收数据t18比较摘要MDBC和MD*BCt3混合成消息摘要MDBCt11商户向银行发送数据t19利用SK2解密EMCt4用PVA签署数字签名t12银行从商户接收数据t20用PBA从DS得到MDBCt5用对称密钥SK1加密t13利用PVB解密DEBt21从C(PI)得到MDCt6用对称密钥SK2加密t14利用SK1解密EMBt22混合成消息摘要MD*BCt7用SK1和PBB加密成数 字信封t15利用PBA从DS得到MDBCt23比较摘要MDBC和MD*BCt8用SK2和PBC加密成数 字信封t16从B(OI)得到MDBt24利用PVC解密DEC23小结 n这里利用Petri网理论，通过对安全电子支付的 详细分析，尤其是发送方加密和接收方解密的 处理，以及对双重数字签名的研究，建立了电 子支付安全协议的Petri网模型 n通过构建可达树，研究了电子支付SET协议的 正确性、保密性、活性以及公平性 n说明了电子支付安全协议Petri网模型的优点和 特点24今后的工作 n可以引入时间Petri网分析安全协议的执 行效率 n考虑入侵检测进行抗攻击分析 n可以利用关联矩阵(incidence matrix)的 方法分析系统的执行状态 n利用随机Petri网来研究安全协议的性能 n利用有色Petri网来解决状态空间爆炸的 问题 25欢迎指正 谢谢大家26