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.