Verification of Authentication Protocols for Epistemic Goals via SAT Compilation

There are no files associated with this record.

Title Verification of Authentication Protocols for Epistemic Goals via SAT Compilation
Author Su, Kaile; Chen, Qing-liang; Sattar, Abdul; Yue, Wei-Ya; Lv, Guan-Feng; Zheng, Xi-Zhong
Journal Name Journal of Computer Science and Technology
Year Published 2006
Place of publication New York
Publisher Springer
Abstract This paper introduces a new methodology that uses knowledge structures, a specific form of Kripke semantics for epistemic logic, to analyze communication protocols 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 difficult-to-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.
Peer Reviewed Yes
Published Yes
Publisher URI http://www.springerlink.com/content/j13u70468p744626/
Copyright Statement Copyright 2006 Springer : Reproduced in accordance with the copyright policy of the publisher : The original publication will be available at SpringerLink (use hypertext links)
Volume 21
Issue Number 6
Page from 932
Page to 943
ISSN 1000-9000
Date Accessioned 2007-03-03
Date Available 2007-08-07T04:52:24Z
Language en_AU
Research Centre Institute for Integrated and Intelligent Systems
Faculty Faculty of Science, Environment, Engineering and Technology
Subject Logics and Meanings of Programs
URI http://hdl.handle.net/10072/11407
Publication Type Journal Articles (Refereed Article)
Publication Type Code c1

Brief Record

Griffith University copyright notice