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

C. Dixon; M.-C.F. Gago; M. Fisher; W. Van Der Hoek

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

C. Dixon, M.-C.F. Gago, M. Fisher, W. Van Der Hoek

Formal Methods

Research output: Chapter in Book/Conference proceeding › Conference contribution › peer-review

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.

Original language	English
Title of host publication	Proceedings of the International Workshop on Temporal Representation and Reasoning
Publisher	IEEE Computer Society
Pages	148-151
Number of pages	4
ISBN (Print)	076952155X
Publication status	Published - 19 Jul 2004

Keywords

Security protocols
temporal resolution
Verification

Cite this

@inproceedings{60ce56ce6a724803ad0d50d7b08b12b0,

title = "Using temporal logics of knowledge in the formal verification of security protocols",

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 = "Security protocols, temporal resolution, Verification",

author = "C. Dixon and M.-C.F. Gago and M. Fisher and \{Van Der Hoek\}, W.",

year = "2004",

month = jul,

day = "19",

language = "English",

isbn = "076952155X",

pages = "148--151",

booktitle = "Proceedings of the International Workshop on Temporal Representation and Reasoning",

publisher = "IEEE Computer Society ",

address = "United States",

}

TY - GEN

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

AU - Dixon, C.

AU - Gago, M.-C.F.

AU - Fisher, M.

AU - Van Der Hoek, W.

PY - 2004/7/19

Y1 - 2004/7/19

N2 - 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.

AB - 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.

KW - Security protocols

KW - temporal resolution

KW - Verification

UR - http://www.scopus.com/inward/record.url?eid=2-s2.0-5644231064&partnerID=MN8TOARS

M3 - Conference contribution

SN - 076952155X

SP - 148

EP - 151

BT - Proceedings of the International Workshop on Temporal Representation and Reasoning

PB - IEEE Computer Society

ER -

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

Abstract

Keywords

Other files and links

Fingerprint

Cite this