Kailar逻辑推理中初始状态假设  

Initial state assumptions in Kailar logic reasoning

作　　者：王可心[1] 韩芳溪[1] 

机构地区：[1]山东大学计算机科学与技术学院,山东济南250062

出　　处：《大连理工大学学报》2003年第z1期193-196,共4页Journal of Dalian University of Technology

基　　金：山东省自然科学基金资助项目(003090309).

摘　　要：Kailar逻辑用于分析电子商务协议的可追究性,但初始状态假设引入不当会导致Kailar逻辑分析协议失败.通过对利用Kailar逻辑证明CMP1(b)协议与CMP1协议可追究性的过程以及对初始状态假设进行分析研究,针对初始状态假设所存在的问题,给出了初始状态假设应遵循的两个原则.实例表明,遵循该原则能够发现初始状态假设存在的问题,从而修正不适当的假设、补充新的假设,避免其引入不当所导致的Kailar逻辑分析协议失败问题.Kailar logic is used to analyze the accountability of electronic commerce protocols. But introducing initial state assumptions improperly can induce Kailar logic′s protocol analyzing failure. Through studying the proving process of CMP1(b) and CMP1 protocols of their accountability property and the initial state assumptions, two principles which should be followed by initial state assumptions are put forward as to the problems existing in them. Instances show that by following these principles, problems in initial state assumptions can be found, improper assumptions can be revised, and new assumptions can be added. Hence Kailar logic′s protocol analyzing failure resulting from introducing initial state assumptions improperly can be avoided.

关 键 词：KAILAR逻辑 电子商务协议 协议分析 初始状态假设 

分 类 号：TP309[自动化与计算机技术—计算机系统结构]