The standard Kripke semantics of epistemic logics has been applied successfully to reasoning communication protocols under the assumption that the network is not hostile. This paper introduces a natural semantics of K...The standard Kripke semantics of epistemic logics has been applied successfully to reasoning communication protocols under the assumption that the network is not hostile. This paper introduces a natural semantics of Kripke semantics called knowledge structure and, by this kind of Kripke semantics, analyzes communication protocols over hostile networks, especially on authentication protocols. Compared with BAN-like logics, the method is automatically implementable because it operates on the actual definitions of the protocols, not on some difficult-to-establish justifications of them. What is more, the corresponding tool called SPV (Security Protocol Verifier) has been developed. Another salient point of this approach is that it is justification-oriented instead of falsification-oriented, i.e. finding bugs in protocols.展开更多
This paper discussed how to handle the fairness conditions in partial Kripke structures. The partial Kripke structures were used for partial state spaces model checking, which is a new technique to solve problems of s...This paper discussed how to handle the fairness conditions in partial Kripke structures. The partial Kripke structures were used for partial state spaces model checking, which is a new technique to solve problems of state explosion. This paper extended the partial Kripke structure with fairness conditions by defining a partial fair Kripke structure, and a 3 valued fair CTL(Computation Tree Logic) semantics correspondingly. It defines a fair preorder between partial Kripke structures that preserves fairness and is akin to fair bisimulation. In addition, a pertinent theorem is also given, which indicates the relationship between the partial state spaces and the more complete one by illustrating the characterizations of states in the partial fair structure in terms of CTL formulae.展开更多
基金the reviewers.an d the trem endous kind help from the editors.This work was supported by the National Natural Science Foundation of China(Grant Nos.64096327,10410638 , 60473004)Germ an Research Foundation(Grant No.446 CHV1 13/240/0.1) Guangdong Provincial Natural Science Foundation(Grant No.04205407)
文摘The standard Kripke semantics of epistemic logics has been applied successfully to reasoning communication protocols under the assumption that the network is not hostile. This paper introduces a natural semantics of Kripke semantics called knowledge structure and, by this kind of Kripke semantics, analyzes communication protocols over hostile networks, especially on authentication protocols. Compared with BAN-like logics, the method is automatically implementable because it operates on the actual definitions of the protocols, not on some difficult-to-establish justifications of them. What is more, the corresponding tool called SPV (Security Protocol Verifier) has been developed. Another salient point of this approach is that it is justification-oriented instead of falsification-oriented, i.e. finding bugs in protocols.
基金National Natural Science Foundation of China( No.60 173 10 3 )
文摘This paper discussed how to handle the fairness conditions in partial Kripke structures. The partial Kripke structures were used for partial state spaces model checking, which is a new technique to solve problems of state explosion. This paper extended the partial Kripke structure with fairness conditions by defining a partial fair Kripke structure, and a 3 valued fair CTL(Computation Tree Logic) semantics correspondingly. It defines a fair preorder between partial Kripke structures that preserves fairness and is akin to fair bisimulation. In addition, a pertinent theorem is also given, which indicates the relationship between the partial state spaces and the more complete one by illustrating the characterizations of states in the partial fair structure in terms of CTL formulae.
基金Supported by the National Natural Science Foundation of China under Grant No.10771129the Innovation Foundation for Doctors of Shaanxi Normal University and the Outstanding Youth Foundation of Lanzhou University of Technology.
