一种颜色Petri网的电子商务协议分析方法  

A Method of Analyzing E-commerce Protocols Based on Colored Petri Nets

作　　者：王宝文[1] 卢贝[1] 司亚利[2] 刘文远[1] 

机构地区：[1]燕山大学信息科学与工程学院,河北秦皇岛066004 [2]燕山大学里仁学院,河北秦皇岛066004

出　　处：《小型微型计算机系统》2013年第11期2594-2598,共5页Journal of Chinese Computer Systems

基　　金：河北省重大技术创新项目(09213562Z)资助;河北省自然科学基金青年科学(G2011203195)资助

摘　　要：针对现有颜色Petri网方法未能分析时限性的缺点,提出一种基于颜色Petri网的电子商务协议分析方法,用于分析可追究性、公平性和时限性三个重要安全属性.针对时限性建立了表示主体是否成功接收消息的状态颜色集和主体自定义的时间颜色集,并充分考虑时限性对公平性的影响,更加有效地分析公平性.文中以KZG协议为例,建立了KZG的分层颜色Petri网模型,利用CPN Tools工具对该模型仿真运行,并通过状态空间和查询函数分析了协议的性质,证明了本方法的有效性.An E-Commerce protocols analysis method based on Colored Petri Nets is proposed which has improved the timeliness dis-advantage of the existing CPN methods. This method can analyze three important security properties which are accountability, fair-ness, and timeliness. Status color sets which represent whether an entity successfully receives another entity＇s messages or not and timeliness color sets which represent the entity＇s self-defined time factor are established. Full consideration of timeliness is given when analyzing fairness in order to make the analysis results more accurate and effective. KZG protocol is taken as an example and a hierar-chical Colored Petri Net model is established. CPN Tools are used to simulate the protocol and state space analysis and query func-tions are taken to analyze it. At the same time, the method we proposed has been proven to be correct and effective.

关 键 词：形式化分析方法 电子商务协议 颜色PETRI网 CPN TOOLS KZG协议 

分 类 号：TP391[自动化与计算机技术—计算机应用技术]