Initial state assumptions in Kailar logic reasoning
Ke Wang · Dalian Ligong Daxue xuebao · 2003
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.