Using Temporal Logics of Knowledge in the Formal Verification of Security Protocols Clare Dixon, M. Carmen Fernández Gago, Michael Fisher, and Wiebe van der Hoek   View Paper (PDF)   Return to Short Papers 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. BIBTEX @inproceedings{DBLP:conf/time/DixonGFH04,    author    = {Clare Dixon and                 M. Carmen FernĂndez Gago and                 Michael Fisher and                 Wiebe van der Hoek},    title     = {Using Temporal Logics of Knowledge in the Formal Verification                 of Security Protocols.},    booktitle = {TIME},    year      = {2004},    pages     = {148-151},    ee        = {http://csdl.computer.org/comp/proceedings/time/2004/2155/00/21550148abs.htm},    crossref  = {conf/time/2004},    bibsource = {DBLP, http://dblp.uni-trier.de}  }  @proceedings{DBLP:conf/time/2004,    title     = {11th International Symposium on Temporal Representation                 and Reasoning (TIME 2004), 1-3 July 2004, Tatihou Island,                 Normandie, France},    booktitle = {TIME},    publisher = {IEEE Computer Society},    year      = {2004},    isbn      = {0-7695-2155-X},    bibsource = {DBLP, http://dblp.uni-trier.de}  } }, ©2005 Association for Computing Machinery