有穷机和逻辑结合的电子商务协议分析方法

发布时间：2018-02-23 01:33

本文关键词： 电子商务协议形式化分析有穷自动机逻辑分析　出处：《小型微型计算机系统》2013年03期 　论文类型：期刊论文

【摘要】：提出一种扩展的有穷自动机模型,并结合卿-周逻辑给出一种新的电子商务协议形式化分析方法,用于分析电子商务协议的可追究性、公平性和时限性.该方法结合了模型检测和逻辑分析两种形式化分析方法的优点,可以准确形象地描述协议的具体运行过程,并且在发生重放攻击时能够正确分析各方的责任.利用该方法对Kim等人提出的改进版ZG协议进行了实例分析,给出了描述该协议运行过程的状态转换图,结合状态转换图对该协议分析得出其满足可追究性、公平性、时限性,并且不存在被重放攻击的可能.最后用时间自动机UPPAAL验证了新方法中有穷自动机模型的准确性和时限性分析的有效性.
[Abstract]:In this paper, an extended finite automaton model is proposed, and a new formal analysis method of electronic commerce protocol is presented, which can be used to analyze the accountability of electronic commerce protocol. This method combines the advantages of two formal analysis methods, model checking and logic analysis, and can describe the specific running process of the protocol accurately and vividly. And when replay attack occurs, the responsibility of all parties can be correctly analyzed. By using this method, the improved ZG protocol proposed by Kim et al is analyzed as an example, and the state transition diagram describing the running process of the protocol is given. According to the analysis of the protocol based on the state transition diagram, it can be concluded that the protocol meets the requirements of accountability, fairness and time limit. Moreover, there is no possibility of being attacked by replay. Finally, the accuracy of the finite automaton model and the validity of the time-limited analysis in the new method are verified by using the timed automaton (UPPAAL).
【作者单位】：燕山大学信息科学与工程学院;燕山大学里仁学院;
【基金】：河北省重大技术创新项目(09213562Z)资助河北省自然科学基金青年科学(G2011203195)资助
【分类号】：TP393.04;F713.36

【参考文献】