Using Temporal Logics of Knowledge in the Formal Verification of Security Protocols

TitleUsing Temporal Logics of Knowledge in the Formal Verification of Security Protocols
Publication TypeConference Paper
Year of Publication2004
AuthorsC. Dixon, C. Fernandez-Gago, M. Fisher, and W. van der Hoek
Conference Name11th International Symposium on Temporal Representation and Reasoning (TIME’04)
Pagination148-151
PublisherIEEE Computer Society
Conference LocationTatihou, Normandie, France
ISSN Number1530-1311
Keywordssecurity protocols, temporal resolution, verification
Abstract

Temporal logics of knowledge are useful for reasoning about situations where the knowledge of an agent or component is important, and where change in this knowledge may occur over time. Here we use temporal logics of knowledge to reason about security protocols. We show how to specify part of the Needham-Schroeder protocol using temporal logics of knowledge and prove various properties using a clausal resolution calculus for this logic.
DOI10.1109/TIME.2004.1314432
Citation KeyDix04
Paper File: 
https://nics.uma.es:8082/sites/default/files/papers/Dix04.pdf