论文部分内容阅读
提出一种扩展的有穷自动机模型,并结合卿-周逻辑给出一种新的电子商务协议形式化分析方法,用于分析电子商务协议的可追究性、公平性和时限性.该方法结合了模型检测和逻辑分析两种形式化分析方法的优点,可以准确形象地描述协议的具体运行过程,并且在发生重放攻击时能够正确分析各方的责任.利用该方法对Kim等人提出的改进版ZG协议进行了实例分析,给出了描述该协议运行过程的状态转换图,结合状态转换图对该协议分析得出其满足可追究性、公平性、时限性,并且不存在被重放攻击的可能.最后用时间自动机UPPAAL验证了新方法中有穷自动机模型的准确性和时限性分析的有效性.
An extended finite automaton model is proposed, and a new e-commerce protocol formal analysis method is given in combination with Qing-Zhou Logic to analyze the accountability, fairness and timeliness of e-commerce protocols. Combining the advantages of the two formal methods of model detection and logic analysis, we can accurately describe the operation process of the protocol and correctly analyze the responsibility of each party in the replay attack.Using this method, Kim et al. The improved version of ZG protocol is analyzed. The state transition diagram describing the operation of the protocol is given. According to the state transition diagram, the protocol is analyzed to find that it meets the requirements of accountability, fairness and timeliness, Put the attack possible.Finally, the time automaton UPPAAL is used to verify the accuracy and timeliness of the finite automaton model in the new method.