Verification of Authentication Protocols for Epistemic Goals via SAT Compilation

作     者：苏开乐 陈清亮 Abdul Sattar 岳伟亚 吕关锋 郑锡忠 

作者机构：Department of Computer Science Sun Yat-Sen University Guangzhou 510275 P.R China Institute for Integrated and Intelligent Systems Griffth University Brisbane Qld 4111 Australia College of Computer Science and Technology Beijing University of Technology Beijing 100022 P.R. China Department of Computer Science Brandenburg University of Technology Cottbus 03036 Germany 

出 版 物：《Journal of Computer Science & Technology》 (计算机科学技术学报（英文版）)

年 卷 期：2006年第21卷第6期

页      面：932-943页

核心收录：

学科分类：08[工学] 0835[工学-软件工程] 081202[工学-计算机软件与理论] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

基　　金：This work is supported by the National Grand Fundamental Research 973 Program of China under Grant No 2005CB321902  the National Natural Science Foundation of China under Grant Nos. 60496327  10410638 and 60473004  German Research Foundation under Grant No. 446 CHV113/240/0-1  Guangdong Provincial Natural Science Foundation under Grant No. 04205407  and KAISI Fund in Sun Yat-Sen University 

主　　题：authentication protocol formal verification knowledge structure SAT 

摘      要：This paper introduces a new methodology for epistemic logic, to analyze communication protocols that uses knowledge structures, a specific form of Kripke semantics over hostile networks. The paper particularly focuses on automatic verification of authentication protocols. Our approach is based on the actual definitions of a protocol, not on some difficultto-establish justifications. The proposed methodology is different from many previous approaches to automatic verification of security protocols in that it is justification-oriented instead of falsification-oriented, i.e., finding bugs in a protocol. The main idea is based on observations： separating a principal executing a run of protocol from the role in the protocol, and inferring a principal＇s knowledge from the local observations of the principal. And we show analytically and empirically that this model can be easily reduced to Satisfiability （SAT） problem and efficiently implemented by a modern SAT solver.