CPNtools 模拟工具适合分析什么样的协议

最近梳理和CPNtools和Scyther之间的性能和差别。方便后面整理使用

1、库所的托肯值是什么?

托肯值也叫作令牌, 即网络系统中的资源,托肯的数目值代表了网络赋予的资源大小。在一个活的网络系统中资源可以在库所中不断的流动。(在CPNtools中我们设定托肯值为拟定的值,可以用来检测协议中的错误,死锁状态),这就是说托肯值是可以可移动的(从一个库所移动到另一个库所),而且每个库所的的的托肯值并不是唯一确定的。

2、  基于CPNtools的网络协议建模与仿真技术研究

提出的问题:托肯值和颜色值是不是一个概念

回答:不是一个概念,首先托肯值是在建模分析的时候在每 个变迁上认为规定的,而颜色值

,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,   ,,,

附录:petri网的一些要点:

Petri里面有两种变迁如果都用发生的条件,则不认为其执行顺序有任何关系。Petri旨在描述变迁之间的因果关系,并由此构造时序。不支持构造大规模的模型,如自定向下,或者相反。

1 CPNtools验证协议存在的问题

PCNtools的本质是:

1、CPNtool 建模的前提条件

CPNtools研究协议存在的一些缺点是什么?

2、CPNtool不能使用模拟来验证协议的性质,,可以用来测试协议和定位协议错误

3、完全状态空间表示正在分析的模型的所有的可能的操作,完全状态空间的基本思想是计算CPN模型中所有可能达到的状态和状态变化(发生绑定元素),并将这些元素在与各有向图里表示,

4、TLS协议秘钥协商要通过客户端和服务端之间的预装置的证书,即证书中包含了双方之间认证需要的公钥,这个在CPN建模原理中不适用。

5、CPN 建模协议的原理和验证协议存在缺陷的问题是------通过状态空间遍历是否乱序或者序列号出现问题,但是这这EtherNet/IP中的种的安全机制中本身采用啦冗余校验机制避免了这种情况。所以使用CPN来分析EthetNet/IP协议本身是错误的,没有任何人价值意义

6、CPNtool 无法解决状态空间爆炸问题,采用约简方式简化状态空间的问题超出的能力范围

7、在模糊和非模糊环境下的协议验证成为Petri网研究的一个难点。

8、CPNtool 无法解决状态空间爆炸问题,采用约简方式简化状态空间的问题超出的能力范围

CPNtools在分析TLS协议中存在的问题

1、CPN建模范围:

如图TLS协议的双方认证机制,和加密认证机制原理图见下:

模拟工具在执行的时候选择随机绑定元素或者手动绑定元素执行序列,这与TLS握手协议双方之间认证过程原理违背。

TLS协议的的认证过程

EtherNet/IP有自己的容错检错机制,没有必要再讨论起安全的时候在再来分析是否丢包和包序列号问题。而CPN重点模拟协议的时候在检查协议错误的时候是以讨论是否存在丢包和乱序问题上。

1、CPNtool 建模的前提条件(待整理)

2、CPNtool不能使用模拟来验证协议的性质,,可以用来测试协议和定位协议错误

3、完全状态空间表示正在分析的模型的所有的可能的操作,完全状态空间的基本思想是计算CPN模型中所有可能达到的状态和状态变化(发生绑定元素),并将这些元素在与各有向图里表示,

4、TLS协议秘钥协商要通过客户端和服务端之间的预装置的证书,即证书中包含了双方之间认证需要的公钥,这个在CPN建模原理中不适用。

5、CPN 建模协议的原理和验证协议存在缺陷的问题是------通过状态空间遍历是否乱序或者序列号出现问题,但是这这EtherNet/IP中的种的安全机制中本身采用啦冗余校验机制避免了这种情况。所以使用CPN来分析EthetNet/IP协议本身是错误的,没有任何人价值意义

图1 是TLS的整个建立过程

分清楚CPNTool和Scyther之间的性能和分析协议我们开始分析协议之间的

这样TLS协议的认证完全不能使用CPN tools来建模分析。即便是使用CPN来建模TLS协议的握手认证过程,也不能来表征协议的安全性。

2、CPNtool不能使用模拟来验证协议的性质,,可以用来测试协议和定位协议错误

3、完全状态空间表示正在分析的模型的所有的可能的操作,完全状态空间的基本思想是计算CPN模型中所有可能达到的状态和状态变化(发生绑定元素),并将这些元素在与各有向图里表示,

4、TLS协议秘钥协商要通过客户端和服务端之间的预装置的证书,即证书中包含了双方之间认证需要的公钥,这个在CPN建模原理中不适用。

5、CPN 建模协议的原理和验证协议存在缺陷的问题是------通过状态空间遍历是否乱序或者序列号出现问题,但是这这EtherNet/IP中的种的安全机制中本身采用啦冗余校验机制避免了这种情况。所以使用CPN来分析EthetNet/IP协议本身是错误的,没有任何价值意义

6、CPNtool 无法解决状态空间爆炸问题,采用约简方式简化状态空间的问题超出的能力范围

第二部分:使用CPN来分析协议

CPNtools 提供给每一个变迁一个用CPN ML语言编程的程序编辑区,当变迁发生变化的时候,执行所编辑的程序,完成所需的功能,程序编辑区有三个固定的语句,input()     optput()   action()  表示输入参数   输出参数  执行语句。我们针对具体的不同的不可否认协议,将安全属性用CPN ML查询函数进行形式化描述。首先用断言函数定义不安全状态,即就是协议满足安全属性时不可能出现的状态。再定义搜索函数对状态空间的所有状态进行断言函数的测试。寻找符合的结点标识,最后于搜索查询函数 分析实验结果。

Scyther : 没有对丢包的验证说法。而只是验证协议的正确性,能否抵抗第三者的攻击

CPN tools  :研究自身协议的漏洞,可达性和

参考文献:苏桂平, 孙莎. 基于CPN模型的不可否认协议分析[J]. 信息安全与通信保密, 2011(08):61-62+65.


原文地址:https://www.cnblogs.com/xinxianquan/p/11836221.html

时间: 2024-11-13 06:46:34

CPNtools 模拟工具适合分析什么样的协议的相关文章

常用 Java 静态代码分析工具的分析与比较

转载自: http://www.oschina.net/question/129540_23043 简介: 本文首先介绍了静态代码分析的基本概念及主要技术,随后分别介绍了现有 4 种主流 Java 静态代码分析工具 (Checkstyle,FindBugs,PMD,Jtest),最后从功能.特性等方面对它们进行分析和比较,希望能够帮助 Java 软件开发人员了解静态代码分析工具,并选择合适的工具应用到软件开发中. 引言 在 Java 软件开发过程中,开发团队往往要花费大量的时间和精力发现并修改代

Geophysical.Software.Solutions(GSS).Potent.v4.12.04 1CD(主流位场模拟工具)

Geophysical.Software.Solutions(GSS)产品: Geophysical.Software.Solutions(GSS).Potent.v4.12.04 1CD(主流位场模拟工具)Honeywell产品: Honeywell.UniSim.Flare.R400.1-ISO 1CD Unisim Design R390.1-ISO 1DVD Unisim Design R390-ISO 1CD Unisim Design R370.1-ISO 1CD(模拟仿真) Hon

【转载】常用 Java 静态代码分析工具的分析与比较

摘自:http://www.oschina.net/question/129540_23043常用 Java 静态代码分析工具的分析与比较 简介: 本文首先介绍了静态代码分析的基本概念及主要技术,随后分别介绍了现有 4 种主流 Java 静态代码分析工具 (Checkstyle,FindBugs,PMD,Jtest),最后从功能.特性等方面对它们进行分析和比较,希望能够帮助 Java 软件开发人员了解静态代码分析工具,并选择合适的工具应用到软件开发中. 引言 在 Java 软件开发过程中,开发团

[转载] 常用 Java 静态代码分析工具的分析与比较

转载自http://www.oschina.net/question/129540_23043 简介: 本文首先介绍了静态代码分析的基本概念及主要技术,随后分别介绍了现有 4 种主流 Java 静态代码分析工具 (Checkstyle,FindBugs,PMD,Jtest),最后从功能.特性等方面对它们进行分析和比较,希望能够帮助 Java 软件开发人员了解静态代码分析工具,并选择合适的工具应用到软件开发中. 引言 在 Java 软件开发过程中,开发团队往往要花费大量的时间和精力发现并修改代码缺

协议分析 - DHCP协议解码详解

协议分析 - DHCP协议解码详解 [DHCP协议简介] DHCP,全称是 Dynamic Host Configuration Protocol﹐中文名为动态主机配置协议,它的前身是 BOOTP,它工作在OSI的应用层,是一种帮助计算机从指定的DHCP服务器获取它们的配置信息的自举协议. DHCP使用客户端/服务器模式,请求配置信息的计算机叫做DHCP客户端,而提供信息的叫做DHCP的服务器.DHCP为客户端分配地址的方法有三种:手工配置.自动配置.动态配置. DHCP最重要的功能就是动态分配

PLSQL_性能优化效能跟踪工具DBMS_PROFILER分析(案例)

一.摘要 Oracle PLSQL性能诊断是经常会遇到问题,所以Oracle提供了比较多的程式诊断工具,其中包括了dbms_profiler包 DBMS_PROFILER中会用到一些基本构建如下 在调用程式前DBMS_PROFILER.START_PROFILER,启动对该程式监控 在调用程式后DBMS_PROFILER.STOP_PROFILER,结束对程式监控 在监控过程中,系统会将资料存放至三个表中PLSQL_PROFILER_RUNS -> UNITS -> DATA 通过profil

终端模拟工具:Xshell 4

终端模拟工具:Xshell 4 2016-09-20 目录 1 安装 2 配置 3 命令 Xshell 是一个强大的安全终端模拟软件,它支持SSH1, SSH2, 以及Microsoft Windows 平台的TELNET NetSarang Xshell 4 Build 0120议. 1 安装 返回 下载地址:http://download.csdn.net/detail/wustzjf/8177749 2 配置 返回 打开工具Xshell 4,点击 菜单 File -> New... 如下图

Cisco PT模拟实验(5) 交换机的生成树协议配置

Cisco PT模拟实验(5) 交换机的生成树协议配置 实验目的: 理解生成树协议工作原理 掌握快速生成树协议RSTP的基本配置方法 实验背景:公司财务部和销售部的PC通过2台交换机实现通信,为提高网络可靠性,冗余链路是一个不错的思路,可防止因某条链路故障导致整个网络的中断,但冗余拓扑存在网络环路等一系列问题,为此需要在交换机上做适当配置. 技术原理: 生成树协议:监视二层交换式网络以找出所有可用的链路,并关闭冗余链路以确保不会出现环路. 首先利用生成树算法创建一个拓扑数据库,然后将网络的冗余备

mysql慢查询分析工具和分析方法

1.mysql慢查询分析工具 1.参考文档: http://www.ttlsa.com/mysql/analyse-slow-query-log-using-anemometer/ http://isadba.com/?p=655 官方文档: https://github.com/box/Anemometer 数据库管理员一般是用percona的toolkit工具来分析MySQL慢查询记录,但是不够直观. 下面介绍一款比较直观的工具来统计分析MySQL慢查询记录anemometer. 在使用之前