• DocumentCode
    3193846
  • Title

    Using temporal logics of knowledge in the formal verification of security protocols

  • Author

    Dixon, Clare ; Gago, Mari-Carmen Fernández ; Fisher, Michael ; Van der Hoek, Wiebe

  • Author_Institution
    Dept. of Comput. Sci., Liverpool Univ., UK
  • fYear
    2004
  • fDate
    1-3 July 2004
  • Firstpage
    148
  • Lastpage
    151
  • 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.
  • Keywords
    formal verification; knowledge verification; multi-agent systems; protocols; security of data; temporal logic; temporal reasoning; Needham-Schroeder protocol; agent knowledge; clausal resolution calculus; component knowledge; formal verification; security protocols; temporal logics; Authentication; Calculus; Computer science; Computer security; Cryptographic protocols; Formal verification; Information security; Logic; Niobium; Public key;
  • fLanguage
    English
  • Publisher
    ieee
  • Conference_Titel
    Temporal Representation and Reasoning, 2004. TIME 2004. Proceedings. 11th International Symposium on
  • ISSN
    1550-1311
  • Print_ISBN
    0-7695-2155-X
  • Type

    conf

  • DOI
    10.1109/TIME.2004.1314432
  • Filename
    1314432
    • Link To Document
    https://search.isc.ac/dl/search/defaultta.aspx?DTC=49&DC=3193846