Tech Reports

ULCS-03-022

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

Clare Dixon, Mari-Carmen Fernandez Gago, Michael Fisher and Wiebe van der Hoek


Abstract

Temporal logics of knowledge are useful for reasoning about situations where the knowledge of an agent or component is important, and where change may occur in this knowledge over time. Here we use temporal logics of knowledge to reason about security protocols. We show how to specify the Needham-Schroeder protocol using temporal logics of knowledge and prove various properties using a resolution calculus for this logic.

[Full Paper]