CPNtools协议建模安全分析（一）

       本文根据最近整理的CPNtools论文和CPNtools官网上的说明，以及参照了乌克兰敖德萨 ---国家电信研究院运输和通讯部关于   电信系统协议仿真关于CPNtools的学生讲义。基于此和和本身的理解整理的关于CPNtools在协议建模状态空间分析以及其余的一些特征。具体的介绍基于对CPNtools的工具的实际操做来讲明。

       由于CPNtools是丹麦奥尔胡斯大学（Aarhus University）大学团队开发的软件，因此在该学院的 Department of Computer Science 部门有不少相关使用该软件作的工做。 学院官网地址：https://cs.au.dk/  能够在搜索栏中检索相关的CPNtools资料

      由于考虑了一下写的内容可能比较多，因此大致上分红几个章节来写。若是后续写的太多，我会在每一个博客作超连接到其余博客页面。（这项工做我会分红大概一周时间完成）

     由于CPNtools官网上的介绍没有针对如何建模协议来说，并且手册部分也很简单对作协议分析内有什么大的帮助。因此综合了不少材料，对CPNtool如何来建模协议模型想具体的写点东西。算是对本身论文的一个辅助材料，凡作事必须讲究认真。严谨的逻辑，不可捕风捉影，协议的形式化分析也必须是合乎规定，任何协议的形式化建模以前必需要根据协议组织的规范文档来作。

第一部分：界面的功能组件的介绍

 1.1 CPNtools的安装

     Windows安装：在官网上 http://cpntools.org/ 上下载界面下载 基于Windows版本的最近版本 ，下载以后安装便可

     Linux 安装：Linux安装以后会出现调用公用库的 libxml2.so.2  报错的问题，提示报错信息：: libxml2.so.2 cannot open shared object file: No such file or directory 解决问题的方法：使用   find 命令查询是否存在该库， 若是存在是不是对应软件版本和系统版本的不匹配问题， 若是没有下载安装便可， 若是有可是关联存在问题，使用 ln -sf 命令 对库文件的地址执行关联。 具体的执行步骤见图

      

  若是按照上面的操做仍是提示不能读取文件，提示下面的信息：

       ./cpntools: error while loading shared libraries:  libxml2.so.2: cannot open shared object file: No such file or directory

• 、首先打开/etc/ld.so.conf文件
• 、加入动态库文件所在的目录：执行vi /etc/ld.so.conf，在"include ld.so.conf.d/*.conf"下方增长"/usr/local/lib"。(具体的看本身的文件库位置)
• 、保存后，在命令行终端执行：/sbin/ldconfig -v；其做用是将文件/etc/ld.so.conf列出的路径下的库文件缓存到/etc/ld.so.cache以供使用，所以当安装完一些库文件，或者修改/etc/ld.so.conf增长了库的新搜索路径，须要运行一下ldconfig，使全部的库文件都被缓存到文件/etc/ld.so.cache中，若是没作，可能会找不到刚安装的库。 通常状况下能够解决共享库不能加载的问题，可是有时候用户仍是提示不能加载库，这个时候应该考虑是不是用户本身添加的软件或者本身生成的 .so动态库没有执行权限。

  安装完成以后操做的主界面以下。

 1.1.1 咱们先举一个简单的登陆协议的模型

   setp 1 首先建立两个库所，分别表示  Send 和 Reciver ,在建立一个变迁表示 网络 NET

     接下来声明颜色集合变量的类型，建模的简单模型结构件下图：

    

 

  step2 这里注意，颜色集绑定的数值标记定义好以后，在变迁NEt中会自动出现，变迁的绑定初始值，这个时候咱们须要点击变迁的左下方的小三角，来选择须要绑定的初始值，也就是将变迁使能。变迁使能绑定初始值见下图，这里我么选择绑定(n=1,p="one")

 

step3 在弧上写上弧表达式， 咱们定义了 var n=INT   p=DATA ， 因此从 SEND---->Reciver  弧的表达式为 （n,p）, 这里 从变迁NET到 Reciver端咱们 使用函数 来判断发送的数据。

step4 ,如今咱们来模拟数据从Send 发送到Reciver端，条件不符合的时候输出 fail  ,条件知足的时候输出 sucess

 

 

 

这里咱们要注意的是几点容易出错的问题：

•     颜色集申明的时候 不能和 默认的（Standard declarations）中的申明重复
•     在标记颜色集的数值的时候，注意 1`(1,"shijian")++   中的符号  `  不是英文的分隔符  ’  
•     变迁的初始值绑定是根据在于其输出的库所中的值决定的，可是须要本身手动来绑定

我本想这将主款工具界面操做部分汉化，可是官网上不发布 CPNtools的源代码版本，只支持对托管源代码的Subversion存储库开放。

1.1.2 tools BOX 的介绍

      我从最经常使用的工具开始介绍：

   Creat： 建立工具。  （功能介绍部分我所有放在图像上面，这样方便你们阅读。）

菱形表示建立一个变迁， 椭圆表示建立一个库所，单箭头表示建立弧

1.2 Petri网--CPNtools 层级网络介绍

  CPNtools最近被Nokia 被用来模型驱动的新一代手机的开发， CPN建模工具提出了强大的Petri网建模工具，一个抽象对象可使用层级网络建模分析，简单的（）

 

 第二部分： 原理的介绍

第三部分：简单协议的建模举例

第四部分：协议建模分析

第五部分：协议状态空间分析

第六部分：协议添加攻击模型的分析

第七部分：

参考文献：

[1] Simonsen K I F , Kristensen L M . Towards a CPN-based modelling approach for reconciling verification and implementation of protocol models.[C]// International Workshop on Model-based Methodologies for Pervasive & Embedded Software. Springer, Berlin, Heidelberg, 2012.

[2] Yiqin Lu, Fang Fang, Runqing Quan. A simulating model of NGN based on CPN tools[M]// Theoretical and Mathematical Foundations of Computer Science. 2011.

[3]D.A.Zaitsev, T.R.Shmeleva. Simulatiing of Telecommunication Systems with CPN Tools[M]// Affiliated on meeting of Communication Networks Department Transaction NO 4 of 10.11.2006.

[4] Wells L . Performance Analysis using CPN Tools[C]// Proceedings of the 1st International Conference on Performance Evaluation Methodolgies and Tools, VALUETOOLS 2006, Pisa, Italy, October 11-13, 2006. DBLP, 2006.

[5]Kent Inge Fagerland Simonsen, Lars M. Kristensen, Ekkart Kindler. Pragmatics Annotated Coloured Petri Nets for Protocol Software Generation and Verification[M]. Springer Berlin Heidelberg, 2016.

[6]Kent Inge.Code Generation from Pragmatics Annotated Coloured Petri Nets Simonsen.[M]//

[7]https://www.cpntools.org

[8]Ole Martin Dahl. Using Colored Petri NEts in Penetration Testing