文档介绍：第六章 Petri网模型及分析
林松
aboc_lin@
四川大学信息安全研究所
第十二届学术年会
2005年11月3日于大连
1
主要内容
Petri网简介
电子支付安全协议的Petri网模型
构建电子支付安全协议的可达树
分析电子支付安全协议
小结
2
前言
电子支付是客户利用电子账户,通过计算机网络来实施的支付,随着计算机和通信的发展,电子支付已经成为各银行生存、发展和参与竞争的重要手段
如果没有安全保障,电子支付很难真正发展起来
因此电子支付安全协议的研究就成为了一个重要的课题
3
Petri网简介
1962年,. Petri在他的博士论文《用自动机通信》中首次使用网状结构模拟通信系统,这是Petri网建立系统模型的起点
Petri网兼顾了严格定义与图形语言两个方面,具有丰富而严格的模型语义,同时又是一种图形化的语言,具有直观、易懂与易用的优点
它采用库所(place)、变迁(transition)、弧(arc)的连接来表示系统的功能和结构
4
库所、变迁、弧和托肯的说明
库所表示系统中的条件、资源和信息等可以静态表达的事物,在图形具体表示中,用圆圈“O”或椭圆表示
变迁表示系统中的变化,如状态的变化、条件的变化、信息的流动以及资源的消耗和产生等需要动态表达的事件,用矩形“口”或短棒“I”代表
弧表示库所与变迁之间的流关系,用“→”来表示有向弧,用“—◦”来表示抑制弧(inhibitor arc)
托肯表示库所中代表的事物的数量,用黑点“•”表示库所中含有的托肯
5
Petri网的特点
Petri网将系统看成一个白盒子,通过对系统内各要素的抽象,分析这些要素相互作用引起的系统变化,是和黑盒子相反的分析方法,白盒子是通过给定输入信号,根据系统的功能,推导输出信号
只要满足给定的条件或约束,Petri网将会自动进行状态转换,体现了系统的动态行为特征
Petri网综合了数据流、控制流和状态变迁,能方便地描述系统的分布、并发、资源共享、同步、异步、冲突等重要特性
6
SET安全协议研究内容
SET(Secure Electronic Transaction)协议是电子支付中比较复杂的安全协议之一
对SET协议的安全处理过程进行描述与分析
重点研究加密和解密的安全处理流程
分析双重数字签名处理过程
用Petri网理论建立起支付协议的安全模型
7
电子支付密码协议的Petri网模型
8
模型中库所的含义
9
模型中变迁的含义
10