基于赋时颜色Petri网的NSSK协议建模.pdfVIP

第20 期 计 算机 技 术 与 发 展 Vo1．20 No．6 2010年 6月 O0M Un RTECHNOLOGYANDDEVELoPMENT Jun． 2010 基于赋时颜色 Petri网的NSSK协议建模 韩 咚 ，田银花2 (1．山东科技大学继续教育学院，山东泰安 271000； 2．山东科技大学信息工程系，山东泰安 271000) 摘 要：随着对计算机网络应用的不断深入，对网络协议的安全性进行分析和研究已经成为信息安全领域的一个十分重 要的研究方向。设计安全协议时，协议的安全性验证是消除安全协议脆弱性和不精确性的关键步骤。验证安全协议的模 型和工具有很多，主要应用赋时颜色 Pe试 网分析了安全协议中著名的NSSK协议，应用赋时颜色 Petri网的变迁为导向的 建模方法，成功地对N跚 (协议进行了建模，并验证了协议运行过程中的有效性。为下一步利用颜色Petri网协议针对 NSSK协议的安全性进行分析打下了良好的基础。 关键词 ：NSSK协议；Petri网；协议分析 中图分类号：粥 93．08 文献标识码：A 文章编号：1673—629X(2010)06—0156—03 TheModelingofNSSK ProtocolsBasedonTimedColoredPetriNets HAN Dong ，TIAN Yin—hua2 (1．AdultEducationCollege，ShandongUniversityofScienceandTechnology，Tai’an271000，China； 2．DepartmentofInformationandEngineering，ShandongUniversityof SciencenadTechnology，Tai’na 271000，China) Abstract：Withthedevelopmentofcomputernetwork，application，analysisandinvestigatbnsecurityprotocolisbecomingaveryimpor- tantas1)ectintheareaofinformationsecurity．VerifieationisacrucialsteptOeliminateweakrlt~sesandinaccuraciesofeffictivesecurity protoeols．TherearemanymodelsandtOO|Stoverifysecurityprotoco1．MainlyapplyTCPN toanalysisnadniodeINSSK protoco1．Itap· pliesthemodelingmethodbasedOnthetranssionsofCPN ，modelsfortheNSSK protocolsuccessfullynadvMidatestheefficiencyofthe protocolprocess，verifyingtheeffectivenessoftheoperationprocessoftheprotoco1．Itmakesgoodfoundationsforthefollowingsecurity analysisofNSSK protocolusjng ，N． KeyWOrdS*．N跚 (protocol；Petrinet；protocolanalysis O 引 言 l 赋时颜色 Petri网 Petri网是一种用于分布式系统建模和分析的重 定义 118]：颜色 Petri网是一个七元组：CPN= (S， 要工具。随着Pet