Using Temporal Logics of Knowledge in the Formal Verification of Security Protocols
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]
For each technical report listed here, copyright and all intellectual property rights remain with the respective authors. Copyright is effective from the year of publication in each case. By downloading a file from this page, you agree to use it only for purposes of research and scholarship. Any other use of this material or storage of it in any medium or its sale or distribution in any form is expressly forbidden without prior written permission from the authors concerned.