改进型有色Petri网的安全协议分析

J4 ›› 2013, Vol. 35 ›› Issue (7): 60-63.

改进型有色Petri网的安全协议分析

张卉,李续武，赵媛莉，校云超

（空军工程大学防空反导学院，陕西西安 710051）

收稿日期:2011-11-22 修回日期:2012-05-28 出版日期:2013-07-25 发布日期:2013-07-25

Security protocols analysis
of improved colored Petri nets

ZHANG Hui,LI Xuwu,ZHAO Yuanli,XIAO Yunchao

(School of Air and Missile Defense,Air Force Engineering University,Xi’an 710051,China)

Received:2011-11-22 Revised:2012-05-28 Online:2013-07-25 Published:2013-07-25

摘要/Abstract

摘要：

利用有色Petri网分析安全协议时存在空间爆炸问题，对此提出了构建入侵者成功攻击安全协议所需知识集RI与入侵者可以获得的知识集KI，并定义入侵成功函数的改进型有色Petri网。利用改进型有色Petri网对具体的Helsinki协议和TMN协议进行了分析。实验表明，该方法能大大简化带有入侵者的Petri网模型的构造过程，有效缓解了Petri网在分析安全协议时的空间爆炸问题。

关键词: 有色Petri网, 安全协议, 攻击成功函数

Abstract:

According to the deficiency that space exploration may occur when the security protocols of colored Petri nets are analyzed, the paper proposes to construct the knowledge RI that is required by intruders to successfully attack the security protocols and the knowledge KI that can be obtained by intruders. And the improved colored Petri net of successful attack functions. The improved colored Petri net is used to analyze Helsinki protocol and TMN protocol. Experiments show that the proposal can simplify the procedure of constructing the Petri net with intruders, and efficiently solve the space exploration problem.

Key words: colored Petri nets；security protocols；attacking successful function

张卉,李续武，赵媛莉，校云超. 改进型有色Petri网的安全协议分析[J]. J4, 2013, 35(7): 60-63.

ZHANG Hui,LI Xuwu,ZHAO Yuanli,XIAO Yunchao. Security protocols analysis
of improved colored Petri nets[J]. J4, 2013, 35(7): 60-63.

[1]	钱文高1，耿宏1，马红岩2. 装配序列约束下的飞机虚拟维修过程建模仿真[J]. 计算机工程与科学, 2019, 41(08): 1482-1489.
[2]	秦济龙1，李庆华2，王恩东1，公维锋1，张峰1，牛赟3，乌力吉3，张向民3. 一种路由交换阵列节点芯片及其系统的设计与实现[J]. 计算机工程与科学, 2016, 38(12): 2392-2401.
[3]	陈星佑1,2，乐晓波1，曹伟1，周恺卿3. 基于分层模糊有色Petri网的防空C3I系统建模研究[J]. J4, 2016, 38(01): 102-107.
[4]	黄贻望1,2,万良1,李祥1. 基于TLA的NS安全协议分析及检测[J]. J4, 2010, 32(7): 38-41.
[5]	李振飞, 徐克林, 郭延涛. 基于HTCP-net的造船流程仿真与优化[J]. J4, 2010, 32(3): 127-129.
[6]	李军郑君杰. 一种设计Fail-Stop协议的新方法[J]. J4, 2008, 30(5): 9-10.
[7]	王彤彤[1] 吕志军[2] 王航[1]. 基于有色Petri网的攻击场景构造[J]. J4, 2008, 30(2): 28-33.
[8]	刘锋李舟军周倜李梦君. 使用组合协议逻辑PCL验证[J]. J4, 2008, 30(11): 13-15.
[9]	张练达卢昱. 星载子网安全通信协议的设计[J]. J4, 2007, 29(2): 19-23.
[10]	程建军[1] 胡旭晖[2]. 构建安全的嵌入式互联网[J]. J4, 2007, 29(12): 29-32.
[11]	刘海燕[1] 杨朝红[1,2] 蔡红柳[1]. 一个面向安全协议分析的非单调逻辑[J]. J4, 2007, 29(10): 1-3.
[12]	刘万伟周倜李梦君李舟军. 一种基于进程代数的安全协议验证消解算法[J]. J4, 2006, 28(7): 14-16.
[13]	周倜李梦君刘万伟李舟军. 安全协议的进程代数规约到逻辑程序的自动转换[J]. J4, 2006, 28(1): 22-24.
[14]	宋震李舟军窦文华. 基于类型理论的安全协议验证技术[J]. J4, 2005, 27(3): 7-9.
[15]	刘锋[1] 李舟军[2] 李梦君[1] 宋震[1] 张艳[3]. 基于SMV的安全协议模型检验[J]. J4, 2004, 26(2): 28-31.