1、替代变迁

包含有替代变迁的页面叫做父页,当CPN网使用替代变迁的时候,替代变迁所表达的逻辑必须在某一个位置得到实现,实现替代变迁逻辑页面叫做子页或者子网。

将替代变迁相邻的库所叫做槽库所,也即是在替代变迁和草库所之间至少有一条弧相连。多重实例的现象,每个子页面的实例都是完全独立的,同一子页面的其他实例标识无关。

2、颜色集

单元颜色集由简单的元素组成,标号为();

color name=unit[with new_unit]

3、 LTS协议建模方面我们使用CPN Tools工具,CPN Tools是丹麦研究员Arhus开发的基于有色Petri网的计算机辅助设计工具,不仅支持CPN ML编程语言,颜色集、世间、层次化模型、状态空间分析,它具有编辑,模拟和分析有色Petri网的功能,支持时间CPN和分成CPN[162],CPN Tools基于Design/CPN开发,使用良好的人机界面即使重新设计用户图形界面(GUI),使用CPN协议仿真工具,用户可以轻松的建模,仿真和分析并行系统,由于CPN Tools使用ML语言来扩展模型,

CPN是一种能够对模型系统进行检验和建模的语言,适合分析和藐视具有并和同步等特征的系统,

CPN ML主要用于定义颜色集、变量和函数、CPN Tools支持的颜色集又单元型 unit 、整型int 、实数型real 乘积型 product 等,支持的函数有指数分布型,均匀分布函数、额泊松分布函数等。定义颜色集用关键字 var,而定义函数使用关键字fun ,定义一个整型变量a, fun c()=discrete(1,10) 定义一个函数 c() 表示随机产生一个从1到10的整数。使用者通过CPN ML定义颜色集、变量、和函数等可以减少变迁和库所的使用量。 对于大规模复杂系统建模有着很大的优势。特别是结合层次化,对模型进行层次建模,有利于理解且有效抑制“空间爆炸问题”

分层,监视器、和空间状态是CPNTools提供的另外三种重要的机制,分层CPNTools提供一种重要的机制,通过分层功能建立层次化模型,有助于模型表达和理解,层次模型不限制网络规模,可求解大规模的排队问题,有效的解决简单Petri网引起的组态爆炸问题,CPNTools通过替代变迁,融合库所等方式实现层次化建模。

本文使用CPN(Colored Petri Net)对TLS协议进行建模,使用仿真工具CPNTools分析TLS握手协议秘钥建立的相关性质,

Petri网是一种基于状态的建模方法,CPN是在Petri网基础上扩展而来,具有概念简单以及图形化表达的特点,Kumar和Spafford将Petri网应用于Web安全领域,[基于CPN的Oauth协议建模与分析7] , CPN在解决协议建模问题上有以下的优势:

层次化: 引入了层次化的网络结构,含有替代变迁和融合库所。可以利用多可彼此联系的CPN网子模型构建复杂系统的整体模型。

可以实现推理,具有变迁机制,库所被触发之后变迁到达新的库所,因果关系明确

可以处理并发和顺序性的问题,具有实践因子可以处理不同行为发生的时间

有较为完善的仿真工具,可以使用CPNTools工具进行可视化建模和房展分析

基础Petri网是一种由库所(P,Place)和变迁(T,Transition),有向弧(C,connection ),以及令牌(Token)等元素组成的简单过程模型。Petri网是一个三元组(P,T,F),FC(PxT)

下面给出CPN的定义:CPN=(P,T,C,Σ,V,F,G,E,I)他是一个九元组。其中

P:表示库所 p(Place ) 的有限集合

T:是变迁 t(Transition )的有限集合

C是有向弧c(Connection)的集合 (PxT)∪(TxP),有向弧智能有库所指向变迁,或者由变迁指向库所。不能指向同类型的节点。

是有限非空颜色集(Color set),建模时由建模者根据模型设计颜色集,赋予令牌更多的信息。

V是变量的集合,对所有的变量v 满足 Type[v]=

F Pà 是颜色的集合,为每个库所指定颜色集

G TàEXPRv是防卫表达式函数,它指定了变迁的防卫表达式,对所有的变迁t,都存在 : Type=[G(t)]=BOOL 防卫表达式的返回值必须是布尔类型

E CàEXPRv 是弧表达函数,它指定了每条弧表达式,对于所有的有向弧c都存在Type[E(a)]=F(p)ms  ,弧表达式的类型和与他相连接的库所的类型相同。

I :P

协议建模的:

首先协议的顶层模型:

定义协议的颜色集合变量如下:

colset DATA=string;

colset NO=INT;

colset NO*DATA=Product NO*DATA;

var success:BOOL;

05-11 10:54