Temporal Logics of Knowledge and their Applications in Security

C. Dixon; M.-C. Fernández Gago; M. Fisher; W. van der Hoek

doi:10.1016/j.entcs.2006.11.043

Temporal Logics of Knowledge and their Applications in Security

C. Dixon, M.-C. Fernández Gago, M. Fisher, W. van der Hoek

Formal Methods

Research output: Contribution to journal › Article › 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 investigate the application of temporal logics of knowledge to the specification and verification of security protocols. We show how typical assumptions relating to authentication protocols can be specified. We consider verification methods for these logics, in particular, focusing on proofs using clausal resolution. Finally we present experiences from using a resolution based theorem prover applied to security protocols specified in temporal logics of knowledge.

Original language	English
Pages (from-to)	27-42
Number of pages	16
Journal	Electronic Notes in Theoretical Computer Science
DOIs	https://doi.org/10.1016/j.entcs.2006.11.043
Publication status	Published - 2007

Keywords

Temporal logics of knowledge
Security
Verification
Theorem proving
Resolution

Access to Document

10.1016/j.entcs.2006.11.043

Cite this

@article{d29cf61973f94cb39a0870589c91812b,

title = "Temporal Logics of Knowledge and their Applications in Security",

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 investigate the application of temporal logics of knowledge to the specification and verification of security protocols. We show how typical assumptions relating to authentication protocols can be specified. We consider verification methods for these logics, in particular, focusing on proofs using clausal resolution. Finally we present experiences from using a resolution based theorem prover applied to security protocols specified in temporal logics of knowledge.",

keywords = "Temporal logics of knowledge, Security, Verification, Theorem proving, Resolution",

author = "C. Dixon and \{Fern{\'a}ndez Gago\}, M.-C. and M. Fisher and \{van der Hoek\}, W.",

year = "2007",

doi = "10.1016/j.entcs.2006.11.043",

language = "English",

pages = "27--42",

journal = "Electronic Notes in Theoretical Computer Science",

issn = "1571-0661",

publisher = "Elsevier BV",

}

TY - JOUR

T1 - Temporal Logics of Knowledge and their Applications in Security

AU - Dixon, C.

AU - Fernández Gago, M.-C.

AU - Fisher, M.

AU - van der Hoek, W.

PY - 2007

Y1 - 2007

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 investigate the application of temporal logics of knowledge to the specification and verification of security protocols. We show how typical assumptions relating to authentication protocols can be specified. We consider verification methods for these logics, in particular, focusing on proofs using clausal resolution. Finally we present experiences from using a resolution based theorem prover applied to security protocols specified in temporal logics of knowledge.

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 investigate the application of temporal logics of knowledge to the specification and verification of security protocols. We show how typical assumptions relating to authentication protocols can be specified. We consider verification methods for these logics, in particular, focusing on proofs using clausal resolution. Finally we present experiences from using a resolution based theorem prover applied to security protocols specified in temporal logics of knowledge.

KW - Temporal logics of knowledge

KW - Security

KW - Verification

KW - Theorem proving

KW - Resolution

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

U2 - 10.1016/j.entcs.2006.11.043

DO - 10.1016/j.entcs.2006.11.043

M3 - Article

SN - 1571-0661

SP - 27

EP - 42

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

ER -

Temporal Logics of Knowledge and their Applications in Security

Abstract

Keywords

Access to Document

Other files and links

Fingerprint

Cite this