Knowledge structure approach to verification of authentication protocols  

作　　者：SUKaile LüGuanfeng CHENQingliang 

机构地区：[1]DepartmentofComputerScience,SunYat-senUniversity,Guangzhou510275,China

出　　处：《Science in China(Series F)》2005年第4期513-532,共20页中国科学（F辑英文版）

基　　金：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.

关 键 词：formal verification security protocol epistemic logic Kripke semantics knowledge structure. 

分 类 号：TP3[自动化与计算机技术—计算机科学与技术]