We use cookies to improve your experience with our site.
Kai-Le Su, Qing-Liang Chen, Abdul Sattar, Wei-Ya Yue, Guan-Feng Lv, Xi-Zhong Zheng. Verification of Authentication Protocols for Epistemic Goals via SAT Compilation[J]. Journal of Computer Science and Technology, 2006, 21(6): 932-943.
Citation: Kai-Le Su, Qing-Liang Chen, Abdul Sattar, Wei-Ya Yue, Guan-Feng Lv, Xi-Zhong Zheng. Verification of Authentication Protocols for Epistemic Goals via SAT Compilation[J]. Journal of Computer Science and Technology, 2006, 21(6): 932-943.

Verification of Authentication Protocols for Epistemic Goals via SAT Compilation

  • This paper introduces a new methodology thatuses \it knowledge structures, a specific form of Kripkesemantics for epistemic logic, to analyze communication protocolsover hostile networks. The paper particularly focuses on automaticverification of authentication protocols. Our approach is based onthe actual definitions of a protocol, not on somedifficult-to-establish justifications. The proposed methodology isdifferent from many previous approaches to automatic verification ofsecurity protocols in that it is justification-oriented instead offalsification-oriented, i.e., finding bugs in a protocol. The mainidea is based on observations: separating a principalexecuting a run of protocol from the role in the protocol, andinferring a principal's knowledge from the local observations ofthe principal. And we show analytically and empirically that thismodel can be easily reduced to Satisfiability (SAT) problemand efficiently implemented by a modern SAT solver.
  • loading

Catalog

    /

    DownLoad:  Full-Size Img  PowerPoint
    Return
    Return