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

A Combining Deterministic Finite Automaton with Logic Rules Approach for Analyzing of E-commerce Protocol

作　　者：刘文远[1] 马生[1] 司亚利[2] 侯贵宾[1] 

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

出　　处：《小型微型计算机系统》2013年第3期492-497,共6页Journal of Chinese Computer Systems

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

摘　　要：提出一种扩展的有穷自动机模型,并结合卿-周逻辑给出一种新的电子商务协议形式化分析方法,用于分析电子商务协议的可追究性、公平性和时限性.该方法结合了模型检测和逻辑分析两种形式化分析方法的优点,可以准确形象地描述协议的具体运行过程,并且在发生重放攻击时能够正确分析各方的责任.利用该方法对Kim等人提出的改进版ZG协议进行了实例分析,给出了描述该协议运行过程的状态转换图,结合状态转换图对该协议分析得出其满足可追究性、公平性、时限性,并且不存在被重放攻击的可能.最后用时间自动机UPPAAL验证了新方法中有穷自动机模型的准确性和时限性分析的有效性.This paper presented an extended DFA,and based on the extended DFA and Qing-Zhou logic presented a new formal method which can be used to analyze security properties such as accountability,fairness and timeliness.This method which combined the advantages of model-checking and logical analysis can accurately and vividly describe the running process of protocols,and can correctly analyze the property when the replay attack occurs.Using this method,the state transition diagram of the improved version of ZG protocol presented by Kim was gave,accountability,fairness and timeliness were analyzed to be satisfied in this protocol,and found there were no replay attacks in this protocol.In the end,the model-checking tool UPPAAL was used to verify that the model of DFA was correct and the analysis of timeliness was effective.

关 键 词：电子商务协议 形式化分析 有穷自动机 逻辑分析 

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