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

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

针对现有颜色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.