【摘要】 Kailar逻辑用于分析电子商务协议的可追究性,但初始状态假设引入不当会导致Kailar逻辑分析协议失败.通过对利用Kailar逻辑证明CMP1(b)协议与CMP1协议可追究性的过程以及对初始状态假设进行分析研究,针对初始状态假设所存在的问题,给出了初始状态假设应遵循的两个原则.实例表明,遵循该原则能够发现初始状态假设存在的问题,从而修正不适当的假设、补充新的假设,避免其引入不当所导致的Kailar逻辑分析协议失败问题.更多还原

【Abstract】 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.更多还原