基于petri网和逻辑电路的网络安全验证

《基于petri网和逻辑电路的网络安全验证》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。

1、万方数据第27卷第5期2010年5月计算机应用研究，ApplicationResearchofComputersV01．27No．5May2010基于Petri网和逻辑电路的网络安全验证白雪，吴长江，杨曼，赵不贿(江苏大学电气信息工程学院，江苏镇江212013)摘要：利用Petri网的库所和变迁来描述网络的状态和行为，用逻辑代数的0和1形象表示库所的状态，将复杂的PN模型转换成简单的逻辑表达式，提出了Petri网与逻辑电路相结合的新型网络数据流验证方式。这种方法具有的形式化步骤与数学模型相支持，是一种新型快捷的网络安全验

2、证方法。关键词：安全验证；Petri网；逻辑电路中图分类号：TP393．08文献标志码：A文章编号：·100l-3695(2010)05．1908．03doi：10．3969／j．issn．1001．3695．2010．05．087VerificationofnetworksecuritybasedonPetrinetandlogiccircuitsBAIXue，WUChaIlg·jiang，YANGMin，ZHAOBu-hui(&hod巧Elecl如f＆InformationEngineering，JmngmUnive

3、rsity，ZhenjiangJiangsu212013，China)Abstract：UsedplacesandchangesofthePetrinettodescribethestateandbehaviorofthenet，whileexpressedthestateoftheplaceby“0’’and⋯1’inthelogicalgebra．thusconvertedthecomplicatedPetrinetmodelstosimplelogicexpressions．Soadvancedanewmethod

4、combingthePetrinetandthelogiccircuit．inwhichsupportedtheformalizedstepandthemathemati-calmodelmutually．Itisaneffectiveandrapidmethodtoverifythenetworksecurity．Keywords：securityverification；Petrinet；logiccircuit0引言计算机网络是信息化的网络系统，保护计算机网络的安全，实质就是对网络信息数据流安全的控制。保护机密数据

5、不被未授权的用户访问是一个典型的安全问题。一般通过应用基于角色访问控制⋯策略的系统来限制用户访问能力及范围，以此来限制对重要敏感资源的访问。然而访问控制策略不能够彻底阻止敏感信息的泄露，因为访问控制策略主要是对用户静态地设置访问控制权限，不能够根据网络环境的变化作出动态调整，这说明仅仅依靠访问控制策略是不够的，还必须考虑对象之间的信息流动拉j，在网络上建立全局动态控制策略。然而所建立的全局控制策略是否有效、是否安全，则要通过一定的网络安全验证。验证方法的优劣将直接影响网络的安全性能。常用的验证方法主要有三类：a)基于模态

6、逻辑的验证方法，最著名的是1989年DEC公司研究人员提出的BAN类逻辑。该逻辑的提出是安全分析验证的一个里程碑；b)基于状态空间搜索的验证方法，状态空间搜索法也叫做模型检测法，它是一种验证有限状态系统的自动化技术；e)基于定理证明的验证方法，定理证明是对形式化后的协议模型和规约，运用证明的技术来证明规约是否在协议模型中满足。随着网络规模的扩大，这些方法往往不太适应，可能会导致状态爆炸现象，从而给验证工作带来困难。新一代网络安全验证方法应运而生，如仿生网络安全技术正受到越来越多的关注pJ，而本文则是将Petri网与逻辑电

7、路相结合，提出了一种新型验证网络数据流系统结构安全与否的方法。Petri网具有异步并发特性MJ，多用于并发和分布式系统行为描述；同时Petri网也是一种数学模型垆J，可以用库所和变迁来描述网络的状态和行为，而逻辑代数用0或1，代表矛盾与对立的两个方面，研究二值变量的运算规律。将两者结合，可以把复杂的Petri网模型转换成简单的特定逻辑表达式，从而使人们能快速高效验证网络系统是否安全可靠。1将Petri网转换为逻辑电路的算法近几年来，基于Petri网的逻辑实现方法逐渐受到了重视。文献[6，7]提出了一种将Petri网转换成

8、逻辑电路的设计思想。文献[8]提出了一种新的基于逻辑代数的化简方法，简称RM．LC(reduorionmethodsbasedonlogiccircuit)。在这些理论和实践基础上，将其运用到网络数据流安全结构验证中。逻辑电路一般都是由以下四个基本构造块(fork、join、choice和merge)按照一定的组合方